A lower bound for the coverability problem in acyclic pushdown VAS

作者: Matthias Englert , Piotr Hofman , Sławomir Lasota , Ranko Lazić , Jérôme Leroux

DOI: 10.1016/J.IPL.2020.106079

关键词:

摘要: Abstract We investigate the coverability problem for a one-dimensional restriction of pushdown vector addition systems with states. improve lower complexity bound to PSpace , even in acyclic case.

参考文章(7)
Stephen Travers, The complexity of membership problems for circuits over sets of integers Theoretical Computer Science. ,vol. 369, pp. 211- 229 ,(2006) , 10.1016/J.TCS.2006.08.017
Jérôme Leroux, M. Praveen, Grégoire Sutre, Hyper-Ackermannian bounds for pushdown vector addition systems logic in computer science. pp. 63- ,(2014) , 10.1145/2603088.2603146
Ranko Lazić, Patrick Totzke, What Makes Petri Nets Harder to Verify: Stack or Data? Springer International Publishing. pp. 144- 161 ,(2017) , 10.1007/978-3-319-51046-0_8
Patrick Totzke, Grégoire Sutre, Jérôme Leroux, On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension arXiv: Formal Languages and Automata Theory. ,(2015)
Georg Zetzsche, Sylvain Schmitz, Coverability is Undecidable in One-dimensional Pushdown Vector Addition Systems with Resets arXiv: Formal Languages and Automata Theory. ,(2019)
Patrick Totzke, Grégoire Sutre, Jérôme Leroux, On Boundedness Problems for Pushdown Vector Addition Systems arXiv: Formal Languages and Automata Theory. ,(2015)
Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, Filip Mazowiecki, The reachability problem for Petri nets is not elementary symposium on the theory of computing. pp. 24- 33 ,(2019) , 10.1145/3313276.3316369