2019 Fiscal Year Research-status 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 – 2023-03-31
|
| Keywords | 定理証明支援系 / 形式化 / ベクトル加算系 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
2年目となる本年度は、ベクトル加算系と等価な状態遷移系であるペトリネットについて、我々の以前の研究である被覆性問題の決定可能性の形式化と、前年度に行った有界性に関する各種性質の形式化を拡張する形で、停止性に関する性質をいくつか形式化した。初期マーキング付きペトリネットが停止性を持つとは、その初期マーキングから始まる無限の遷移列が存在しない、すなわち、どのように遷移し続けたとしてもいずれ遷移できなくなることである。この停止性について、被覆性問題の決定可能性の形式化の際に構築したKarp-Miller木を用いて判定可能であることを、定理証明支援系Coqおよび証明言語であるSSReflect、数学ライブラリMathCompを用いて形式化した。
また、上述のKarp-Miller木と到達可能性の双方に深く関連するイデアルに関する理論のライブラリの整備に向けて、MathCompにおける順序関係ライブラリ等の基本的な調査を行った。次年度以降はこのイデアルに関する理論のライブラリを本格的に整備していく予定である。
研究協力者 井上 健太 (千葉大学), 稲垣 衛 (千葉大学)
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
今年度は学科長という立場であったこともあり、あまりまとまった時間をかけることができなかったため、進行が見られた部分は完全に新規のものというよりも、これまでの研究の続きの側面が強い。
|
| Strategy for Future Research Activity |
次年度は当初今年度に予定していたイデアルに関するライブラリの整備をより強力に推し進め、本題の到達可能性問題に活用することを目指す。
|
| Causes of Carryover |
今年度は学科長であったことで出張を控えたため、未使用額が生じた。
次年度以降、COVID-19の状況が改善し次第、旅費として使用する計画である。
|
