2017 Fiscal Year Annual Research Report

再帰プログラムの拡張における到達可能性問題を広く可解とする構造の究明と応用

Research Project

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)と呼ばれる時間プッシュダウン・オートマトンにおける「到達可能性問題」の構造的な決定可能性証明を与えた。SRTAは上里が2015年に導入した計算モデルで、時間プッシュダウン・オートマトンで基礎となる二つの体系Pushdown Timed Automata(PTA)やDense-timed Pushdown Automata(DTPDA)を拡張し、特に言語クラスについてこの二つより真に強い。今回与えた証明は、SRTAの素朴な意味論に加え、複数の中間意味論と有限性を備える抽象意味論という4つの意味論を用いた段階的なものになっている。これにより、証明が簡明になっただけでなく、決定可能性を成立させる上で重要な構造や手法が明らかになったと言える。この内容をまとめた雑誌論文が出版済みである。 ②「複数の局所クロックを持つ時間プッシュダウン・オートマトン(MTPDA)」を提案した。MTPDAは、DTPDAを次の点で拡張する体系である (i) DTPDAでは局所クロックがただ一つであるのに対し、複数の局所クロックを許す; (ii) DTPDAでは局所クロックの値の検査やリセットが非常に制限されていたのに対し、これらの操作に対する制限がない。見かけには既存のPTAやDTPDAを大きく拡張することになるが、今回は（形式言語のクラスとして）これらと同等の表現力を持つことを示した。この結果自体が見かけに反する意外なものであるが、同時に、他の拡張の言語クラスを調べる上でも有効な証明手法を確立できたと考える。この内容をまとめた雑誌論文も出版済みである。
Research Progress Status	29年度が最終年度であるため、記入しない。
Strategy for Future Research Activity	29年度が最終年度であるため、記入しない。