×

Small vertex cover makes Petri net coverability and boundedness easier. (English) Zbl 1410.68258

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} ({\operatorname{ef}}(k, W){\operatorname{poly}}(n))\), where \(\operatorname{ef}(k,W)\) is some super-polynomial function and \(\operatorname{poly}(n)\) is some polynomial in the size of the input \(n\). We then extend the ParaPspace result to model checking a logic that can express some generalizations of coverability and boundedness.

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.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Atig, M.F., Habermehl, P.: On Yen’s path logic for Petri nets. Int. J. Found. Comput. Sci. 22(4), 783–799 (2011) · Zbl 1230.68153 · doi:10.1142/S0129054111008428
[2] Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4), 1–48 (2011) · Zbl 1237.68056
[3] Borosh, I., Treybig, L.: Bounds on positive integral solutions of linear diophantine equations. Proc. Am. Math. Soc. 55(2), 299–304 (1976) · Zbl 0291.10014 · doi:10.1090/S0002-9939-1976-0396605-3
[4] Demri, S.: On selective unboundedness of VASS. In: Proceedings of the Twelfth International Workshop on Verification of Infinite-State Systems. Electronic Proceedings in Theoretical Computer Science, vol. 39, pp. 1–15. Open Publishing Association (2010) · Zbl 1285.68094
[5] Desel, J., Reisig, W.: Place/transition Petri nets. In: Lectures on Petri Nets I: Basic Models, Advances in Petri Nets. Lecture Notes in Computer Science, vol. 1491, pp. 122–173. Springer, Berlin (1998) · Zbl 0926.68083
[6] Downey, R.: Parameterized complexity for the skeptic. In: Proceedings of the Eighteenth IEEE Conference on Computational Complexity, pp. 147–170. IEEE Comput. Soc., Los Alamitos (2003)
[7] 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 Series in Discrete Mathematics and Theoretical Computer Science, vol. 49, pp. 49–100. Am. Math. Soc., Providence (1999) · Zbl 0935.68046
[8] Esparza, J.: Decidability and complexity of Petri net problems- an introduction. In: Lectures on Petri Nets I: Basic Models, Advances in Petri Nets. Lecture Notes in Computer Science, vol. 1491, pp. 374–428. Springer, Berlin (1998) · Zbl 0926.68087
[9] Esparza, J., Nielsen, M.: Decidability issues for Petri nets–a survey. J. Inf. Process. Cybern. 30(3), 143–160 (1994) · Zbl 0838.68082
[10] Fellows, M.R., Lokshtanov, D., Misra, N., Rosamond, F.A., Saurabh, S.: Graph layout problems parameterized by vertex cover. In: Proceedings of the Nineteenth International Symposium on Algorithms and Computation. Lecture Notes in Computer Science, vol. 5369, pp. 294–305. Springer, Berlin (2008) · Zbl 1183.68424
[11] 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
[12] Habermehl, P.: On the complexity of the linear-time {\(\mu\)}-calculus for Petri-nets. In: Proceedings of the Eighteenth International Conference on Application and Theory of Petri Nets. Lecture Notes in Computer Science, vol. 1248, pp. 102–116. Springer, Berlin (1997)
[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: Proceedings of the Fourteenth ACM Symposium on Theory of Computing, pp. 267–281. Association for Computing Machinery, New York (1982)
[15] Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. In: Proceedings of the Sixteenth International conference on Term Rewriting and Applications. Lecture Notes in Computer Science, vol. 3467, pp. 308–322. Springer, Berlin (2005). Full version at http://www.lsv.ens-cachan.fr/Publis/RAPPORTS%5FLSV/PS/rr-lsv-2004-16.rr.ps · Zbl 1078.68034
[16] Lipton, R.: The reachability problem requires exponential space. Technical report 62, Yale university (1975)
[17] Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings of the Thirteenth ACM Symposium on Theory of Computing, pp. 238–246. Association for Computing Machinery, New York (1981)
[18] Petri, C.A.: Kommunikation mit automaten. Ph.D. thesis, Institut für Instrumentelle Mathematik (1962)
[19] Praveen, M., Lodaya, K.: Modelchecking counting properties of 1-safe nets with buffers in ParaPspace. In: Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics, vol. 4, pp. 347–358 (2009). Schloss Dagstuhl–Leibniz Center for Informatics · Zbl 1248.68356
[20] 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
[21] Reisig, W., Rozenberg, G.: Informal introduction to Petri nets. In: Lectures on Petri Nets I: Basic Models, Advances in Petri Nets. Lecture Notes in Computer Science, vol. 1491, pp. 1–11. Springer, Berlin (1998) · Zbl 0903.00072
[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. Comput. 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.