Abstract
Model-checking regular properties is well established and a powerful verification technique for regular as well as context-free program behaviours. Recently, through the use of ω-visibly pushdown languages (ωVPLs), defined by ω-visibly pushdown automata, model-checking of properties beyond regular expressiveness was made possible and shown to be still decidable even when the program’s model of behaviour is an ωVPL. In this paper, we give a grammatical representation of ωVPLs and the corresponding finite word languages – VPL. From a specification viewpoint, the grammatical representation provides a more natural representation than the automata approach.
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
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing, pp. 202–211. ACM Press, New York (2004)
Alur, R., Madhusudan, P.: Adding nesting structure to words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1–13. Springer, Heidelberg (2006)
Berstel, J., Boasson, L.: Balanced grammars and their languages. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, pp. 3–25. Springer, Heidelberg (2002)
Engelfriet, J.: An elementary proof of double Greibach normal form. Information Processing Letters 44(6), 291–293 (1992)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 2nd edn. Addison-Wesley, Reading (2001)
Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Baran, J., Barringer, H. (2007). A Grammatical Representation of Visibly Pushdown Languages. In: Leivant, D., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2007. Lecture Notes in Computer Science, vol 4576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73445-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-73445-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73443-7
Online ISBN: 978-3-540-73445-1
eBook Packages: Computer ScienceComputer Science (R0)