再帰プログラムの拡張における到達可能性問題を広く可解とする構造の究明と応用
| Project/Area Number |
15J01843
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
上里 友弥 筑波大学, システム情報工学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2015-04-24 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2017: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2016: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2015: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| 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年度が最終年度であるため、記入しない。
|
Report
(3 results)
Research Products
(7 results)
-
-
-
-
[Journal Article] Synchronized Recursive Timed Automata2015
Author(s)
Yuya Uezato and Yasuhiko Minamide
-
Journal Title
Logic for Programming, Artificial Intelligence, and Reasoning
Volume: LNCS 9450
Pages: 249-265
DOI
ISBN
9783662488980, 9783662488997
Related Report
Peer Reviewed / Acknowledgement Compliant
-
-
-
