VASS可达性的算法研究

Petri网理论的研究已有半个多世纪。作为一个并发及因果关系的模型，Petri网在系统规范说明和验证中有广泛的应用。Petri网有两个等价的、更适合于理论研究的模型，即向量加法系统（VAS）和带状态的向量加法系统（VASS）。用VASS模型，我们可以对系统性质进行形式化和算法验证。在所有的VASS性质里，最具挑战性的是可达性。形式语言、逻辑和并发中的一大类问题都可以转化成VASS的可达性问题。一些理论计算机科学中的著名问题和VASS的一些变种上的可达性问题等价，如BVASS（Branching VASS）的可达性。本申请项目拟对理论计算机科学中的两个著名的公开问题进行研究，目标一是给出VASS可达性问题的一个完备性结果，目标二是证明BVASS的可达性问题是可判定的。本项研究对验证理论和系统安全有重要意义。

Petri net theory has been studied for well over half a century. As a model for concurrency and causality, Petri net model finds a wide range of applications in system specification and verification. Two equivalent formulations of Petri nets, Vector Addition System (VAS) and Vector Addition System with States (VASS), have been investigated in theoretical setting. Many system properties can be formalized and checked algorithmically in VASS model, among which reachability has proved to be the most challenging one. A variety of problems in language, logic, and concurrency can be reduced to VASS reachability problem. Some famous problems in theoretical computer science are related to reachability problem of extended VASS, say BVASS (branching VAS). The project proposes to carry out investigations into two important open problems in theoretical computer science. One is to give a complete characterization of the complexity of the VASS reachability problem. This problem has been open for fifty years. The other is to prove that BVASS reachability problem is decidable. The studies will be significant to verification, system safety, and computer science logic.