Formalization of the decidability of the reachability problem for vector addition systems

2023 Fiscal Year Final Research Report

• Project/Area Number: 18K11154
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Chiba University
• Principal Investigator: Yamamoto Mitsuharu 千葉大学, 大学院理学研究院, 教授 (00291295)
• Project Period (FY): 2018-04-01 – 2024-03-31
• Keywords: 定理証明支援系 / 形式化 / ベクトル加算系

Outline of Final Research Achievements

We have formalized several problems around reachability for vector addition systems or their equivalent state transition systems. Concretely, boundedness and termination for Petri nets, and reachability-preserving transformation from a vector addition system with states to a vector addition system are formalized. Although formalization of the decidability of the reachability problem for vector addition systems could not be completed, some insight into promising approach to formalization is obtained by investigating several methods for proving the decidability.

Free Research Field

情報数理学

Academic Significance and Societal Importance of the Research Achievements

定理証明支援系を用いた形式化によって、機械的に検査された正しい証明が得られるだけでなく、一旦完了した証明に対する試行錯誤や適切な抽象化の検討がしやすくなる。本研究の成果の一部である状態付きベクトル加算系からベクトル加算系への変換の形式化においても、適切な抽象化を行うことで元の証明に用いられていた変換が改良された。
また、形式化の過程で構築・蓄積された技術やノウハウは、後に別の定理を形式的に証明する際の道具として生かされる。上記の変換の形式化においてもベクトルの回転に関するライブラリが整備された。