Abstract
Pushdown automata may contain transitions that are never used in any accepting run of the automaton. We present an algorithm for detecting such useless transitions. A finite automaton that captures the possible stack content during runs of the pushdown automaton, is first constructed in a forward procedure to determine which transitions are reachable, and then employed in a backward procedure to determine which of these transitions can lead to a final state. An implementation of the algorithm is shown to exhibit a favorable performance.
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
Similar content being viewed by others
References
Bertsch, E., Nederhof, M.-J.: Regular closure of deterministic languages. SIAM J. Comput. 29(1), 81–102 (1999)
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). doi:10.1007/3-540-63141-0_10
Chatzikalymnios, E.: Comparison of two algorithms for detecting useless transitions in pushdown automata. BSc. thesis, Vrije Universiteit Amsterdam (2016). http://www.cs.vu.nl/~tcs/chatzikalymnios-bscthesis.pdf
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). doi:10.1007/10722167_20
Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: INFINITY 1997. ENTCS, vol. 9, pp. 27–37. Elsevier (1997)
Goldstine, J., Price, J.K., Wotschke, D.: A pushdown automaton or a context-free grammar - which is more economical? Theoret. Comput. Sci. 18, 33–40 (1982)
Griffin, C.: A note on deciding controllability in pushdown systems. IEEE Trans. Autom. Control 51(2), 334–337 (2006)
Grune, D., Jacobs, C.: Parsing Techniques - A Practical Guide, 2nd edn. Springer, Heidelberg (2008)
Linz, P.: An Introduction to Formal Languages and Automata. Jones & Bartlett, Burlington (2011)
Nederhof, M.-J., Bertsch, E.: Linear-time suffix parsing for deterministic languages. J. ACM 43(3), 524–554 (1996)
Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996). doi:10.1007/3-540-61474-5_58
Acknowledgments
Javier Esparza proposed the alternative approach using \({ pre}{*}\) and \({ post}{*}\). Jörg Endrullis provided a useful suggestion for the efficient implementation of this alternative approach.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Grune, D., Fokkink, W., Chatzikalymnios, E., Hond, B., Rutgers, P. (2017). Detecting Useless Transitions in Pushdown Automata. In: Drewes, F., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2017. Lecture Notes in Computer Science(), vol 10168. Springer, Cham. https://doi.org/10.1007/978-3-319-53733-7_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-53733-7_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-53732-0
Online ISBN: 978-3-319-53733-7
eBook Packages: Computer ScienceComputer Science (R0)