摘要: The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. semidecision method, and it may fail give an answer for some systems, particular those communicating means of shared variables. In this paper, we complement so called trap equation. We show that both together significantly extend range verifiable systems conducting several case studies.
core.ac.uk
springer.com
sci-hub.st 参考文章(18)
Enric Pastor, Oriol Roig, Jordi Cortadella, Rosa M. Badia, Petri Net Analysis Using Boolean Manipulation applications and theory of petri nets. pp. 416- 435 ,(1994) , 10.1007/3-540-58152-9_23
André Arnold, Verification and Comparison of Transition Systems colloquium on trees in algebra and programming. pp. 121- 135 ,(1993) , 10.1007/3-540-56610-4_60
Stephan Kleuker, A Gentle Introduction to Specification Engineering Using a Case Study in Telecommunications colloquium on trees in algebra and programming. pp. 636- 650 ,(1995) , 10.1007/3-540-59293-8_225
J. Ezpeleta, J. M. Couvreur, M. Silva, A New Technique for Finding a Generating Family of Siphons, Traps and st-Components. Application to Colored Petri Nets applications and theory of petri nets. pp. 126- 147 ,(1991) , 10.1007/3-540-56689-9_42
M. Raynal, D. Beeson, Algorithms for mutual exclusion ,(1986)
George S. Avrunin, Ugo A. Buy, James C. Corbett, Integer Programming in the Analysis of Concurrent Systems computer aided verification. ,vol. 575, pp. 92- 102 ,(1991) , 10.1007/3-540-55179-4_10
Alexander Schrijver, Theory of Linear and Integer Programming ,(1986)
T. Murata, Petri nets: Properties, analysis and applications Proceedings of the IEEE. ,vol. 77, pp. 541- 580 ,(1989) , 10.1109/5.24143
Javier Esparza, Manuel Silva, A polynomial-time algorithm to decide liveness of bounded free choice nets Theoretical Computer Science. ,vol. 102, pp. 185- 205 ,(1992) , 10.1016/0304-3975(92)90299-U
James C. Corbett, George S. Avrunin, Using integer programming to verify general safety and liveness properties computer aided verification. ,vol. 6, pp. 97- 123 ,(1995) , 10.1007/BF01384316