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

Abstract. 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 automat...

• Type: Conference
• Year: 2007
• Where: ICALP
• Authors: Marcelo Arenas, Pablo Barceló, Leonid Libkin
• Keywords: Alternating Automata, ICALP 2007, Nested Words, Regular Languages, Theoretical Computer Science