A grammatical representation of visibly pushdown languages

Joachim Baran; Howard Barringer

A grammatical representation of visibly pushdown languages

Joachim Baran, Howard Barringer

Research output: Chapter in Book/Conference proceeding › Conference contribution

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. © Springer-Verlag Berlin Heidelberg 2007.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	1-11
Number of pages	10
Volume	4576
ISBN (Print)	9783540734437
Publication status	Published - 2007
Event	14th International Workshop on Logic, Language, Information and Computation, WoLLIC 2007 - Rio de Janeiro Duration: 1 Jul 2007 → …

Conference

Conference	14th International Workshop on Logic, Language, Information and Computation, WoLLIC 2007
City	Rio de Janeiro
Period	1/07/07 → …

Keywords

Computer Science, Theory & Methods

Cite this

@inproceedings{565954ec19e142acabdebd43689ec68e,

title = "A grammatical representation of visibly pushdown languages",

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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.",

keywords = "Computer Science, Theory \& Methods",

author = "Joachim Baran and Howard Barringer",

note = "Assoc Symbol Logic, Interest Grp Pure Baran, Joachim Barringer, Howard 6 BERLIN BGK03; 14th International Workshop on Logic, Language, Information and Computation, WoLLIC 2007 ; Conference date: 01-07-2007",

year = "2007",

language = "English",

isbn = "9783540734437",

volume = "4576",

pages = "1--11",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

}

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)|Lect. Notes Comput. Sci.. vol. 4576, Springer Nature, pp. 1-11, 14th International Workshop on Logic, Language, Information and Computation, WoLLIC 2007, Rio de Janeiro, 1/07/07.

A grammatical representation of visibly pushdown languages. / Baran, Joachim; Barringer, Howard.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 4576 Springer Nature, 2007. p. 1-11.

Research output: Chapter in Book/Conference proceeding › Conference contribution

TY - GEN

T1 - A grammatical representation of visibly pushdown languages

AU - Baran, Joachim

AU - Barringer, Howard

N1 - Assoc Symbol Logic, Interest Grp Pure Baran, Joachim Barringer, Howard 6 BERLIN BGK03

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - Computer Science, Theory & Methods

UR - https://www.scopus.com/pages/publications/38149098500

M3 - Conference contribution

SN - 9783540734437

VL - 4576

SP - 1

EP - 11

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 14th International Workshop on Logic, Language, Information and Computation, WoLLIC 2007

Y2 - 1 July 2007

ER -

A grammatical representation of visibly pushdown languages

Abstract

Conference

Keywords

Other files and links

Fingerprint

Cite this