The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

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.