Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization

Marcelo Arenas, Pablo Barceló, Leonid Libkin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Nested words are a restriction of the class of visibly pushdown languages that provide a natural model of runs of programs with recursive procedure calls. The usual connection between monadic second-order logic (MSO) and automata extends from words to nested words and gives us a natural notion of regular languages of nested words.
In this paper we look at some well-known aspects of regular languages – their characterization via fixed points, deterministic and alternating automata for them, and synchronization for defining regular relations – and extend them to nested words. We show that mu-calculus is as expressive as MSO over finite and infinite nested words, and the equivalence holds, more generally, for mu-calculus with past modalities evaluated in arbitrary positions in a word, not only in the first position. We introduce the notion of alternating automata for nested words, show that they are as expressive as the usual automata, and also prove that Muller automata can be determinized (unlike in the case of visibly pushdown languages). Finally we look at synchronization over nested words. We show that the usual letter-to-letter synchronization is completely incompatible with nested words (in the sense that even the weakest form of it leads to an undecidable formalism) and present an alternative form of synchronization that gives us decidable notions of regular relations.
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages13
ISBN (Electronic)978-3-540-73420-8
ISBN (Print)978-3-540-73419-2
Publication statusPublished - 2007


Dive into the research topics of 'Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization'. Together they form a unique fingerprint.

Cite this