微信服务号

微信订阅号

2025年4月7日 0:14 星期一
首页 > 过刊浏览>2020年第31卷第8期 >2388-2403. DOI:10.13328/j.cnki.jos.005959
PDF HTML阅读 XML下载 导出引用 引用提醒
基本并行进程活性的限界模型检测
作者:
作者简介:

谭锦豪(1996-),男,硕士生,CCF学生会员,主要研究领域为形式化验证,程序语言理论;李国强(1979-),男,博士,副教授,CCF高级会员,主要研究领域为形式化方法,程序语言理论,知识表示与推理.

通讯作者:

李国强,E-mail:li.g@sjtu.edu.cn

基金项目:

国家自然科学基金（61872232，61732013）


Bounded Model Checking Liveness on Basic Parallel Processes
Author:
Fund Project:

National Natural Science Foundation of China (61872232, 61732013)

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

    基本并行进程是一个用于描述和分析并发程序的模型，是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑，其中的AF算子表示从当前的状态出发性质最终会被满足，因此EG逻辑是能够表达活性的逻辑.然而，基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此，提出了基本并行进程上EG逻辑的限界模型检测方法.首先给出了基本并行进程上EG逻辑的限界语义，然后采用基于约束的方法，将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题，最后利用SMT求解器进行求解.

    Abstract:

    Basic parallel process (BPP) is a model for describing and analyzing concurrent programs, which is an important subclass of Petri nets. The logic EG is a branching time logic obtained by extending Hennessy-Milner Logic with the EG operator, in which the AF operator means that a certain property will be satisfied eventually from the current state. Hence, the logic EG is a logic that can express liveness. However, model checking the logic EG over BPP is undecidable. This study proposes an algorithm for the problem of bounded model checking EG over BPP. First, a bounded semantics of EG over BPP is proposed. Then, according to the constraint-based approach, a reduction from the problem of bounded model checking EG over BPP to the satisfiability problem of linear integer arithmetic formulas is given. Finally, the linear integer arithmetic formulas are solved by SMT solvers.

    参考文献
    [1] Kaiser A, Kroening D, Wahl T. Dynamic cutoff detection in parameterizedconcurrent programs. In:Proc. of the 22nd Int'l Conf. on Computer Aided Verification, Vol.6174. Berlin:Springer-Verlag, 2010. 645-659.
    [2] D'Osualdo E, Kochems J, Ong CHL. Automatic verification of Erlang-styleconcurrency. In:Proc. of the 20th Int'l Symp. on Static Analysis, Vol.7935. Berlin:Springer-Verlag, 2013. 454-476.
    [3] Kaiser A, Kroening D, Wahl T. Efficient coverability analysis by proof minimization. In:Proc. of the 23rd Int'l Conf. on Concurrency Theory, Vol.7454. Berlin:Springer-Verlag, 2012. 500-515.
    [4] Bouajjani A, Emmi M. Bounded phase analysis of message-passing programs. In:Proc. of the 18th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Vol.7214. Berlin:Springer-Verlag, 2012. 451-465.
    [5] Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Trans. on Programming Languages and Systems, 2012,34(1):Article No.6.
    [6] Petri CA. Communication with automata[Ph.D. Thesis]. Technische Universitat Darmstadt, 1962.
    [7] Vardi MY. Verification of concurrent programs:The automata-theoretic framework. Annals of Pure and Applied Logic, 1991,51:79-98.
    [8] Ganty P, Majumdar R, Rybalchenko A. Verifying liveness for asynchronous programs. In:Proc. of the 36th Symp. on Principles of Programming Languages. New York:ACM, 2009. 102-113.
    [9] Czerwinski W, Lasota S, Lazic R, Leroux J, Mazowiecki F. The reachability problem for Petri nets is not elementary. In:Proc. of the 51st Annual Symp. on Theory of Computing. New York:ACM, 2019. 24-33.
    [10] Christensen S. Decidability and decomposition in process algebras[Ph.D. Thesis]. Edinburgh:The University of Edinburgh, 1993.
    [11] Esparza J. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 1997,31:13-25.
    [12] Esparza J. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 1997,34(2):85-107.
    [13] Fu H. Model checking EGF on basic parallel processes. In:Proc. of the 9th Int'l Symp. on Automated Technology for Verification and Analysis. Berlin:Springer-Verlag, 2011. 120-134.
    [14] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories:From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL (T). Journal of the ACM, 2006,53(6):937-977.
    [15] Dutertre B. Yices 2.2. In:Proc. of the Int'l Conf. on Computer Aided Verification, Vol.8559. Berlin:Springer-Verlag, 2014. 737-744.
    [16] De Moura L, Bjorner N. Z3:An efficient SMT solver. In:Proc. of the 14th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2008. 337-340.
    [17] Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C. CVC4. In:Proc. of the 23rd Int'l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2011. 171-177.
    [18] Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R. The MathSAT5 SMT solver. In:Proc. of the 19th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2013. 93-107.
    [19] Minsky M. Computation:Finite and Infinite Machines. Prentice Hall, 1967.
    [20] Esparza J. On the decidability of model checking for several mu-calculi and Petri nets. In:Proc. of the Trees in Algebra and Programming (CAAP'94). Berlin:Springer-Verlag, 1994. 115-129.
    [21] Mayr R. Weak bisimulation and model checking for basic parallel processes. In:Proc. of the 16th Conf. on Foundations of Software Technology and Theoretical Computer Science, Vol.1180. Berlin:Springer-Verlag, 1996. 88-99.
    [22] To AW, Libkin L. Recurrent reachability analysis in regular model checking. In:Proc. of the 15th Int'l Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, Vol.5330. Berlin:Springer-Verlag, 2008. 198-213.
    [23] Strehl K, Thiele L. Interval diagram techniques for symbolic model checking of Petri nets. In:Proc. of the 1999 Design, Automation and Test in Europe. Berlin:Springer-Verlag, 1999. 756-757.
    [24] Mayr E. An algorithm for the general Petri net reachability problem. In:Proc. of the 13th Annual Symp. on Theory of Computing. New York:ACM, 1981. 238-246.
    [25] Lipton R. The reachability problem requires exponential-space hard. Technical Report, 62, Department of Computer Science, Yale University, 1976.
    [26] Leroux J, Schmitz S. Reachability in vector addition systems is primitive-recursive in fixed dimension. In:Proc. of the 34th Annual Symp. on Logic in Computer Science. IEEE, 2019. 1-13.
    [27] Karp RM, Miller RE. Parallel program schemata. Journal of Computer and System Sciences, 1969,3(2):147-195.
    [28] Rackoff C. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 1978,6(2):223-231.
    [29] Kloos J, Majumdar R, Niksic F, et al. Incremental, inductive coverability. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2013. 158-173.
    [30] Esparza J, Ledesma-Garza R, Majumdar R, et al. An SMT-based approach to coverability analysis. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2014. 603-619.
    [31] Ding RJ, Li GQ. Efficient implementation of coverability verification on communication-free Petri net. Ruan JianXue Bao/Journal of Software, 2019,30(7):1939-1952(in Chinese with English abstract). http.//www.jos.org.cn/1000-9825/5750.htm[doi:10.13328/j. cnki.jos.005750]
    [32] Biere A, Cimatti A, Clarke EM, Zhu YS. Symbolic model checking without BDDs. In:Proc. of the Tools and Algorithms for Construction and Analysis of Systems, Vol.1579. Berlin:Springer-Verlag, 1999. 193-207.
    [33] Penczek W, Wozna B, Zbrzezny A. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 2002, 51(1-2):135-156.
    [34] Zhang WH. Bounded semantics. Theoretical Computer Science, 2015,564:1-29.
    [35] Meski A, Pólrola A, Penczek W, Wozna-Szczesniak B, Zbrzezny A. Bounded model checking approaches for verification of distributed time Petri nets. In:Proc. of the Int'l Workshop on Petri Nets and Software Engineering, Vol.723. CEUR-WS.org, 2011. 72-91.
    [36] Schüle T, Schneider K. Bounded model checking of infinite state systems. Formal Methods in System Design, 2007,30(1):51-81.
    附中文参考文献:
    [31] 丁如江,李国强.非交互式Petri网可覆盖性验证的高效实现.软件学报,2019,30(7):1939-1952. http.//www.jos.org.cn/1000-9825/5750.htm[doi:10.13328/j.cnki.jos.005750]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

谭锦豪,李国强.基本并行进程活性的限界模型检测.软件学报,2020,31(8):2388-2403

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

京公网安备 11040202500063号