2010 Fiscal Year Annual Research Report
等式付ツリーオートマトンの算術制約翻訳可能性と自動検証技術への応用に関する研究
| Project/Area Number |
21700022
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
大崎 人士 独立行政法人産業技術総合研究所, 産学官連携推進部門, 連携研究体副体長 (00356627)
|
|---|
| Keywords | ツリーオートマトン / 書き換え系 / 計算論 / 可換文法 / 算術制約 |
|---|
| Research Abstract |
正則ACツリーオートマトン(regular AC-tree automata)の葉言語(leaf-languages)を表現する正則可換文法(commutative regular grammar)は、線形算術制約および正数ベクトル加算系(non-negative vector-addition systems)と等価な表現力を持つ(Parikh1966他)。本研究では、正数ベクトル加算系の定義を、整数(正値、零、負値)から成る座標系上に拡張した場合、それに対応する可換文法が満たすべき代数的性質を解明する。本研究では始めに、可換クリーニ代数の上に割り算の概念を導入するため、単項演算子iを導入して、可換クリーニ代数の公理系にiに関する6つの新たな公理を加えた(i-可換クリーニ代数と呼ぶ)。次に、i-可換クリーニ代数の具体例であるi-可換正規文法に着目して、HopkinsとKozen(1999)による「Parikhの定理の一般化」の中で用いられた言語多項式のテイラー展開の手法が、i-可換正規文法に適用可能であることを示した。その結果、(1)i-可換正規文法は、た可換文脈自由文法と等価な表現力を持つこと、(2)i-可換正規文法は、整数ベクトル加算系と等価な表現力を持つことが示せた。以上により、正則可換文法、線形算術制約、正数ベクトル加算系の同形関係は、整数制約上へ自然に拡張可能であることが判明した。
以上の成果とともに、本研究では、大崎(2001)が提唱する等式付ツリーオートマトン理論の普及活動を行った。研究期間中には、国際サマースクール(ISR'09)や、複数の国内大学(大阪大学、北海道大学他)にて等式付オートマトンの講義を行い、計算機科学分野の若い研究者らに広める機会を創出した。
|
