Deadlock checking using net unfoldings

  • Stephan Melzer
  • Stefan Römer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


McMillan presented a deadlock detection technique based on unfoldings of Petri net systems. It is realized by means of a backtracking algorithm that has its drawback for unfoldings that increase widely. We present an approach that exploits precisely this property. Moreover, we introduce a fast implementation of McMillan's algorithm and compare it with our new technique.


Transitive Closure Deadlock Detection Reachable Marking Finite Configuration Finite Prefix 
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.


  1. 1.
    E. Best and C. Fernández: Nonsequential Processes — A Petri Net View. EATCS Monographs on Theoretical Computer Science 13 (1988).Google Scholar
  2. 2.
    CPLEX 3.0 Manual, CPLEX Corp. (1995).Google Scholar
  3. 3.
    James C. Corbett: Evaluating Deadlock Detection Methods. University of Hawaii at Manoa (1994).Google Scholar
  4. 4.
    J. Engelfriet: Branching processes of Petri nets. Acta Informatica 28, pp. 575–591 (1991).Google Scholar
  5. 5.
    J. Esparza, S. Römer and W. Vogler: An Improvement of McMillan's Unfolding Algorithm. Proc. of Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1055, 87–106 (1996).Google Scholar
  6. 6.
    H. Hellwagner: Scalable Readers/Writers Synchronization on Shared-Memory Machines, Esprit P5404 (GP MIMD), Working Paper (1993).Google Scholar
  7. 7.
    A.J. Martin: The Design of a self-timed Circuit of Distributed Mutual Exclusion. In Henry Fuchs, editor, 1985 Chapel Hill Confernce on VLSI, pp. 245–260. Computer Science Press (1985).Google Scholar
  8. 8.
    K.L. McMillan: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. Proc. 4th Workshop on Computer Aided Verification, LNCS 663, 164–174 (1992).Google Scholar
  9. 9.
    S. Melzer and J. Esparza: Checking System Properties via Integer Programming. In Proc. of European Symp. on Programming, LNCS 1058, 250–264 (1996).Google Scholar
  10. 10.
    T. Murata: Petri nets: Properties, Analysis and Applications. In Proc. of the IEEE 77(4), pp. 541–580 (1989).Google Scholar
  11. 11.
    M. Nielsen, G. Plotkin and G. Winskel: Petri Nets, Event Structures and Domains. Theoretical Computer Science 13(1), pp. 85–108 (1980).Google Scholar
  12. 12.
    S. Römer: Implementation of a Compositional Partial Order Semantics of Petri Boxes. Diploma Thesis (in German). Universität Hildesheim (1993).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Stephan Melzer
    • 1
  • Stefan Römer
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenGermany

Personalised recommendations