2016 Fiscal Year Annual Research Report
再帰プログラムの拡張における到達可能性問題を広く可解とする構造の究明と応用
| Project/Area Number |
15J01843
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
上里 友弥 筑波大学, システム情報工学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2015-04-24 – 2018-03-31
|
| Keywords | プッシュダウンオートマトン / 時間オートマトン / 到達可能性問題 |
|---|
| Outline of Annual Research Achievements |
本年度は、以下二つの結果を得た
1. 時間オートマトンとプッシュダウン・オートマトンを組合せた計算モデルとして、時間プッシュダウン・オートマトン（Dense-Timed Pushdown Automata, TPDA）が2012年にAbdullaらにより導入された。TPDAは、複雑な体系でありながらも、位置到達可能性問題と呼ばれる重要な判定問題が解けることから注目を集めている。このTPDAを拡張し、新たに「複数の局所クロックを持つTPDA（TPDA with Multiple-Local Clocks, MTPDA）」を提案した。MTDPAは一見ではTPDAより遥かに強力な体系に思えるのだが、今回示したMTPDAにおけるUntiming定理により、TPDAと同等の表現力を持つ（同じ言語クラスを特徴づける）ことを示した。MTPDA版のUntiming定理は、先行研究のTPDA版のUntiming定理の証明を単純化し精緻化することで証明した。
2. 昨年度に提案した、TPDAを真に含む計算モデル、Synchronized Recursive Timed Automata (SRTA) に対してより精密な結果を与えた。昨年度は、SRTAの「位置到達可能性問題」と呼ばれる判定問題が解けることを証明した。この証明では、backward-simulationと呼ばれる証明手法が重要であったが、これを利用して、新たに「計算状況到達可能性問題」の決定可能性を示した。この判定問題は、SRTAに限定された問題ではなく、時間オートマトンの場合についても自然に考えることができ、その場合の決定可能性は既知である。しかし、我々の知る限りでは、backward-simulationに基づく証明は存在しないため、時間オートマトンに関しても新たな証明方法を得たことになる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今年度は、時間プッシュダウン・オートマトン（TPDA）及びSynchronized Recursive Timed Automata (SRTA)を、既存の有力な枠組みの中で再形式化し、到達可能性問題に対するより単純な証明を与えることを目的としていた。特に、既存の有力な枠組みとして、我々が既に提案したPushdown Systems with Stack Manipulation (TrPDS) を考えていた。
TPDAやSRTAには、「時間遷移」と呼ばれる、スタック全体を書き換える操作がある。TrPDSは、スタック全体を操作する拡張を扱う枠組みであるから、TPDAやSRTAをTrPDSとして形式化することは自然な発想である。しかし、TPDAやSRTAの時間操作は、TrPDSの枠組みで自然に形式化することが難しいことが比較的早い段階で分かった。そのため、TPDAとSRTAの両方を一層詳細に分析することと、それと同時にTrPDSを一般化することが不可欠であると考え、まずTPDAとSRTAの構造を調べることにした。その結果、研究概要に記した成果をあげることができたため、目的のうち前半については達成できたと考える。一方で、今年度ではTrPDSの一般化までは至らなかった。しかし、一般化の際に注意しなければならない点についての洞察を得ることができたため、このことも踏まえ「おおむね順調に進展している」とした。
現在はTrPDSを一般化することで、これまで難しいと考えられていたTPDAとSRTAの形式化が自然に達成できると考えている。この点については、【今後の研究の推進方策】で詳述する。
|
| Strategy for Future Research Activity |
次年度は、TrPDSを一般化することで、時間プッシュダウン・オートマトン（TPDA）及びSynchronized Recursive Timed Automata (SRTA) を形式化することを考えている。TrPDSは、形式言語理論の道具である文字列変換器(transducer)でプッシュダウン・オートマトンを拡張した計算モデルである。文字列変換器は、文字列を文字列の集合に非決定的に変換する関数を実現する計算モデルで、TrPDSではスタックをスタックの集合に変換する為に用いる。
TPDAやSRTAを自然に模倣しようとしたとき、これらに固有の操作である「時間遷移」を文字列変換器では表現できない点が問題となることが分かった。時間遷移を模倣するためには、スタックの中の離れた箇所にある要素を「同期」する必要がある。しかし、離れた箇所にある要素に対する関係を追加すると、文字列ではなく、より一般の構造であるグラフを操作することになる。
そこで、文字列から文字列の集合に変換する文字列変換器ではなく、グラフからグラフの集合に変換するグラフ変換器（graph transduction）と呼ばれる、より一般的な道具を使うことを考えている。ただし、到達可能性問題を決定可能とするには、単なるグラフではなく、木幅有界(bounded tree-width)なグラフに収めなくてはならないことも、グラフ変換器の理論から分かっている。
既に我々の行ったSRTAに対する到達可能性問題の決定可能性証明は、「同期」情報を一切持たないが、不自然な形式化を行っているとみなせる。一方で、素直に同期情報をグラフとして表現すると、木幅が有界とならないことも分かっている。そこで、SRTAのスタック構造を自然に、かつ、木幅有界となるように符号化する新たな方法を開発する必要があり、これに取り組む。
|
