×

zbMATH — the first resource for mathematics

Small vertex cover makes Petri net coverability and boundedness easier. (English) Zbl 1253.68250
Raman, Venkatesh (ed.) et al., Parameterized and exact computation. 5th international symposium, IPEC 2010, Chennai, India, December 13–15, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-17492-6/pbk). Lecture Notes in Computer Science 6478, 216-227 (2010).
Summary: The coverability and boundedness problems for Petri nets are known to be Expspace-complete. Given a Petri net, we associate a graph with it. With the vertex cover number \(k\) of this graph and the maximum arc weight \(W\) as parameters, we show that coverability and boundedness are in ParaPspace. This means that these problems can be solved in space \(\mathcal{O}(\mathrm{ef}(k,W)\mathrm{poly}(n))\), where \(\mathrm{ef}(k,W)\) is some exponential function and \(\mathrm{poly}(n)\) is some polynomial in the size of the input. We then extend the ParaPspace result to model-checking a logic that can express some generalizations of coverability and boundedness.
For the entire collection see [Zbl 1202.68012].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
05C70 Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Atig, M.F., Habermehl, P.: On Yen’s path logic for Petri nets. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 51–63. Springer, Heidelberg (2009) · Zbl 1260.68255 · doi:10.1007/978-3-642-04420-5_7
[2] Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: TACAS 2009. LNCS, vol. 5505, pp. 107–123. Springer, Heidelberg (2009) · Zbl 1234.68068
[3] Demri, S.: On selective unboundedness. In: Infinity (to appear, 2010) · Zbl 1285.68094
[4] Downey, R.: Parameterized complexity for the skeptic. In: CCC 2003, pp. 147–170 (2003) · doi:10.1109/CCC.2003.1214417
[5] Downey, R.G., Fellows, M.R., Stege, U.: Parameterized complexity: A framework for systematically confronting computational intractability. In: Contemporary Trends in Discrete Mathematics: From DIMACS and DIMATIA to the Future. DIMACS, vol. 49, pp. 49–100 (1999) · Zbl 0935.68046 · doi:10.1007/978-1-4612-0515-9
[6] Esparza, J.: Decidability and complexity of Petri net problems – An introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998) · Zbl 0926.68087 · doi:10.1007/3-540-65306-6_20
[7] Esparza, J., Nielsen, M.: Decidability issues for Petri nets – a survey. J. Inform. Process. Cybernet. 30(3), 143–160 (1994) · Zbl 0838.68082
[8] Fellows, M.R., Lokshtanov, D., Misra, N., Rosamond, F.A., Saurabh, S.: Graph layout problems parameterized by vertex cover. In: Hong, S.-H., Nagamochi, H., Fukunaga, T. (eds.) ISAAC 2008. LNCS, vol. 5369, pp. 294–305. Springer, Heidelberg (2008) · Zbl 1183.68424 · doi:10.1007/978-3-540-92182-0_28
[9] Flum, J., Grohe, M.: Describing parameterized complexity classes. Inf. Comput. 187(2), 291–319 (2003) · Zbl 1076.68031 · doi:10.1016/S0890-5401(03)00161-5
[10] Göller, S., Haase, C., Ouaknine, J., Worrell, J.: Model checking succinct and parametric one-counter automata. In: Gavoille, C. (ed.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 575–586. Springer, Heidelberg (2010) · Zbl 1288.68164 · doi:10.1007/978-3-642-14162-1_48
[11] Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in succinct and parametric one-counter automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol. 5710, pp. 369–383. Springer, Heidelberg (2009) · Zbl 1254.68134 · doi:10.1007/978-3-642-04081-8_25
[12] Habermehl, P.: On the complexity of the linear-time \(\mu\)-calculus for Petri-nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997) · doi:10.1007/3-540-63139-9_32
[13] Kavi, K.M., Moshtaghi, A., Chen, D.-J.: Modeling multithreaded applications using petri nets. Int. J. Parallel Program. 30(5), 353–371 (2002) · Zbl 1083.68578 · doi:10.1023/A:1019917329895
[14] Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proc. 14th STOC, pp. 267–281 (1982)
[15] Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 308–322. Springer, Heidelberg (2005) · Zbl 1078.68034 · doi:10.1007/978-3-540-32033-3_23
[16] Lipton, R.: The reachability problem requires exponential space. Technical report, Yale university (1975)
[17] Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proc. 13th STOC, pp. 238–246 (1981) · doi:10.1145/800076.802477
[18] Petri, C.A.: Kommunikation mit Automaten. PhD thesis, Inst. Instrumentelle Math. (1962)
[19] Praveen, M., Lodaya, K.: Modelchecking counting properties of 1-safe nets with buffers in parapspace. In: FSTTCS 2009. LIPIcs, vol. 4, pp. 347–358 (2009) · Zbl 1248.68356
[20] Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoret. Comp. Sci. 6, 223–231 (1978) · Zbl 0368.68054 · doi:10.1016/0304-3975(78)90036-1
[21] Reisig, W., Rozenberg, G.: Informal introduction to Petri nets. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 1–11. Springer, Heidelberg (1998) · doi:10.1007/3-540-65306-6_13
[22] Rosier, L.E., Yen, H.-C.: A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci. 32(1), 105–135 (1986) · Zbl 0614.68048 · doi:10.1016/0022-0000(86)90006-1
[23] Thorup, M.: All structured programs have small tree width and good register allocation. Inf. and Comp. 142(2), 159–181 (1998) · Zbl 0924.68023 · doi:10.1006/inco.1997.2697
[24] 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
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.