Abstract
Pushdown systems (PDSs) model single-thread recursive programs, and well-structured transition systems (WSTSs), such as vector addition systems, are useful to represent non-recursive multi-thread programs. Combining these two ideas, our goal is to investigate well-structured pushdown systems (WSPDSs), pushdown systems with well-quasi-ordered control states and stack alphabet.
This paper focuses on subclasses of WSPDSs, in which the coverability becomes decidable. We apply WSTS-like techniques on classical P-automata. A Post *-automata (resp. Pre *-automata) construction is combined with Karp-Miller acceleration (resp. ideal representation) to characterize the set of successors (resp. predecessors) of given configurations. As examples, we show that the coverability is decidable for recursive vector addition system with states, multi-set pushdown systems, and a WSPDS with finite control states and well-quasi-ordered stack alphabet.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P., Cerans, K., Jonsson, C., Yih-Kuen, T.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160(1-2), 109–127 (2000)
Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent pro-grams with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 107–123. Springer, Heidelberg (2009)
Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: Principles of Programming Languages (POPL 2012), pp. 203–214. ACM (2012)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 136–150. Springer, Heidelberg (2007)
Demri, S., Jurdziński, M., Lachish, O., Lazic, R.: The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences 79(1), 23–38 (2012)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 499–508. Springer, Heidelberg (1987)
Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electronic Notes Theoretical Computer Science 9, 27–37 (1997)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)
Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, Part I: Completions. In: STACS 2009, pp. 433–444 (2009), http://www.stacs-conf.org
Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, Part II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 188–199. Springer, Heidelberg (2009)
Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: Principles of Programming Languages (POPL 2007), pp. 339–350. ACM (2007)
Lazić, R.: The reachability problem for vector addition systems with a stack is not elementary (2012), http://rp12.labri.fr (manuscript)
Leroux, J.: Vector addition system reachability problem. In: Principles of Programming Languages (POPL 2011), pp. 307–316. ACM (2011)
Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM Journal Computing 13(3), 441–460 (1984)
Mayr, R.: Process rewrite systems. Information and Computation 156, 264–286 (1999)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Programming Languages and Systems 22(2), 416–430 (2000)
Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 300–314. Springer, Heidelberg (2006)
Verma, K., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Discrete Mathematics & Theoretical Computer Science 7(1), 217–230 (2005)
Weiermann, A.: Complexity bounds for some finite form of Kruskal’s theorem. Journal of Symbolic Computation 18, 463–488 (1994)
Xiaojuan, C., Ogawa, M.: Well-structured pushdown system, Part 1: Decidable classes for coverability. JAIST Research Report IS-RR-2013-001 (2013), http://hdl.handle.net/10119/11347
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cai, X., Ogawa, M. (2013). Well-Structured Pushdown Systems. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-40184-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40183-1
Online ISBN: 978-3-642-40184-8
eBook Packages: Computer ScienceComputer Science (R0)