We propose {\em nested words\/} to capture models where there is
{\em both\/} a natural linear sequencing of positions and a hierarchically
nested matching of positions. Such dual structure exists for executions of
structured programs where there is a natural well-nested correspondence among
entries to and exits from program components such as functions and procedures,
and for XML documents where each open-tag is matched with a closing tag in a
well-nested manner.
We define and study finite-state automata as acceptors of nested words.
A nested-word automaton is similar to a classical finite-state word
automaton, and reads the input from left to right according to the linear
sequence.
However, at a position with two predecessors, one due to linear
sequencing and one due to a hierarchical nesting edge, the next state
depends on states of the run at both these predecessors.
The resulting class of {\em regular\/} languages of nested words 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 operations such
as union, intersection, complementation, concatenation, and Kleene-$*$;
decision problems such as membership, emptiness, language
inclusion, and language equivalence are all decidable;
definability in monadic second order logic of nested words corresponds exactly
to finite-state recognizability; and finiteness of the congruence induced by a
language of nested words is a necessary and sufficient condition for
regularity.
The motivating application area for our results has been software verification.
Given a sequential program $P$ with stack-based control flow, the execution
of $P$ is modeled as a nested word with nesting edges from calls to returns.
Specification of the program is given as a nested word automaton $A$, and
verification corresponds to checking whether every nested word generated by $P$
is accepted by $A$. Nested-word automata can express a variety of requirements
such as stack-inspection properties, pre-post conditions, and interprocedural
data-flow properties.
If we were to model program executions as words,
all of these properties are non-regular, and hence inexpressible in classical
specification languages based on temporal logics, automata, and fixpoint
calculi (recall that context-free languages cannot be used as specification
languages due to nonclosure under intersection and undecidability of key
decision problems such as language inclusion).
In finite-state software model checking, the data variables in the program are
abstracted into a set of boolean variables, and in that case, the set of nested
words generated by the abstracted program is regular.
This implies that algorithmic software verification is possible for all regular
specifications of nested words.
We believe that the nested-word view will provide a unifying basis for the next
generation of specification logics for program analysis, software model
checking, and runtime monitoring.
As explained in Section 3, another potential area of application is XML
document processing.
