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

来源：软件学报杂志2018年第6期北京时间：

作者：张文博,龙环

单位：张文博，上海交通大学 软件学院, 上海 20024011,龙环，上海交通大学 计算机科学与工程系, 上海 20024002

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

关键词：Petri网;向量加法系统;可达性;形式化验证;算法复杂性

基金资助：国家自然科学基金（61472239，61772336，61572318）