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

摘要

Petri网是形式化验证领域最重要的模型之一,具有重要的理论和应用价值.从验证算法分析的角度,Petri网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中,人们又发展了一些重要的扩展模型.对近些年来国内外学者在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几个关键验证问题的形式化定义,并重点总结了一般向量加法系统模型上可达性问题的最新研究进展和关键技术;接着总结了当限定模型的维度为固定值时相关研究进展,重点给出了2维情况的核心定理;随后介绍了几个重要扩展模型,并总结了这些模型上验证问题研究的最新进展.在每一部分,都对未来研究方向及可能面临的挑战进行了展望.%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.First,formal definitions of the vector addition systems and their key verification problems are provided with emphasis on the discussion about reachability problem,including the latest results and the main proof techniques.Then the development on the case where the dimension is a constant number rather than a variable is summarized along with some key theorems which are fundamental to the current complexity results.Furthermore,as some important variants of vector addition systems have been proposed in recent years,a brief introduction is given to the motivation and definitions 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.