Formalization of the decidability of the reachability problem for vector addition systems
| 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 |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
|
|---|
| Project Period (FY) |
2018-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Fiscal Year 2022: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2021: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2020: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2019: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 定理証明支援系 / 形式化 / ベクトル加算系 / 到達可能性 / ペトリネット |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
今年度は、一般のベクトル加算系の到達可能性問題を、有界なベクトル加算系の到達可能性問題に還元する方法について引き続き調査・検討を行った。この還元によって決定可能性を示すという方法は、本研究課題の開始時点では知られていなかった新しい手法である。還元先である有界なベクトル加算系の到達可能性問題の決定可能性や判定アルゴリズムは、一般の場合と比較して格段に易しく、それと状態遷移系として等価である有界なペトリネットに関する到達可能性と判定アルゴリズムは、本研究課題の初年度で形式化を行っているため、その成果を利用できることが見込まれる。また、この還元は到達可能性の決定可能性だけでなく、到達可能性の計算量の上界を示す際にも用いられるため、この還元の形式化により、将来的には到達可能性の計算量の形式化にも寄与することが期待される。
異なる状態遷移系およびそれらの間の関係を統一的に記述するため、形式化に使用している証明言語SSReflectの上に開発されているライブラリHierarchy Builderを使用する。ベクトル加算系とペトリネットの間の関係については大学院生と共同で形式化を進めている。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
2020年度来のコロナ禍で授業形態が大きく変更されたことに伴う対応に時間を割き進捗が遅れたが、その影響を十分に取り戻せていない状況である。
|
| Strategy for Future Research Activity |
今年度が本研究課題の最終年度であるが、現在までの進捗状況に鑑み、期間を延長する。また、2020年度・2021年度は配属されていなかった大学院生が2022年度は配属されたため、当初の計画通り、大学院生と共同で分担して課題を進めていく。2022年度前半は証明検証系Coq, 証明言語SSReflectおよび数学ライブラリMathCompの基本的な使い方の習得が主であったが、2022年度末から実際の問題にとりかかっている。
|
Report
(5 results)
Research Products
(4 results)
