微信服务号

微信订阅号

2025年3月26日 4:23 星期三
首页 > 过刊浏览>2018年第29卷第6期 >1566-1581. DOI:10.13328/j.cnki.jos.005465
PDF HTML阅读 XML下载 导出引用 引用提醒
向量加法系统验证问题研究综述
作者:
作者简介:

张文博(1992-),男,河南洛阳人,学士,主要研究领域为理论计算机科学;龙环(1980-),女,博士,副教授,博士生导师,主要研究领域为理论计算机科学.

通讯作者:

龙环,E-mail:longhuan@sjtu.edu.cn

基金项目:

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


State-of-the-Art Survey on Verification of Vector Addition Systems
Author:
Fund Project:

National Natural Science Foundation of China (61472239, 61772336, 61572318)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [55]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    [1] Petri CA. Kommunikation mit Automaten. Bonn:Institut fur Instrumentelle Mathematik, Schriften des ⅡM Nr. 2, 1962.
    [2] Ball T, Chaki S, Rajamani S. Parameterized verification of multithreaded software libraries. In:Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2031, Springer-Verlag, 2001. 158-173.[doi:10.1007/3-540-45319-9_12]
    [3] van der Aalst W. The application of Petri nets to workflow management. Journal of Circuits, Systems, and Computers, 1998,8(1):21-66.[doi:10.1142/S0218126698000043]
    [4] Heiner M, Gilbert D, Donaldson R. Petri nets for systems and synthetic biology. In:Proc. of the Formal Methods for Computational Systems Biology. 2008. 215-264.[doi:10.1007/978-3-540-68894-5_7]
    [5] Lei L, Lin C, Zhong ZD. Stochastic Petri nets for wireless networks. In:Springer Briefs in Electrical and Computer Engineering, Springer-Verlag, 2015. 1-101.[doi:10.1007/978-3-319-16883-8]
    [6] Fan LJ, Wang YZ, Li JY, Cheng XQ, Lin C. Privacy Petri net and privacy leak software. Journal of Computer Science and Technology, 2015,30(6):1318-1343.[doi:10.1007/s11390-015-1601-7]
    [7] Yu WY, Yan CG, Ding ZJ, Jiang CJ, Zhou MC. Modeling and validating E-commerce business process based on Petri nets. IEEE Trans. on Systems, Man, and Cybernetics:Systems, 2014,44(3):327-341.[doi:10.1109/TSMC.2013.2248358]
    [8] 林闯.随机Petri网和系统性能评价.北京:清华大学出版社,2005.
    [9] Jiang YX, Lin C, Qu Y, Yin H. Research on Model-Checking Based on Petri Nets. Ruan Jian Xue Bao/Journal of Software, 2004,15(9):1265-1276(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/15/1265.htm
    [10] Hopcroft J, Pansiot JJ. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 1979, 8(2):135-159.[doi:10.1016/0304-3975(79)90041-0]
    [11] Lipton RJ. The reachability problem is exponential-space-hard. Technical Report, 62, Department of Computer Science, Yale University, 1976.
    [12] Rackoff C. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 1978,6:223-231.[doi:10.1016/0304-3975(78)90036-1]
    [13] Rosier L, Yen HC. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences, 1986,32:105-135.[doi:10.1016/0022-0000(86)90006-1]
    [14] Sacerdote GS, Tenney RL. The decidability of the reachability problem for vector addition systems (preliminary version). In:Proc. of the 9th Annual ACM Symp. on Theory of Computing. ACM Press, 1977. 61-76.[doi:10.1145/800105.803396]
    [15] Mayr EW. An algorithm for the general Petri net reachability problem. In:Proc. of the STOC'81. ACM Press, 1981. 238-246.[doi:10.1145/800076.802477]
    [16] Kosaraju SR. Decidability of reachability in vector addition systems. In:Proc. of the STOC'82. ACM Press, 1982. 267-281.[doi:10.1145/800070.802201]
    [17] Lambert JL. A structure to decide reachability in Petri nets. Theoretical Computer Science, 1992,99(1):79-104.[doi:10.1016/0304-3975(92)90173-D]
    [18] Leroux J. The general vector addition system reachability problem by presburger inductive invariants. In:Proc. of the 24th IEEE Symp. on Logic in Computer Science (LICS 2009). 2009.[doi:10.1109/LICS.2009.10]
    [19] Leroux J. Vector addition system reachability problem (a short self-contained proof). In:Proc. of the Principles of Programming Languages. Austin:ACM Press, 2011. 307-316.[doi:10.1145/1926385.1926421]
    [20] Leroux J. Vector addition systems reachability problem (a simpler solution). In:Voronkov A, ed. Proc. of the Alan Turing Centenary Conf. (Turing-100). 2012.
    [21] Leroux J, Schmitz S. Demystifying reachability in vector addition systems. In:Proc. of the 30th IEEE Symp. on Logic in Computer Science (LICS 2015). 2015. 56-67.[doi:10.1109/LICS.2015.16]
    [22] Karp RM, Miller RE. Parallel program schemata. Journal of Computer and System Sciences, 1969,3(2):147-195.[doi:10:1016/S0022-0000(69) 80011-5] [doi:10.1016/S0022-0000(69)80011-5]
    [23] Muller H. The reachability problem for VAS. In:Proc. of the Advances in Petri Nets 1984. NCS 188. Springer-Verlag, 1985. 376-391.
    [24] Dershowitz N, Manna Z. Proving termination with multiset orderings. Communications of the ACM, 1979,22(8):465-476.[doi:10:1145/359138:359142] [doi:10.1145/359138.359142]
    [25] Figueira D, Figueira S, Schmitz S, Schnoebelen P. Ackermannian and primitive-recursive bounds with Dickson's Lemma. In:Proc. of the LICS 2011. IEEE Press, 2011.[doi:10:1109/LICS:2011:39]
    [26] Schmitz S. Complexity hierarchies beyond Elementary. ACM Trans. on Computation Theory, 2015. http://arxiv:org/abs/1312:5686[doi:10.1145/2858784]
    [27] Ginsburg S, Spanier EH. Semigroups, presburger formulas and languages. Pacific Journal of Mathematics, 1966,16(2):285-296.[doi:10.2140/pjm.1966.16.285]
    [28] Lazic R. The reachability problem for vector addition systems with a stack is not elementary. 2013. https://arxiv.org/pdf/1310.1767.pdf
    [29] Haase C, Kreutzer S, Ouaknine J, Worrell J. Reachability in succinct and parametric one-counter automata. In:Proc. of the Concurrency Theory (CONCUR 2009). 2009. 369-383.[doi:10.1007/978-3-642-04081-8_25]
    [30] Haase C. On the complexity of model checking counter automata[Ph.D. Thesis]. University of Oxford, 2012.
    [31] Howell RR, Rosier LE, Huynh DT, Yen HC. Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states. Theoretical Computer Science, 1986,46(3):107-140.[doi:10.1016/0304-3975(86)90026-5]
    [32] Fearnley J, Jurdzinski M. Reachability in two-clock timed automata is PSPACE-complete. In:Proc. of the 40th Int'l Colloquium on Automata, Languages, and Programming (ICALP), Vol.2. 2013. 212-223.[doi:10.1007/978-3-642-39212-2_21]
    [33] Blondin M, Finkel A, Göller S, Haase C, McKenzie P. Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In:Proc. of the 30th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS 2015). 2015. 32-43.[doi:10.1109/LICS.2015.14]
    [34] Leroux J, Sutre G. On flatness for 2-dimensional vector addition systems with states. In:Proc. of the CONCUR 2004-15th Int'l Conf. on Concurrency Theory. 2004. 402-416.[doi:10.1007/978-3-540-28644-8_26]
    [35] Englert M, Lazic P, Totzke P. Reachability in two-dimensional unary vector addition systems with states is NL-complete. In:Proc. of the LICS 2016. 2016. 477-484.[doi:10.1145/2933575.2933577]
    [36] Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Trans. on Programming Languages and Systems, 2012,34(1):6:1-6:48.[doi:10.1145/2160910.2160915]
    [37] Leroux J, Praveen M, Sutre G. Hyper-Ackermannian bounds for pushdown vector addition systems. In:Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS) (CSL-LICS 2014). 2014.[doi:10.1145/2603088.2603146]
    [38] Leroux J, Sutre G, Totzke P. On the coverability problem for pushdown vector addition systems in one dimension. In:Proc. of the ICALP, Vol.2. 2015. 324-336.[doi:10.1007/978-3-662-47666-6_26]
    [39] Finkel A, Leroux J. Recent and simple algorithms for Petri nets. Software and System Modeling, 2015,14(2):719-725.[doi:10. 1007/s10270-014-0426-0]
    [40] Leroux J, Sutre G, Totzke P. On boundedness problems for pushdown vector addition systems. In:Proc. of the RP. 2015. 101-113.[doi:10.1007/978-3-319-24537-9_10]
    [41] Lincoln P, Mitchell J, Scedrov A, Shankar N. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 1992,56(1-3):239-311.[doi:10.1016/0168-0072(92)90075-B]
    [42] Courtois JB, Schmitz S. Alternating vector addition systems with states. In:Proc. of the MFCS, Vol.1. 2014. 220-231.[doi:10.1007/978-3-662-44522-8_19]
    [43] Verma KN, Goubault-Larrecq J. Karp-Miller trees for a branching extension of VASS, discr. Mathematics & Theoretical Computer Science, 2005,7:217-230.
    [44] Lazic R. The reachability problem for branching vector addition systems requires doubly-exponential space. Information Processing Letters, 2010,110(17):740-745.[doi:10.1016/j.ipl.2010.06.008]
    [45] Demri S, Jurdzinski M, Lachish O, Lazic R. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 2013,79(1):23-38.[doi:10.1016/j.jcss.2012.04.002]
    [46] Lazic R, Schmitz S. Non-Elementary complexities for branching VASS, MELL, and extensions. In:Proc. of the CSL/LICS. 2014.[doi:10.1145/2603088.2603129]
    [47] Lazic R, Schmitz S. Non-Elementary complexities for branching VASS, MELL, and extensions. ACM Trans. on Computational Logic, 2015,16(3):1-30.[doi:10.1145/2733375]
    [48] Göller S, Haase C, Lazic R, Totzke P. A polynomial-time algorithm for reachability in branching VASS in dimension one. 2016, 105:1-13. https://arxiv.org/abs/1602.05547
    [49] Lazic R, Newcomb T, Ouaknine J, Roscoe A, Worrell J. Nets with tokens which carry data. Fund Information, 2008,88(3):251-274.[doi:10.1007/978-3-540-73094-1_19]
    [50] Haddad S, Schmitz S, Schnoebelen P. The ordinal recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In:Proc. of the LICS. IEEE Press, 2012. 355-364.[doi:10.1109/LICS.2012.46]
    [51] Rosa-Velardo F. Ordinal recursive complexity of unordered data nets. Technical Report, TR-4-14, Departamento de Sistemas Informaticosy Computacion, Universidad Complutense de Madrid, 2014.
    [52] Hofman P, Lasota S, Lazić R, Leroux J, Schmitz S, Totzke P. Coverability trees for Petri nets with unordered data. In:Proc. of the 19th Int'l Conf. on Foundations of Software Science and Computation Structures (FoSSaCS). 2016.[doi:10.1007/978-3-662-49630-5_26]
    [53] Lazic R, Totzke P. What makes Petri nets harder to verify:Stack or data? In:Proc. of the Concurrency, Security, and Puzzles 2017. 2017. 144-161.[doi:10.1007/978-3-319-51046-0_8]
    附中文参考文献:
    [9] 蒋屹新,林闯,曲扬,尹浩.基于Petri网的模型检测研究.软件学报,2004,15(9):1265-1276. http://www.jos.org.cn/1000-9825/15/1265.htm
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

张文博,龙环.向量加法系统验证问题研究综述.软件学报,2018,29(6):1566-1581

复制
分享
文章指标
  • 点击次数:3671
  • 下载次数: 5521
  • HTML阅读次数: 3371
  • 引用次数: 0
历史
  • 收稿日期:2017-07-01
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19732522位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号