2015 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 |
時間プッシュダウン・オートマトンと呼ばれる計算モデルに関する研究を行い，新たな体系Synchronized Recursive Timed Automata(SRTA)を導入し，その成果を国際会議で報告した．
当研究課題の目的は，プッシュダウン・オートマトンの拡張における本質的な構造の抽出と，これをもとに重要な判定問題である到達可能性問題の容易な証明を獲得し，到達可能性判定手続きを実装することである．今年度の成果は，「本質的な構造の抽出」と「容易な証明の獲得」に相当する．
時間プッシュダウン・オートマトンは，プッシュダウン・オートマトンと時間オートマトンを組合せた計算モデルで，スタックの要素として単一の実数（クロックと呼ばれる）を考える．スタックに加え，実数の稠密性や非有界性という異なる無限性を含む，理論的に高度なプッシュダウン・オートマトンの拡張である．
2012年に，時間プッシュダウン・オートマトンの一つ，Dense Timed PushDown Automata(DTPDA)に対し，到達可能性問題が決定可能であることが証明された．ただし，その証明は難解で，それをもとに更なる拡張を行うことは困難であった．そこで，決定可能性を導く要諦を明らかにするべく，証明の構造を調べ，DTPDAの本質をSRTAとして形式化した．
SRTAはDTPDAの拡張となっており，例えば，DTPDAではスタックの要素は単一のクロックであるのに対し，SRTAではクロックの組が要素となる．また，クロックの値を比較したり，クロックの小数部分の値を検査できる．これらの拡張はDTPDAで表現不能な言語を表すのに有効で，SRTAはDPDAより表現力が強いことが分かった．さらに，SRTAはDTPDAの拡張でありながら，到達可能性問題は決定可能である．この証明は，直感的な性質の組み合わせからなる，明瞭なものである．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
今年度の研究実施計画は，時間プッシュダウン・オートマトンのうち，到達可能性問題の決定可能性が分かっているDense-Timed PushDown Automata(DTPDA)について研究し，DTPDAの本質的な構造を抽出することにあった．
研究実績に記載の通り，新たな体系 Synchronized Recursive Timed Automata(SRTA) を，DTPDAに対する分析によって獲得することができたこと，そしてSRTAはDTPDAを真に拡張したものでありながら，到達可能性問題は依然として決定可能であることから，DTPDAの本質を適切な形で定式化できたと考える．
したがって，「当初の計画以上に」研究が進んでいると評価する．
DTPDAという具体的な体系に対しては深い理解に至ったと考えるが，一方で，研究課題全体からみると不満が残る．
研究課題は，プッシュダウン・オートマトンの広範な拡張に共通する本質的な構造を抽出し，これを具体的な体系や枠組みとして形式化することである．この視点に立つと，SRTAとは，あくまでもDTPDAに立脚した限定的な体系であると言わざるをえない．最終的な目標は，SRTAをも含む枠組みを与えるということにあるが，この点については，【今後の研究の推進方策】で詳述する．
|
| Strategy for Future Research Activity |
時間プッシュダウン・オートマトンの研究上で導入した，Synchronized Recursive Timed Automata(SRTA)は，既存の重要な体系であるDense-Timed Pushdown Automata(DTPDA)を，真に拡張するものである．ただし本研究課題の狙いが，広範なプッシュダウン・オートマトンの拡張に共通する本質的構造の抽出にあることを考えると，SRTAはDTPDAに立脚した限定的な拡張であると言わざるをえない．
今後はSRTAを含むと同時に，プッシュダウン・オートマトンの他の重要な拡張（高階プッシュダウン・オートマトンや，マルチスタック・プッシュダウン・オートマトン）をも包含する，より一般的な枠組みを与えることに注力する．
具体的には，SRTAを更に拡張し，これをWeighted Pushdown Automataと呼ばれる抽象的枠組みで扱うことを考えている．更なる拡張とは，時間オートマトンの一種，更新可能時間オートマトンの特徴である「クロックの更新操作」を，SRTAに取り込むことを指す．既に，SRTAの特徴である「クロック値の小数部検査」を更新可能時間オートマトンに取り込むと，興味深い表現力を持つ体系となることを証明している．このことから，SRTAにクロックの更新操作を加えると表現力が拡張されるが，同時に到達可能性問題の決定可能性も予想される．しかし，決定可能性は予想されるものの，SRTAに対する既存の証明は有効ではないことが分かっている．
そこで，より抽象的なWeighted Pushdown Automataの枠組みを通して，このSRTAの拡張を分析し，Weighted Pushdown Automataの理論を一層精緻なものとしながら，決定可能性証明を与えることを考えている．
|
