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

点击翻译按钮获取中文摘要

本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。今年度は、一般のベクトル加算系の到達可能性問題を、有界なベクトル加算系の到達可能性問題に還元する方法について引き続き調査・検討を行った。この還元によって決定可能性を示すという方法は、本研究課題の開始時点では知られていなかった新しい手法である。還元先である有界なベクトル加算系の到達可能性問題の決定可能性や判定アルゴリズムは、一般の場合と比較して格段に易しく、それと状態遷移系として等価である有界なペトリネットに関する到達可能性と判定アルゴリズムは、本研究課題の初年度で形式化を行っているため、その成果を利用できることが見込まれる。また、この還元は到達可能性の決定可能性だけでなく、到達可能性の計算量の上界を示す際にも用いられるため、この還元の形式化により、将来的には到達可能性の計算量の形式化にも寄与することが期待される。異なる状態遷移系およびそれらの間の関係を統一的に記述するため、形式化に使用している証明言語SSReflectの上に開発されているライブラリHierarchy Builderを使用する。ベクトル加算系とペトリネットの間の関係については大学院生と共同で形式化を進めている。