Skip to main content
Log in

Deciding a class of path formulas for conflict-free petri nets

  • Published:
Theory of Computing Systems Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

The aim of this paper is to develop a unified approach for deriving complexity results for problems concerning conflict-free Petri nets. To do so, we first define a class of formulas for paths in Petri nets. We then show that answering the satisfiability problem for conflict-free Petri nets is tantamount to solving a system of linear inequalities (which is known to be in P). Since a wide spectrum of Petri net problems (including various fairness-related problems) can be reduced to the satisfiability problem in a straightforward manner, our approach offers an umbrella under which many Petri net problems for conflict-free Petri nets can be shown to be solvable in polynomial time. As a side-product, our analysis provides evidence as to why detecting unboundedness for conflict-free Petri nets is easier (provided P ≠ NP) than for normal and sinkless Petri nets (which are two classes that properly contain conflict-free Petri nets).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. P. Alimonti, E. Feuerstain, and U. Nanni, Linear time algorithms for liveness and boundedness in conflict-free Petri nets,Proc. 1992Latin American Symposium on Theoretical Informatics (LATIN ’92), Lecture Notes in Computer Science, Vol. 583, Springer-Verlag, Berlin, 1992, pp. 1–14.

    Google Scholar 

  2. H. Baker, Rabin’s Proof of the Undecidability of the Reachability Set Inclusion Problem of Vector Addition Systems, Memo 79, MIT Project MAC, Computer Structure Group, 1973.

  3. S. Crespi-Reghizzi and D. Mandrioli, A decidability theorem for a class of vector addition systems,Inform. Process. Lett.,3 (1975), 78–80.

    Article  MathSciNet  MATH  Google Scholar 

  4. J. Esparza, A solution to the covering problem for 1-bounded conflict-free Petri nets,Inform. Process. Lett.,41 (1992), 313–319.

    Article  MathSciNet  MATH  Google Scholar 

  5. M. Garey and D. Johnson,Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, California, 1979.

    MATH  Google Scholar 

  6. J. Grabowski, The decidability of persistence for vector addition systems,Inform. Process. Lett.,11 (1980), 20–23.

    Article  MathSciNet  MATH  Google Scholar 

  7. M. Hack, The equality problem for vector addition systems is undecidable,Theoret. Comput. Sci.,2 (1976), 77–95.

    Article  MathSciNet  MATH  Google Scholar 

  8. M. Heiner, Petri Net Based Software Validation Prospects and Limitations, TR-92-022, International Computer Science Institute, Berkeley, California, March, 1992.

    Google Scholar 

  9. J. Hopcroft and J. Pansiot, On the reachability problem for 5-dimensional vector addition systems,Theoret. Comput. Sci.,8 (1979), 135–159.

    Article  MathSciNet  MATH  Google Scholar 

  10. J. Hopcroft and J. Ullman,Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Massachusetts, 1979.

    MATH  Google Scholar 

  11. R. Howell and L. Rosier, Completeness results for conflict-free vector replacement systems,J. Comput. System Sci.,37 (1988), 349–366.

    Article  MathSciNet  MATH  Google Scholar 

  12. R. Howell and L. Rosier, On questions of fairness and temporal logic for conflict-free Petri nets, in G. Rozenberg, editor,Advances in Petri Nets 1988, Lecture Notes in Computer Science, Vol. 340, Springer-Verlag, Berlin, 1988, pp. 200–226.

    Google Scholar 

  13. R. Howell, L. Rosier, D. Huynh, and H. Yen, Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states,Theoret. Comput. Sci.,46 (1986), 107–140.

    Article  MathSciNet  MATH  Google Scholar 

  14. R. Howell, L. Rosier, and H. Yen, AnO(n 1.5) algorithm to decide boundedness for conflict-free vector replacement systems,Inform. Process. Lett.,25 (1987), 27–33.

    Article  MathSciNet  MATH  Google Scholar 

  15. R. Howell, L. Rosier, and H. Yen, A taxonomy of fairness and temporal logic problems for Petri nets,Theoret. Comput. Sci.,82 (1991), 341–372.

    Article  MathSciNet  MATH  Google Scholar 

  16. R. Howell, L. Rosier, and H. Yen, Normal and sinkless Petri nets,J. Comput. System Sci.,46 (1993), 1–26.

    Article  MathSciNet  MATH  Google Scholar 

  17. N. Jones, L. Landweber, and Y. Lien, Complexity of some problems in Petri nets,Theoret. Comput. Sci.,4 (1977), 277–299.

    Article  MathSciNet  MATH  Google Scholar 

  18. L. Khachian, A polynomial algorithm for linear programming,Dokl. Akad. Nauk USSR,244(5) (1979), 1093–96. Translated inSoviet Math. Dokl.,20 (1979), 191–94.

    Google Scholar 

  19. R. Kosaraju, Decidability of reachability in vector addition systems,Proc. 14th Annual ACM Symposium on Theory of Computing, 1982, pp. 267–280.

  20. L. Landweber and E. Robertson, Properties of conflict-free and persistent Petri nets,J. Assoc. Comput. Mach.,25 (1978), 352–364.

    Article  MathSciNet  MATH  Google Scholar 

  21. R. Lipton, The Reachability Problem Requires Exponential Space, Technical Report 62, Dept. of Computer Science, Yale University, Jan. 1976.

  22. E. Mayr, An algorithm for the general Petri net reachability problem,SIAM J. Comput.,13 (1984), 441–460.

    Article  MathSciNet  MATH  Google Scholar 

  23. T. Murata, Petri nets: properties, analysis and applications,Proc. IEEE,77 (1989), 541–580.

    Article  Google Scholar 

  24. J. Peterson,Petri Net Theory and the Modeling of Systems, Prentice-Hall, Englewood Cliffs, New Jersey, 1981.

    Google Scholar 

  25. C. Rackoff, The covering and boundedness problems for vector addition systems,Theoret. Comput. Sci.,6 (1978), 223–231.

    Article  MathSciNet  MATH  Google Scholar 

  26. W. Reisig,Petri Nets: An Introduction, Springer-Verlag, Heidelberg, 1985.

    MATH  Google Scholar 

  27. M. Silva and T. Murata, B-fairness and structural B-fairness in Petri net models of concurrent systems,J. Comput. System Sci.,44 (1992), 447–477.

    Article  MathSciNet  MATH  Google Scholar 

  28. L. Stockmeyer, The polynomial-time hierarchy,Theoret. Comput. Sci.,3 (1977), 1–22.

    Article  MathSciNet  MATH  Google Scholar 

  29. I. Suzuki and T. Kasami, Three measures for synchronic dependence in Petri nets,Acta Inform.,19 (1983), 325–338.

    Article  MathSciNet  MATH  Google Scholar 

  30. R. Valk and M. Jantzen, The residue of vector sets with applications to decidability problems in Petri nets,Acta Inform.,21 (1985), 643–674.

    Article  MathSciNet  MATH  Google Scholar 

  31. H. Yamasaki, Normal Petri nets,Theoret. Comput. Sci.,31 (1984), 307–315.

    Article  MathSciNet  MATH  Google Scholar 

  32. H. Yen, A polynomial time algorithm to decide pairwise concurrency of transitions for 1-bounded conflict-free Petri nets,Inform. Process. Lett.,38 (1991), 71–76.

    Article  MathSciNet  MATH  Google Scholar 

  33. H. Yen, A unified approach for deciding the existence of certain Petri net paths,Inform. and Comput.,96 (1992), 119–137.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Additional information

A preliminary version was presented at the 14th International Conference on Application and Theory of Petri Nets, Chicago, IL, USA, June 1993.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Yen, HC., Wang, BY. & Yang, MS. Deciding a class of path formulas for conflict-free petri nets. Theory of Computing Systems 30, 475–494 (1997). https://doi.org/10.1007/BF02679458

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02679458

Keywords

Navigation