Abstract
This paper investigates a general framework of a pushdown system with well-quasi-ordered states and stack alphabet to show decidability of reachability, which is an extension of our earlier work (Well-structured Pushdown Systems, CONCUR 2013). As an instance, an alternative proof of the decidability of the reachability for dense-timed pushdown system (in P.A. Abdulla, M.F. Atig, F. Stenman, Dense-Timed Pushdown Automata, IEEE LICS 2012) is presented. Our proof would be more robust for extensions, e.g., regular valuations with time. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Cai, X., & Ogawa, M. (2014). Well-structured pushdown system: Case of dense timed pushdown automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8475 LNCS, pp. 336–352). Springer Verlag. https://doi.org/10.1007/978-3-319-07151-0_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
