In [3], 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.
CITATION STYLE
Esparza, J. (1993). Model checking using net unfoldings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 668 LNCS, pp. 613–628). Springer Verlag. https://doi.org/10.1007/3-540-56610-4_93
Mendeley helps you to discover research relevant for your work.