2022 年度実施状況報告書

ベクトル加算系における到達可能性問題の決定可能性の形式化

研究課題

研究課題/領域番号	18K11154
研究機関	千葉大学
研究代表者	山本光晴千葉大学, 大学院理学研究院, 教授 (00291295)
研究期間 (年度)	2018-04-01 – 2024-03-31
キーワード	定理証明支援系 / 形式化 / ベクトル加算系
研究実績の概要	本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。今年度は、一般のベクトル加算系の到達可能性問題を、有界なベクトル加算系の到達可能性問題に還元する方法について引き続き調査・検討を行った。この還元によって決定可能性を示すという方法は、本研究課題の開始時点では知られていなかった新しい手法である。還元先である有界なベクトル加算系の到達可能性問題の決定可能性や判定アルゴリズムは、一般の場合と比較して格段に易しく、それと状態遷移系として等価である有界なペトリネットに関する到達可能性と判定アルゴリズムは、本研究課題の初年度で形式化を行っているため、その成果を利用できることが見込まれる。また、この還元は到達可能性の決定可能性だけでなく、到達可能性の計算量の上界を示す際にも用いられるため、この還元の形式化により、将来的には到達可能性の計算量の形式化にも寄与することが期待される。異なる状態遷移系およびそれらの間の関係を統一的に記述するため、形式化に使用している証明言語SSReflectの上に開発されているライブラリHierarchy Builderを使用する。ベクトル加算系とペトリネットの間の関係については大学院生と共同で形式化を進めている。
現在までの達成度 (区分)	現在までの達成度 (区分) 4: 遅れている理由 2020年度来のコロナ禍で授業形態が大きく変更されたことに伴う対応に時間を割き進捗が遅れたが、その影響を十分に取り戻せていない状況である。
今後の研究の推進方策	今年度が本研究課題の最終年度であるが、現在までの進捗状況に鑑み、期間を延長する。また、2020年度・2021年度は配属されていなかった大学院生が2022年度は配属されたため、当初の計画通り、大学院生と共同で分担して課題を進めていく。2022年度前半は証明検証系Coq, 証明言語SSReflectおよび数学ライブラリMathCompの基本的な使い方の習得が主であったが、2022年度末から実際の問題にとりかかっている。
次年度使用額が生じた理由	当初計画では今年度が最終年度であったが、課題期間を延長することから、次年度使用額を残した。また、今年度はデスクトップパソコンを購入する予定であったが、円安の影響もあり、既存のノートパソコンを接続する外付けモニターの購入に留めた。次年度は旅費やパソコンの購入費用に充てる予定である。