向量加法系统验证问题研究综述-张文博 , 龙环.pdf
免费下载
软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2018,29(6):1566−1581 [doi: 10.13328/j.cnki.jos.005465] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563
向量加法系统验证问题研究综述
∗
张文博
1
,
龙
环
2
1
(上海交通大学 软件学院,上海 200240)
2
(上海交通大学 计算机科学与工程系,上海 200240)
通讯作者:龙环, E-mail: longhuan@sjtu.edu.cn
摘 要: Petri 网是形式化验证领域最重要的模型之一,具有重要的理论和应用价值.从验证算法分析的角度,Petri
网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中,人们又发展了一些重要的扩展模型.对近些年来
国内外学者在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几个关键验证问题
的形式化定义,并重点总结了一般向量加法系统模型上可达性问题的最新研究进展和关键技术;接着总结了当限定
模型的维度为固定值时相关研究进展,重点给出了 2 维情况的核心定理;随后介绍了几个重要扩展模型,并总结了这
些模型上验证问题研究的最新进展.在每一部分,都对未来研究方向及可能面临的挑战进行了展望.
关键词: Petri 网;向量加法系统;可达性;形式化验证;算法复杂性
中图法分类号: TP311
中文引用格式: 张文博,龙环.向量加法系统验证问题研究综述.软件学报,2018,29(6):1566−1581. http://www.jos.org.cn/1000-
9825/5465.htm
英文引用格式: Zhang WB, Long H. State-of-the-Art survey of the verification of vector addition systems. Ruan Jian Xue Bao/
Journal of Software, 2018,29(6):1566−1581 (in Chinese). http://www.jos.org.cn/1000-9825/5465.htm
State-of-the-Art Survey on Verification of Vector Addition Systems
ZHANG Wen-Bo
1
, LONG Huan
2
1
(School of Software, Shanghai Jiaotong University, Shanghai 200240, China)
2
(Departmet of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240, China)
Abstra ct : 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.
Key words: Petri nets; vector addition systems; reachability; formal verification; complexity
自 1962 年 Petri 网
[1]
的概念提出以来,经过半个多世纪的发展,其已成为描述与分析并发系统最重要的形式
∗ 基金项目: 国家自然科学基金(61472239, 61772336, 61572318)
Foundation item: National Natural Science Foundation of China (61472239, 61772336, 61572318)
本文由形式化方法的理论基础专题特约编辑傅育熙教授、李国强副教授、田聪教授推荐.
收稿时间: 2017-07-01; 修改时间: 2017-09-01; 采用时间: 2017-11-06; jos 在线出版时间: 2017-12-28
CNKI 网络优先出版: 2017-12-29 13:19:12, http://kns.cnki.net/kcms/detail/11.2560.TP.20171229.1318.005.html
张文博 等:向量加法系统验证问题研究综述
1567
化工具之一.除在并发程序语言形式化验证中的重要应用外,Petri 网模型还被广泛应用于生物、化学、金融、
网络、安全等不同领域的建模和分析
[2−9]
.其中,Ball 等人定义了并行库系统(parameterized library system,简称
PLS),在此基础上实现了多线程程序的模型检测工具
[2]
,并证明了 PLS 系统上的一些验证问题与 Petri 网上的验
证问题等价;Aalst 用 Petri 网对工作流管理系统进行建模,用 Petri 网理论来验证工作流过程的正确性
[3]
;Heiner
等人
[4]
用 Petri 网对生化反应过程建模,实现了对生化系统中短时间内的行为进行有效的分析等.国内的研究者
也对类似问题进行了深入研究,特别是将 Petri 网理论广泛应用于对网络及安全等领域的验证.代表性的工作包
括:北京交通大学 Lei 教授等人用 Petri 网对无线网络系统建模,以实现对无线网络的性能的有效分析
[5]
;清华大
学林闯教授等人在 Petri 网的基础上定义了私有 Petri 网,对恶意软件造成的私有信息泄露行为进行分析
[6]
;以及
同济大学 Yu教授等人用 Petri 网对电子商务的支付过程建模,验证电子商务支付系统的安全性
[7]
等.
与 Petri 网等价的数学模型向量加法系统(vector addition system,简称 VAS) 具有数学描述上的简洁性,且现
实中并发系统的状态和迁移往往都可以用向量描述,故 VA S 本身也具有重要的理论和应用价值.VAS 模型验证
的核心问题之一是可达性(reachability)问题,即对给定的 VA S 模型,判断从一个初始格局出发能否到达一个指
定的目标格局.令人遗憾的是:虽然关于 VA S 已经有了大量的理论和应用研究,也有了一些高效的实现工具,但
对可达性问题的复杂性,至今仍没有给出令人满意的回答.另一方面,VAS 是极为简洁的系统,在实际研究中,人
们根据不同的应用背景提出了一些重要的扩展模型(如下推向量加法系统 PVAS、交互向量加法系统 AVAS S 、
分枝向量加法系统 BVASS、带数据的 Petri 网模型 PND(Petri nets with data)等).但对这些模型的相关验证问题
的研究都处于初始阶段.
本文第 1 节形式化定义向量加法系统及一些重要的验证问题.第 2 节为本文重点,总结一般 VA S 上可达性
问题的主要结论和核心研究技术.第 3 节陈述当维度固定时 VA S 上可达性问题的主要结论和技术.第 4 节总结
几个重要 VA S 扩展模型上的验证问题的结论.第 5 节给出现有主要验证结论一览表.本文覆盖了 VA S 研究领域
的最新进展、关键技术和开放问题.
1 向量加法系统基础
1.1 VAS的形式化定义
向量加法系统(vector addition system,简称 VAS ), 可以表示为二元组 V=〈d,A〉.d∈
表示 V 的维度,A⊆
d
表示
迁移规则(transition rule)集合.VAS 中的一次迁移
a
V
uv⎯⎯→ 满足 v=u+a,其中,u,v∈
d
,a∈A.VAS 的一次从向量 u
0
到 u
n
的运行(run)是一个有限长度的迁移序列
1
011
...
n
a
a
VV
nn
uu uu
−
⎯⎯→⎯⎯→ ,也可以写作
1
...
0
n
aa
V
n
uu⎯⎯⎯→ .用符
号
σ
=a
1
…a
n
表示迁移规则序列.
带状态的向量加法系统(vector addition system with states,简称 VA SS ) 可以表示为三元组 V=〈Q,d,T〉.Q
是有限的状态集合,d∈
表示 V 的维度,T⊆Q×
d
×Q 表示迁移规则集合.VASS 中,格局(configuration)指的是集合
Confs
V
=Q×
d
中的元素.VASS 中的一次迁移 (,) ( ,)
t
V
qu q v⎯⎯
′
→ 是满足 v=u+a 的三元组,其中,u,v∈
d
,t=(q,a, q′)∈T.
从格局 c
0
到格局 c
n
的一次运行是一个有限长度的迁移序列
1
011
...
n
t
t
VV
nn
cc cc
−
⎯⎯→⎯⎯→ ,也可以写作:
1
...
0
n
tt
V
n
cc⎯⎯⎯→ .
针对上面两个模型,Hopcroft 和 Pansiot 在 1979 年的工作
[10]
中证明了 n 维 VA S S 可以用 n+3 维 VA S 来表
达
,因此两者的可达性问题等价.
1.2 验证问题的形式化定义
本节具体给出 VA S 模型上几个著名验证问题的形式化定义.
可达性(reachability)问题.
输入:VAS V (VASS V),初始和结束向量 u,u′(格局 c,c′);
问题:是否存在一次从 u 到 u′(从 c 到 c′)的运行.
of 16
免费下载
【版权声明】本文为墨天轮用户原创内容，转载时必须标注文档的来源（墨天轮），文档链接，文档作者等基本信息，否则作者和墨天轮有权追究责任。如果您发现墨天轮中有涉嫌抄袭或者侵权的内容，欢迎发送邮件至：contact@modb.pro进行举报，并提供相关证据，一经查实，墨天轮将立刻删除相关内容。
下载排行榜
评论