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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Baran, J., & Barringer, H. (2007). A grammatical representation of visibly pushdown languages. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4576 LNCS, pp. 1–11). Springer Verlag. https://doi.org/10.1007/978-3-540-73445-1_1
Mendeley helps you to discover research relevant for your work.