Small Vertex Cover makes Petri Net Coverability and Boundedness Easier

详细信息    查看全文

• 作者：M. Praveen (1)
  
• 关键词：Petri nets ; Vertex cover ; Parameterized complexity ; ParaPspace
• 刊名：Algorithmica
• 出版年：2013
• 出版时间：April 2013
• 年：2013
• 卷：65
• 期：4
• 页码：713-753
• 参考文献：1. Atig, M.F., Habermehl, P.: On Yen鈥檚 path logic for Petri nets. Int. J. Found. Comput. Sci. 22(4), 783鈥?99 (2011) CrossRef
  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鈥?8 (2011)
  3. Borosh, I., Treybig, L.: Bounds on positive integral solutions of linear diophantine equations. Proc. Am. Math. Soc. 55(2), 299鈥?04 (1976) CrossRef
  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鈥?5. Open Publishing Association (2010)
  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鈥?73. Springer, Berlin (1998) CrossRef
  6. Downey, R.: Parameterized complexity for the skeptic. In: Proceedings of the Eighteenth IEEE Conference on Computational Complexity, pp. 147鈥?70. 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鈥?00. Am. Math. Soc., Providence (1999)
  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鈥?28. Springer, Berlin (1998) CrossRef
  9. Esparza, J., Nielsen, M.: Decidability issues for Petri nets鈥攁 survey. J. Inf. Process. Cybern. 30(3), 143鈥?60 (1994)
  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鈥?05. Springer, Berlin (2008) CrossRef
  11. Flum, J., Grohe, M.: Describing parameterized complexity classes. Inf. Comput. 187(2), 291鈥?19 (2003) CrossRef
  12. Habermehl, P.: On the complexity of the linear-time / 渭-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鈥?16. 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鈥?71 (2002) CrossRef
  14. Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proceedings of the Fourteenth ACM Symposium on Theory of Computing, pp. 267鈥?81. 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鈥?22. Springer, Berlin (2005). Full version at http://www.lsv.ens-cachan.fr/Publis/RAPPORTS%5FLSV/PS/rr-lsv-2004-16.rr.ps CrossRef
  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鈥?46. 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鈥?58 (2009). Schloss Dagstuhl鈥擫eibniz Center for Informatics
  20. Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223鈥?31 (1978) CrossRef
  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鈥?1. Springer, Berlin (1998) CrossRef
  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鈥?35 (1986) CrossRef
  23. Thorup, M.: All structured programs have small tree width and good register allocation. Inf. Comput. 142(2), 159鈥?81 (1998) CrossRef
  24. Yen, H.-C.: A unified approach for deciding the existence of certain Petri net paths. Inf. Comput. 96(1), 119鈥?37 (1992) CrossRef
  
• 作者单位：M. Praveen (1)
  
  1. The Institute of Mathematical Sciences, Chennai, India
  
• ISSN：1432-0541

文摘

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} ({\mathit{ef}}(k, W){\mathit{poly}}(n) )$ , where ef(k,W) is some super-polynomial function and 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.