zbMATH — the first resource for mathematics

On Yen’s path logic for Petri nets. (English) Zbl 1230.68153
In a paper by H.-C. Yen [Inf. Comput. 96, No. 1, 119–137 (1992; Zbl 0753.68078)], a class of formulas for paths in Petri nets was defined. Yen presented a proof showing that satisfiability of these formulas is EXPSPACE-complete. This proof was based on a lemma which contains an error. The present paper shows that the satisfiability problem for this class of formulas is as hard as the reachability problem of Petri nets. Moreover, almost all of Yen’s results are salvaged by defining a fragment of this class, for which the satisfiability problem is EXPSPACE-complete by adapting Yen’s proof.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI
[1] Esparza Javier, Bulletin of the EATCS 52 pp 244–
[2] DOI: 10.1016/0304-3975(91)90228-T · Zbl 0728.68090 · doi:10.1016/0304-3975(91)90228-T
[3] DOI: 10.1016/0304-3975(92)90173-D · Zbl 0769.68104 · doi:10.1016/0304-3975(92)90173-D
[4] DOI: 10.1007/BF00289268 · Zbl 0454.68048 · doi:10.1007/BF00289268
[5] DOI: 10.1016/0304-3975(78)90036-1 · Zbl 0368.68054 · doi:10.1016/0304-3975(78)90036-1
[6] DOI: 10.1007/BF00290730 · Zbl 0504.68032 · doi:10.1007/BF00290730
[7] DOI: 10.1007/BF00289715 · Zbl 0545.68051 · doi:10.1007/BF00289715
[8] DOI: 10.1016/0022-0000(81)90067-2 · Zbl 0473.68057 · doi:10.1016/0022-0000(81)90067-2
[9] DOI: 10.1016/0890-5401(92)90059-O · Zbl 0753.68078 · doi:10.1016/0890-5401(92)90059-O
[10] Yen Hsu-Chun, Inf. Process. Lett. 56 pp 237– · Zbl 1022.68574 · doi:10.1016/0020-0190(95)00168-2
[11] DOI: 10.1006/inco.1996.0013 · Zbl 0853.68138 · doi:10.1006/inco.1996.0013
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.