An Isaac Newton Institute Workshop

Games and Verification (GAMES 2006)

Nested words and trees

Author: Alur, R (University of Pennsylvania)

Abstract

This talk is centered around our recent model of nested words as a representation of data with both a linear ordering and a hierarchically nested matching of items. Such dual structure occurs in diverse corners of computer science ranging from executions of structured programs where there is a natural well-nested matching of entries to and exits from functions and procedures, to XML documents with the well-nested structure given by start-tags matched with end-tags. Finite-state acceptors for nested words define the class of regular languages of nested words that has all the appealing theoretical properties that the class of classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, and Kleene-*; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We argue that for algorithmic linear-time verification of pushdown systems, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words, and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics. We also discuss nested trees that are obtained adding nesting edges along paths of trees, and finite-state acceptors over nested trees. This leads to a very expressive fixpoint logic (equivalently, alteranting parity nested tree automata) with a decidable model checking problem for pushdown systems.