Abstract
In [8], McMillan described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. The algorithm is based on Linear Programming. It compares favourably with other algorithms for the class of deterministic concurrent systems.
This work was partially supported by the Esprit Basic Research Action CALIBAN.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
E. Best and J. Esparza: Model Checking of Persistent Petri Nets. Computer Science Logic 91, LNCS 626, 35–52 (1991).
E. Best and C. Fernández: Nonsequential Processes — A Petri Net View. EATCS Monographs on Theoretical Computer Science Vol. 13 (1988).
J. Engelfriet: Branching processes of Petri nets. Acta Informatica Vol. 28, 575–591 (1991).
J. Esparza: Model Checking Using Net Unfoldings. Hildesheimer Informatikfachbericht 14/92 (October 1992).
P. Godefroid and P. Wolper: Using Partial Orders for the Eficient Verification of Deadlock Freedom and Safety Properties. Computer Aided Verification, LNCS 575, 332–343 (1991).
R. Howell and L. Rosier: On questions of fairness and temporal logic for conflictfree Petri nets. Advances in Petri Nets 1988, LNCS 340, 200–220, Springer, Berlin (1988).
G.E. Hughes and M.J. Creswell: An Introduction to Modal Logic. Methuen and Co. (1968).
K.L. McMillan: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. 4th Workshop on Computer Aided Verification, Montreal, 164–174 (1992).
M. Nielsen, G. Plotkin and G. Winskel: Petri Nets, Event Structures and Domains. Theor. Comp. Sci. Vol. 13, 1, pp. 85–108 (1980).
D. K. Probst and H.F. Li: Partial-Order Model Checking: A Guide for the Perplexed. Computer Aided Verification, LNCS 575, 322–332 (1991).
M. Tiusanen: Some Unsolved Problems in Modelling Self-Timed Circuits Using Petri Nets. EATCS Bulletin Vol. 36, 152–160 (1988).
A. Valmari: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, LNCS 483, 491–515 (1990).
H. Yen: A polynomial time algorithm to decide pairwise concurrency of transitions for 1-bounded conflict-free Petri nets. Inf. Proc. Lett. 38, 71–76 (1991).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Esparza, J. (1993). Model checking using net unfoldings. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_93
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_93
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive