Abstract
We study the complexity of several standard problems for 1-safe Petri nets and some of its subclasses. We prove that reachability, liveness, and deadlock are all PSPACE-complete for 1-safe nets. We also prove that deadlock is NP-complete for free-choice nets and for 1-safe free-choice nets. Finally, we prove that for arbitrary Petri nets, deadlock is equivalent to reachability and liveness.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Luca Bernardinello and Fiorella De Cindio. A survey of basic net models and modular net classes. In Advances in Petri Nets 1992, pages 304–351. Springer-Verlag (LNCS 609), 1992.
Eike Best, Raymond Devillers, and Jon G. Hall. The Box calculus: a new causal algebra with multi-label communication. In Advances in Petri Nets 1992, pages 21–69. Springer-Verlag (LNCS 609), 1992.
Eike Best and César Fernández. Nonsequential Processes — a Petri Net View. EATCS Monographs on Theoretical Computer Science Vol.13, 1988.
Eike Best and P.S. Thiagarajan. Some classes of live and save Petri nets. In K. Voss, H.J. Genrich, and G. Rozenberg, editors, Advances in Petri Nets, pages 71–94. Springer-Verlag, 1987.
Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Technical Report DAIMI PB-455, Computer Science Department, Aarhus University, September 1993.
Fred Commoner, Anatole W. Holt, S. Even, and Amir Pnueli. Marked directed graphs. Journal of Computer and System Sciences, 5:511–523, 1971.
Pierpaolo Degano, Rocco De Nicola, and Ugo Montanari. A distributed operational semantics for CCS based on C/E systems. Acta Informatica, 26:59–91, 1988.
Jörg Desel. A proof of the rank theorem. In Advances in Petri Nets 1992, pages 304–351. Springer-Verlag (LNCS 609), 1992.
Jörg Desel and Javier Esparza. Shortest paths in reachability graphs. In Proc. Application and Theory of Petri Nets, pages 224–241. Springer-Verlag (LNCS 691), 1993.
Javier Esparza. Model checking using net unfoldings. In Proc. TAPSOFT'93, pages 613–628. Springer-Verlag (LNCS 668), 1993.
Javier Esparza and Manuel Silva. A polynomial-time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992.
Michael R. Garey and David S. Johnson. Computers and Intractability. Freeman, 1979.
Hartmann J. Genrich and Kurt Lautenbach. Synchronisationsgraphen. Acta Informatica, 2:143–161, 1973.
Patrice Godefroid. Using partial orders to improve automatic verification methods. In Proc. CAV'90, 2nd Workshop on Computer-Aided Verification, pages 176–185. Springer-Verlag (LNCS 531), 1990.
Ursula Goltz. On representing CCS programs by finite Petri nets. In Proc. MFCS'88, Mathematical Foundations of Computer Science, pages 339–350. Springer-Verlag (LNCS 324), 1988.
Michel Hack. The recursive equivalence of the reachabilty problem and the liveness problem for Petri nets and vector addition systems. In Proc. 15th Annual Symposium on Switching and Automata Theory, pages 156–164, 1974.
Michel Hack. The equality problem for vector addition systems is undecidable. Theoretical Computer Science, 2:77–95, 1976.
John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley Publishing Company, 1979.
Rodney R. Howell and Louis E. Rosier. Completeness results for conflict-free vector replacement systems. Journal of Computer and System Sciences, 37:349–366, 1988.
Rodney R. Howell and Louis E. Rosier. Problems concerning fairness and temporal logic for conflict-free Petri nets. Theoretical Computer Science, 64(3):305–329, 1989.
Lalita Jategaonkar and Albert Meyer. Deciding true concurrency equivalences on finite safe nets. In Proc. ICALP'93, pages 519–531, 1993.
Neil D. Jones, Lawrence H. Landweber, and Y. Edmund Lien. Complexity of some problems in Petri nets. Theoretical Computer Science, 4:277–299, 1977.
Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976.
Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM Journal on Computing, 13:441–460, 1984.
Kenneth L. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. CAV'92, Fourth Workshop on Computer-Aided Verification, pages 164–174, 1992.
José Meseguer and Ugo Montanari. Petri nets are monoids. Information and Computation, 88:105–155, 1990.
Tadao Murata. Petri nets: Properties, analysis and applications. In Proc. of the IEEE, volume 77(4), pages 541–580, 1989.
Mogens Nielsen, Grzegorz Rozenberg, and P.S. Thiagarajan. Behavioural notions for elementary net systems. Distributed Computing, 4(1):45–57, 1990.
Ernst R. Olderog. Nets, Terms and Formulas. Cambridge University Press, 1991. Number 23 Tracts in Theoretical Computer Science.
Wolfgang Reisig. Petri Nets — An Introduction. EATCS Monographs in Computer Science Vol.4, 1985.
Iain A. Stewart. On the reachability problem for some classes of Petri nets. Research Report, University of Newcastle upon Tyne, 1992.
P.S. Thiagarajan. Elementary net systems. In Advances in Petri Nets 1986, part I, pages 26–59. Springer-Verlag (LNCS 254), 1987.
Antti Valmari. Stubborn sets for reduced state space generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990, pages 491–515. Springer-Verlag (LNCS 483), 1990.
Glynn Winskel. Petri nets, algebras, morphisms and compositionality. Information and Computation, 72(3):197–238, 1987.
Glynn Winskel and Mogens Nielsen. Models for concurrency. Technical Report DAIMI PB-429, Computer Science Department, Aarhus University, November 1992. To appear as a chapter in the Handbook of Logic and the Foundations of Computer Science, Oxford University Press.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cheng, A., Esparza, J., Palsberg, J. (1993). Complexity results for 1-safe nets. In: Shyamasundar, R.K. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1993. Lecture Notes in Computer Science, vol 761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57529-4_66
Download citation
DOI: https://doi.org/10.1007/3-540-57529-4_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57529-0
Online ISBN: 978-3-540-48211-6
eBook Packages: Springer Book Archive