2018 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年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
また、ベクトル加算系と等価な状態遷移系であるペトリネットについて、我々の以前の研究である被覆性問題の決定可能性の形式化を拡張する形で、有界性に関する性質をいくつか形式化した。具体的には、有界性の決定可能性、有界性の複数の定義の間の同値性、有界であるときの到達可能性の決定可能性である。有界であるときに限定した場合の到達可能性の決定可能性は一般の場合と比較すれば非常に簡単な問題ではあるが、これは、研究協力者の大学院生に、形式化に使用している定理証明支援系Coqおよび証明言語であるSSReflect、数学ライブラリMathCompに習熟してもらうことをねらいとしている。
次のステップとしては2017年に発表された、イデアル・カープ・ミラー・アルゴリズムの形式化を考えている。この形式化には、被覆性問題の決定可能性の形式化に関する我々の知見を生かせることが期待できるとともに、形式化の過程で前述のイデアルに関するライブラリを整備することにより、本題の到達可能性問題に活用できるのではないかと考えている。
研究協力者 稲垣 衛 (千葉大学)
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
初年度に実施することを想定していた基本的な調査、さらには研究協力者となる大学院生に対して適切な難易度の具体的な問題の解決を通して形式化をある程度習熟させることは、予定通り行えたと考える。
|
| Strategy for Future Research Activity |
「研究実績の概要」でも述べたが、次はイデアル・カープ・ミラー・アルゴリズムの形式化を通して、被覆性問題の決定可能性の形式化に関する我々の知見を生かすともに、形式化の過程でイデアルに関するライブラリを整備することで、本題の到達可能性問題に活用することを目指す。
|
| Causes of Carryover |
当初の計画では、初年度の予算の多くを研究協力者である大学院生が使用するノートパソコンの購入費用として計上していたのだが、院生が既に所持していた自分のノートパソコンを使用することを希望したため、この分が未使用となった。来年度以降に次の大学院生が配属された場合に同様にノートパソコンの購入費用として使用する計画である。
|
