×

zbMATH — the first resource for mathematics

On Yen’s path logic for Petri nets. (English) Zbl 1260.68255
Bournez, Olivier (ed.) et al., Reachability problems. 3rd international workshop, RP 2009, Palaiseau, France, September 23–25, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04419-9/pbk). Lecture Notes in Computer Science 5797, 51-63 (2009).
Summary: In [Inf. Comput. 96, No. 1, 119–137 (1992; Zbl 0753.68078)], H.-C. Yen defines a class of formulas for paths in Petri nets and claims that its satisfiability problem is ExpSpace-complete. In this paper, we show that in fact the satisfiability problem for this class of formulas is as hard as the reachability problem for Petri nets. Moreover, we salvage almost all of Yen’s results by defining a fragment of this class of formulas for which the satisfiability problem is ExpSpace-complete by adapting his proof.
For the entire collection see [Zbl 1175.68005].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Esparza, J.: On the decidability of model checking for several \(\mu\)-calculi and petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 115–129. Springer, Heidelberg (1994) · Zbl 0938.03537 · doi:10.1007/BFb0017477
[2] Esparza, J., Nielsen, M.: Decidability issues for petri nets - a survey. Bulletin of the EATCS 52, 244–262 (1994) · Zbl 0791.68123
[3] Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: POPL, pp. 102–113. ACM, New York (2009) · Zbl 1315.68064
[4] Hack, M.H.T.: Decidability Questions for Petri Nets. PhD thesis, M.I.T (1976)
[5] Haddad, S., Poitrenaud, D.: Checking linear temporal formulas on sequential recursive petri nets. In: TIME, pp. 198–205 (2001) · doi:10.1109/TIME.2001.930718
[6] Keller, R.M.: A fundamental tehoerem of asynchronous parallel computation. In: Tse-Yun, F. (ed.) Parallel Processing. LNCS, vol. 24, pp. 102–112. Springer, Heidelberg (1975) · doi:10.1007/3-540-07135-0_113
[7] Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: STOC, pp. 267–281. ACM, New York (1982)
[8] Lambert, J.L.: A structure to decide reachability in petri nets. Theor. Comput. Sci. 99(1), 79–104 (1992) · Zbl 0769.68104 · doi:10.1016/0304-3975(92)90173-D
[9] Lipton, R.: The reachability problem requires exponential time. Technical Report TR 66 (1976)
[10] Mayr, E.W.: An algorithm for the general petri net reachability problem. In: STOC, pp. 238–246. ACM, New York (1981)
[11] Mayr, E.W.: Persistence of vector replacement systems is decidable. Acta Inf. 15, 309–318 (1981) · Zbl 0454.68048 · doi:10.1007/BF00289268
[12] Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978) · Zbl 0368.68054 · doi:10.1016/0304-3975(78)90036-1
[13] Yen, H.-C.: A unified approach for deciding the existence of certain petri net paths. Inf. Comput. 96(1), 119–137 (1992) · Zbl 0753.68078 · doi:10.1016/0890-5401(92)90059-O
[14] Yen, H.-C.: A note on fine covers and iterable factors of vas languages. Inf. Process. Lett. 56(5), 237–243 (1995) · Zbl 1022.68574 · doi:10.1016/0020-0190(95)00168-2
[15] Yen, H.-C.: On the regularity of petri net languages. Inf. Comput. 124(2), 168–181 (1996) · 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.