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).
Similar content being viewed by others
References
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.
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.
S. Crespi-Reghizzi and D. Mandrioli, A decidability theorem for a class of vector addition systems,Inform. Process. Lett.,3 (1975), 78–80.
J. Esparza, A solution to the covering problem for 1-bounded conflict-free Petri nets,Inform. Process. Lett.,41 (1992), 313–319.
M. Garey and D. Johnson,Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, California, 1979.
J. Grabowski, The decidability of persistence for vector addition systems,Inform. Process. Lett.,11 (1980), 20–23.
M. Hack, The equality problem for vector addition systems is undecidable,Theoret. Comput. Sci.,2 (1976), 77–95.
M. Heiner, Petri Net Based Software Validation Prospects and Limitations, TR-92-022, International Computer Science Institute, Berkeley, California, March, 1992.
J. Hopcroft and J. Pansiot, On the reachability problem for 5-dimensional vector addition systems,Theoret. Comput. Sci.,8 (1979), 135–159.
J. Hopcroft and J. Ullman,Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Massachusetts, 1979.
R. Howell and L. Rosier, Completeness results for conflict-free vector replacement systems,J. Comput. System Sci.,37 (1988), 349–366.
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.
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.
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.
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.
R. Howell, L. Rosier, and H. Yen, Normal and sinkless Petri nets,J. Comput. System Sci.,46 (1993), 1–26.
N. Jones, L. Landweber, and Y. Lien, Complexity of some problems in Petri nets,Theoret. Comput. Sci.,4 (1977), 277–299.
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.
R. Kosaraju, Decidability of reachability in vector addition systems,Proc. 14th Annual ACM Symposium on Theory of Computing, 1982, pp. 267–280.
L. Landweber and E. Robertson, Properties of conflict-free and persistent Petri nets,J. Assoc. Comput. Mach.,25 (1978), 352–364.
R. Lipton, The Reachability Problem Requires Exponential Space, Technical Report 62, Dept. of Computer Science, Yale University, Jan. 1976.
E. Mayr, An algorithm for the general Petri net reachability problem,SIAM J. Comput.,13 (1984), 441–460.
T. Murata, Petri nets: properties, analysis and applications,Proc. IEEE,77 (1989), 541–580.
J. Peterson,Petri Net Theory and the Modeling of Systems, Prentice-Hall, Englewood Cliffs, New Jersey, 1981.
C. Rackoff, The covering and boundedness problems for vector addition systems,Theoret. Comput. Sci.,6 (1978), 223–231.
W. Reisig,Petri Nets: An Introduction, Springer-Verlag, Heidelberg, 1985.
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.
L. Stockmeyer, The polynomial-time hierarchy,Theoret. Comput. Sci.,3 (1977), 1–22.
I. Suzuki and T. Kasami, Three measures for synchronic dependence in Petri nets,Acta Inform.,19 (1983), 325–338.
R. Valk and M. Jantzen, The residue of vector sets with applications to decidability problems in Petri nets,Acta Inform.,21 (1985), 643–674.
H. Yamasaki, Normal Petri nets,Theoret. Comput. Sci.,31 (1984), 307–315.
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.
H. Yen, A unified approach for deciding the existence of certain Petri net paths,Inform. and Comput.,96 (1992), 119–137.
Author information
Authors and Affiliations
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
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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF02679458