2023 Fiscal Year Annual Research Report
Formalization of the decidability of the reachability problem for vector addition systems
| Project/Area Number |
18K11154
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
|
|---|
| Project Period (FY) |
2018-04-01 – 2024-03-31
|
| Keywords | 定理証明支援系 / 形式化 / ベクトル加算系 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
最終年度は、研究室所属の大学院生と共同で、状態付きベクトル加算系の到達可能性問題を、状態なしのベクトル加算系の到達可能性問題に還元させる方法の形式化を完成させた。これにより、ベクトル加算系の到達可能性の決定可能性を、状態付きベクトル加算系にも適用させることが可能となる。
研究期間全体を通じて、研究室所属の大学院生と共同で、ベクトル加算系およびそれと等価な状態遷移系における到達可能性問題周辺のいくつかの問題について形式化を完成させた。具体的には、ペトリネットの有界性問題および停止性問題に関する形式化である。とくに有界な場合の到達可能性が決定可能であることも形式化しているが、この問題に一般のベクトル加算系の到達可能性問題を還元させることが可能であることが2020年に発表されている。
ベクトル加算系における到達可能性問題の決定可能性については形式化の完成を見なかったが、この問題に対する様々な証明手法を調査することで、2019年に発表されたHaskell上の到達可能性判定プログラムKReachで用いられている手法が形式化に有望なのではないかという知見を得た。現在、この手法で必要となるいくつかの補題について形式化が進行中である。引き続きこの方針で形式化を進めていく予定である。
|
