权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

向量加法系统可达性问题可判定性的形式化

基本信息

批准号：
18K11154
负责人：
山本光晴
金额：
$ 1.58万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2018
资助国家：
日本
起止时间：
2018-04-01 至 2024-03-31
项目状态：
已结题

项目摘要

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

The purpose of this study is to formalize the problem of arrival probability in addition to the system of theorem proving. This problem was solved in 1981 and proved in 1990. In 2011, the complex decomposition operation was used in the form of a new proof, and the proof was simplified. The old proof is now complex decomposition operation, the theory is reverse "decomposition" and the call is beautiful characteristic pay is reverse, the recent research is clear. This year, the general algorithm arrival probability problem, the bounded algorithm arrival probability problem and the method of return are discussed. The method of determining the possibility of this study is to know the starting point of this study. In this paper, we discuss the possibility of arrival determination of bounded additive system, and compare the probability of arrival determination of bounded additive system with the probability of arrival determination of state transition system. For example, the probability of determining the probability of arrival of the return element is determined by the upper bound of the calculation quantity of the probability of arrival. The relationship between different state transitions is described in a unified way, and the formal use is used to prove the development of speech SSReflect. The relationship between college students and common formalization