×

zbMATH — the first resource for mathematics

Coverability trees for Petri nets with unordered data. (English) Zbl 06591835
Jacobs, Bart (ed.) et al., Foundations of software science and computation structures. 19th international conference, FOSSACS 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49629-9/pbk; 978-3-662-49630-5/ebook). Lecture Notes in Computer Science 9634, 445-461 (2016).
Summary: We study an extension of classical Petri nets where tokens carry values from a countable data domain, that can be tested for equality upon firing transitions. These unordered data Petri nets (UDPN) are well-structured and therefore allow generic decision procedures for several verification problems including coverability and boundedness.
We show how to construct a finite representation of the coverability set in terms of its ideal decomposition. This not only provides an alternative method to decide coverability and boundedness, but is also an important step towards deciding the reachability problem. This also allows to answer more precise questions about the reachability set, for instance whether there is a bound on the number of tokens on a given place (place boundedness), or if such a bound exists for the number of different data values carried by tokens (place width boundedness).
We provide matching Hyper-Ackermann bounds on the size of coverability trees and on the running time of the induced decision procedures.
For the entire collection see [Zbl 1333.68011].

MSC:
68Qxx Theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Inform. and Comput. 160(1–2), 109–127 (2000) · Zbl 1046.68567 · doi:10.1006/inco.1999.2843
[2] Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 108–119. Springer, Heidelberg (2011) · Zbl 1343.68152 · doi:10.1007/978-3-642-22993-0_13
[3] Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Logic. Meth. Comput. Sci. 10(3:4), 1–44 (2014) · Zbl 1338.68140
[4] Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative semigroups: preliminary report. In: STOC 1976, pp. 50–54. ACM (1976) · Zbl 0374.20067 · doi:10.1145/800113.803630
[5] Demri, S.: On selective unboundedness of VASS. J. Comput. Syst. Sci. 79(5), 689–713 (2013) · Zbl 1285.68094 · doi:10.1016/j.jcss.2013.01.014
[6] Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In: LICS 2011, pp. 269–278. IEEE Press (2011) · doi:10.1109/LICS.2011.39
[7] Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001) · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[8] Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: completions. In: STACS 2009. LIPIcs, vol. 3, pp. 433–444. LZI (2009) · Zbl 1236.68183
[9] Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: complete WSTS. Logic. Meth. Comput. Sci. 8(3:28), 1–35 (2012) · Zbl 1248.68329
[10] Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing Petri net extensions. Inform. and Comput. 195(1–2), 1–29 (2004) · Zbl 1101.68696 · doi:10.1016/j.ic.2004.01.005
[11] Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: LICS 2012, pp. 355–364. IEEE Press (2012) · Zbl 1362.68214 · doi:10.1109/LICS.2012.46
[12] Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969) · Zbl 0198.32603 · doi:10.1016/S0022-0000(69)80011-5
[13] Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proceedings STOC 1982, pp. 267–281. ACM (1982)
[14] 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
[15] Lazić, R., Newcomb, T., Ouaknine, J., Roscoe, A., Worrell, J.: Nets with tokens which carry data. Fund. Inform. 88(3), 251–274 (2008) · Zbl 1154.68090
[16] Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: LICS 2015, pp. 56–67. IEEE Press (2015) · Zbl 1392.68308 · doi:10.1109/LICS.2015.16
[17] Lipton, R.: The reachability problem requires exponential space. Technical Report 62, Yale University (1976)
[18] Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings STOC 1981, pp. 238–246. ACM (1981) · doi:10.1145/800076.802477
[19] Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6(2), 223–231 (1978) · Zbl 0368.68054 · doi:10.1016/0304-3975(78)90036-1
[20] Rosa-Velardo, F.: Ordinal recursive complexity of unordered data nets. Technical Report TR-4-14, Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid (2014). http://antares.sip.ucm.es/frosa/docs/complexityUDN.pdf
[21] Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci. 412(34), 4439–4451 (2011) · Zbl 1231.68172 · doi:10.1016/j.tcs.2011.05.007
[22] Rosa-Velardo, F., Martos-Salgado, M., de Frutos-Escrig, D.: Accelerations for the coverability set of Petri nets with names. Fund. Inform. 113(3–4), 313–341 (2011) · Zbl 1248.68357
[23] Schmitz, S.: Complexity hierarchies beyond elementary. ACM Trans. Comput. Theor. (2016) (to appear). http://arxiv.org/abs/1312.5686 · Zbl 1347.68162
[24] Schmitz, S., Schnoebelen, P.: Algorithmic aspects of WQO theory. Lecture notes (2012). http://cel.archives-ouvertes.fr/cel-00727025
[25] Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 5–24. Springer, Heidelberg (2013) · Zbl 1390.68488 · doi:10.1007/978-3-642-40184-8_2
[26] Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010) · Zbl 1287.68059 · doi:10.1007/978-3-642-15155-2_54
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.