Lattice Automata
================
Several verification methods involve reasoning about multi-valued
systems, in which an atomic proposition is interpreted at a state as a
lattice element, rather than a Boolean value. The automata-theoretic
approach for reasoning about Boolean-valued systems has proven to be
very useful and powerful. We develop an automata-theoretic framework
for reasoning about multi-valued objects, and describe its
application. The basis to our framework are {\em lattice automata} on
finite and infinite words, which assign to each input word a lattice
element. We study the expressive power of lattice automata, their
closure properties, the blow-up involved in related constructions, and
decision problems for them. Our framework and results are different
and stronger then those known for semi-ring and weighted automata.
Lattice automata exhibit interesting features from a theoretical point
of view. In particular, we study the complexity of constructions and
decision problems for lattice automata in terms of the size of both
the automaton and the underlying lattice. For example, we show that
while determinization of lattice automata involves a blow up that
depends on the size of the lattice, such a blow up can be avoided when
we complement lattice automata. Thus, complementation is easier than
determinization. In addition to studying the theoretical aspects of
lattice automata, we describe how they can be used for an efficient
reasoning about a multi-valued extension of LTL.