向量加法系统验证问题研究综述

Petri网是形式化验证领域最重要的模型之一,具有重要的理论和应用价值.从验证算法分析的角度Petri网可以被等价地抽象为"向量加法系统".在对向量加法模型的研究中人们又发展了一些重要的扩展模型.本文对近些年来国内外学者在向量加法系统验证领域取得的成果进行了系统总结.首先,给出了向量加法系统及几个关键验证问题的形式化定义,并重点总结了一般向量加法系统模型上可达性问题的最新研究进展和关键技术;接着,总结了当限定模型的维度为固定值时相关研究进展,重点给出了2维情况的核心定理;随后,介绍了几个重要扩展模型,并总结了这些模型上验证问题研究的最新进展.在每一部分都对未来研究方向及可能面临的挑战进行了展望.

State-of-the-Art Survey on Verification of Vector Addition Systems

Petri nets is a fundamental model in the area of formal verification. It is popular in both theoretical study and application. For the analysis of algorithmic properties of Petri nets, they are often equivalently viewed as vector addition systems. This survey gives a comprehensive review of the recent achievements in this area. We start by giving formal definitions of the vector addition systmes and the key verification problems, focusing on the discussion about reachability problem, including the latest results and the main proof techniques. Then we summarize the development on the case where the dimension is a constant number rather than a variable, along with some key theorems which are fundamental to the current complexity results. Furthermore, as some important variants of vector addition systems are proposed in recent years, we also give a brief introduction to the motivation and definintions of some of the most representative ones, and the latest results on verification relating to these models. In addition, possible future work are highlighted at the end of each section.