Symbolic visibly pushdown automata

22Citations
Citations of this article
15Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

Nested words model data with both linear and hierarchical structure such as XML documents and program traces. A nested word is a sequence of positions together with a matching relation that connects open tags (calls) with the corresponding close tags (returns). Visibly Pushdown Automata are a restricted class of pushdown automata that process nested words, and have many appealing theoretical properties such as closure under Boolean operations and decidable equivalence. However, like any classical automata models, they are limited to finite alphabets. This limitation is restrictive for practical applications to both XML processing and program trace analysis, where values for individual symbols are usually drawn from an unbounded domain. With this motivation, we introduce Symbolic Visibly Pushdown Automata (SVPA) as an executable model for nested words over infinite alphabets. In this model, transitions are labeled with predicates over the input alphabet, analogous to symbolic automata processing strings over infinite alphabets. A key novelty of SVPAs is the use of binary predicates to model relations between open and close tags in a nested word. We show how SVPAs still enjoy the decidability and closure properties of Visibly Pushdown Automata. We use SVPAs to model XML validation policies and program properties that are not naturally expressible with previous formalisms and provide experimental results for our implementation. © 2014 Springer International Publishing.

References Powered by Scopus

Z3: An efficient SMT Solver

5748Citations
N/AReaders
Get full text

Visibly pushdown languages

459Citations
N/AReaders
Get full text

Adding nesting structure to words

266Citations
N/AReaders
Get full text

Cited by Powered by Scopus

The power of symbolic automata and transducers

41Citations
N/AReaders
Get full text

Extended symbolic finite automata and transducers

24Citations
N/AReaders
Get full text

Automata modulo theories

23Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

D’Antoni, L., & Alur, R. (2014). Symbolic visibly pushdown automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8559 LNCS, pp. 209–225). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_14

Readers over time

‘14‘17‘18‘19‘20‘21‘22‘23‘2401234

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 4

67%

Professor / Associate Prof. 1

17%

Researcher 1

17%

Readers' Discipline

Tooltip

Computer Science 9

100%

Save time finding and organizing research with Mendeley

Sign up for free
0