Ramsey Goes Visibly Pushdown
METADATA ONLY
Loading...
Author / Creator
Date
2013
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
Abstract
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. © 2013 Springer-Verlag.
Permanent link
Publication status
published
External links
Book title
Automata, Languages, and Programming : 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II
Journal / series
Volume
7966 (2013)
Pages / Article No.
224 - 237
Publisher
Springer
Event
40th International Colloquium on Automata, Languages, and Programming (ICALP 2013)
Edition / version
Methods
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David