Hardness Results for Coverability Problem of Well-Structured Pushdown Systems
Well-Structured Pushdown Systems (WSPDSs) are pushdown systems extended with states and stack alphabet to be vectors, for modeling (restricted) recursive concurrent programs. It has been considered to be “very close to the border of undecidability”. In this paper, we prove some hardness results for the coverability problem of WSPDSs. We show that for WSPDS with three dimensional vectors as states and WSPDS with three dimensional vectors as stack alphabet, the coverability problem becomes Ackermann-hard.
KeywordsAutomata and logic Coverability Lower bounds
This research is partially supported by NSFC project 61472238, 61261130589, and 61511140100. The authors would like to thank Prof. Mizuhito Ogawa and anonymous reviewers for their helpful comments on the earlier version of this work.
- 3.Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: Proceedings of Principles of Programming Languages, POPL 2012, pp. 203–214. ACM (2012)Google Scholar
- 5.Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: Proceedings of Logic in Computer Science, LICS 2012, pp. 355–364. IEEE (2012)Google Scholar
- 6.Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary. CoRR abs/1310.1767 (2013)Google Scholar
- 7.Lei, S., Cai, X., Ogawa, M.: Termination and boundedness for well-structured pushdown systems. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering, TASE 2016, pp. 22–29 (2016)Google Scholar
- 8.Leroux, J., Praveen, M., Sutre, G.: Hyper-Ackermannian bounds for pushdown vector addition systems. In: Proceedings of Joint Meeting of Computer Science Logic and Logic in Computer Science, CSL-LICS 2014, pp. 1–10 (2014)Google Scholar
- 9.Lipton, R.J.: The reachability problem requires exponential space. Technical report, Yale University (1976)Google Scholar
- 10.Minsky, M.L.: Computation: Finite and Infinite Machines. American Mathematical Monthly (1968)Google Scholar