Ramsey Goes Visibly Pushdown

  • Oliver Friedmann
  • Felix Klaedtke
  • Martin Lange
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)


Checking whether one formal language is included in another is vital to many verification tasks. In this paper, we provide solutions for checking the inclusion of the languages given by visibly pushdown automata over both finite and infinite words. Visibly pushdown automata are a richer automaton model than the classical finite-state automata, which allows one, e.g., to reason about the nesting of procedure calls in the executions of recursive imperative programs. The highlight of our solutions is that they do not comprise automata constructions for determinization and complementation. Instead, our solutions are more direct and generalize the so-called Ramsey-based inclusion-checking algorithms, which apply to classical finite-state automata and proved effective there, to visibly pushdown automata. We also experimentally evaluate our algorithms thereby demonstrating the virtues of avoiding determinization and complementation constructions.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A., Chen, Y.-F., Clemente, L., Holík, L., Hong, C.-D., Mayr, R., Vojnar, T.: Advanced Ramsey-based Büchi automata inclusion testing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 187–202. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Progr. Lang. Syst. 27(4), 786–818 (2005)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 1–43 (2009)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Breuers, S., Löding, C., Olschewski, J.: Improved Ramsey-based Büchi complementation. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 150–164. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  6. 6.
    Bruyère, V., Ducobu, M., Gauwin, O.: Visibly pushdown automata: Universality and inclusion via antichains. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 190–201. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  7. 7.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the 1960 Internat. Congr. on Logic, Method, and Philosophy of Science, pp. 1–11 (1960)Google Scholar
  8. 8.
    Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time μ-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273–284. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Doyen, L., Raskin, J.-F.: Antichains for the automata-based approach to model-checking. Log. Methods Comput. Sci. 5(1) (2009)Google Scholar
  11. 11.
    Driscoll, E., Burton, A., Reps, T.: Checking conformance of a producer and a consumer. In: ESEC/FSE 2011, pp. 113–123.Google Scholar
  12. 12.
    Driscoll, E., Thakur, A., Reps, T.: OpenNWA: A nested-word automaton library. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 665–671. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  13. 13.
    Fogarty, S., Vardi, M.Y.: Büchi complementation and size-change termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 16–30. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Fogarty, S., Vardi, M.Y.: Efficient Büchi universality checking. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 205–220. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Friedmann, O., Klaedtke, F., Lange, M.: Ramsey goes visibly pushdown (2012) (Manuscript); Available at authors’ web pagesGoogle Scholar
  16. 16.
    Friedmann, O., Lange, M.: Ramsey-based analysis of parity automata. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 64–78. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  17. 17.
    Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL 2010, pp. 471–482 (2010)Google Scholar
  18. 18.
    La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007, pp. 161–170 (2007)Google Scholar
  19. 19.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL 2001, pp. 81–92 (2001)Google Scholar
  20. 20.
    Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc. 30, 264–286 (1928)MathSciNetGoogle Scholar
  21. 21.
    Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of büchi complementation. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 261–271. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  22. 22.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986, pp. 332–344 (1986)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Oliver Friedmann
    • 1
  • Felix Klaedtke
    • 2
  • Martin Lange
    • 3
  1. 1.LMU MunichGermany
  2. 2.ETH ZurichSwitzerland
  3. 3.University of KasselGermany

Personalised recommendations