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

2020 Fiscal Year Research-status Report

• 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年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
今年度オンラインで開催された国際会議LICS/ICALPでのJerome Leroux氏による招待講演において、一般のベクトル加算系の到達可能性問題が、有界なベクトル加算系の到達可能性問題に対数領域還元可能であるという内容が発表された。後者の有界な場合に限った決定可能性や判定アルゴリズムは、一般の場合と比較して格段に易しい。この還元は前年度に同氏らがLICSで発表した論文中の定理の応用となっており、今年度はこの内容について調査を行った。有界なベクトル加算系への還元によって決定可能性を示すという方法は、本研究課題の開始時点では知られていなかった新しい手法である。還元先である有界なベクトル加算系の到達可能性問題の決定可能性については、それと等価である有界なペトリネットに関しては本研究課題の初年度で形式化を行っているため、その成果を利用できるのではないかと考えている。

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

今年度はコロナ禍で授業形態が大きく変更されたことに伴う対応に時間を割かざるを得なかったため。

Strategy for Future Research Activity

コロナ禍による授業形態の変更への対応は今年度である程度ノウハウが蓄積されたため、次年度以降は本研究課題の遂行に時間をかけることができるように思われる。

Causes of Carryover

今年度はコロナ禍で出張が不可能であったため、未使用額が生じた。
次年度以降、状況が改善し次第、旅費として使用する計画である。
今後の進捗状況によっては期間延長も考慮に入れる。