Shortest paths in reachability graphs

  • Jörg Desel
  • Javier Esparza
Full Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 691)


We prove the following property for safe conflict-free Petri nets and live and safe extended free-choice Petri nets:

Given two markings M 1 , M 2 of the reachability graph, if some path leads from M1 to M2, then some path of polynomial length in the number of transitions of the net leads from M1 to M2.


Short Path Induction Hypothesis Model Checker Safe System Maximal Transition 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    T. van Aardenne-Ehrenfest and N.G. de Bruijn: Circuits and Trees in Oriented Linear Graphs, Simon Stevin 28, 203–217 (1951).Google Scholar
  2. [2]
    E. Best and J. Desel: Partial Order Behaviour and Structure of Petri Nets. Formal Aspects of Computing Vol. 2 No.2, 123–138 (1990).Google Scholar
  3. [3]
    E. Best and J. Esparza: Model Checking of Persistent Petri Nets. Computer Science Logic 91, E. Börger, G. Jäger, H. Kleine Büning and M.M. Richter (eds.), LNCS 626, 35–53 (1992).Google Scholar
  4. [4]
    E. Best and P.S. Thiagarajan: Some Classes of Live and Save Petri Nets. Concurrency, K. and Nets K., Voss H.J., Genrich G., Rozenberg G. (eds.), Advances in Petri Nets. — Berlin: Springer-Verlag, 71–94 (1987).Google Scholar
  5. [5]
    E. Best and K. Voss: Free Choice Systems have Home States. Acta Informatica 21, 89–100 (1984).Google Scholar
  6. [6]
    F. Commoner, A.W. Holt, S. Even and A. Pnueli: Marked Directed Graphs. Journal of Computer and System Science Vol. 5, 511–523 (1971).Google Scholar
  7. [7]
    J. Esparza: Model Checking Using net Unfoldings. Hildesheimer Informatik Fachbericht 14/92 (October 1992). To appear in the Proceedings of TAPSOFT'93.Google Scholar
  8. [8]
    H. Fleischner: Eulerian Graphs and Related Topics, Part 1, Volume 1. Annals of Discrete Mathematics Vol.45. North-Holland (1990).Google Scholar
  9. [9]
    H.J. Genrich and K. Lautenbach: Synchronisationsgraphen. Acta Informatica Vol. 2, 143–161 (1973).Google Scholar
  10. [10]
    M. Hack: Analysis of Production Schemata by Petri Nets. TR-94, MIT-MAC (1972). Corrections (1974).Google Scholar
  11. [11]
    R. Howell and L. Rosier: On questions of fairness and temporal logic for conflict-free Petri nets. Advances in Petri Nets 1988, G. Rozenberg (ed.), LNCS 340, 200–226 (1988).Google Scholar
  12. [12]
    L. Landweber and E. Robertson: Properties of Conflict-Free and Persistent Petri Nets. JACM, Vol. 25, No.3, 352–364 (1978).Google Scholar
  13. [13]
    K.L. McMillan: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. Proceedings of the 4th Workshop on Computer Aided Verification, Montreal, pp. 164–174 (1992).Google Scholar
  14. [14]
    P.S. Thiagarajan and K. Voss: A Fresh look at free-choice Nets. Information and Control, Vol. 61, No. 2, 85–113 (1984).Google Scholar
  15. [15]
    H. Yen: A polynomial time algorithm to decide pairwise concurrency of transitions for 1-bounded conflict-free Petri nets. Information Processing Letters 38, 71–76 (1991).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Jörg Desel
    • 1
  • Javier Esparza
    • 2
  1. 1.Institut für InformatikTechnische Universität MünchenMünchen 2
  2. 2.Institut für InformatikUniversität HildesheimHildesheim

Personalised recommendations