Detecting Useless Transitions in Pushdown Automata

  • Dick Grune
  • Wan FokkinkEmail author
  • Evangelos Chatzikalymnios
  • Brinio Hond
  • Peter Rutgers
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10168)


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.



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.


  1. 1.
    Bertsch, E., Nederhof, M.-J.: Regular closure of deterministic languages. SIAM J. Comput. 29(1), 81–102 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    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 Google Scholar
  3. 3.
    Chatzikalymnios, E.: Comparison of two algorithms for detecting useless transitions in pushdown automata. BSc. thesis, Vrije Universiteit Amsterdam (2016).
  4. 4.
    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 CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Griffin, C.: A note on deciding controllability in pushdown systems. IEEE Trans. Autom. Control 51(2), 334–337 (2006)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Grune, D., Jacobs, C.: Parsing Techniques - A Practical Guide, 2nd edn. Springer, Heidelberg (2008)CrossRefzbMATHGoogle Scholar
  9. 9.
    Linz, P.: An Introduction to Formal Languages and Automata. Jones & Bartlett, Burlington (2011)zbMATHGoogle Scholar
  10. 10.
    Nederhof, M.-J., Bertsch, E.: Linear-time suffix parsing for deterministic languages. J. ACM 43(3), 524–554 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    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 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Dick Grune
    • 1
  • Wan Fokkink
    • 1
    Email author
  • Evangelos Chatzikalymnios
    • 1
  • Brinio Hond
    • 1
  • Peter Rutgers
    • 1
  1. 1.Department of Computer ScienceVrije Universiteit AmsterdamAmsterdamThe Netherlands

Personalised recommendations