Symbolic Automata: 𝜔-Regularity Modulo Theories
Margus Veanes
Microsoft Research
Abstract:
Symbolic automata are finite state automata that support
potentially infinite alphabets, such as the set of rational numbers,
generally applied to regular expressions/languages over
finite words. In symbolic automata (or automata modulo A),
an alphabet is represented by an effective Boolean algebra A,
supported by a decision procedure for satisfiability. Regular
languages over infinite words (so called 𝜔-regular languages)
have a rich history paralleling that of regular languages over
finite words, with well known applications to model checking
via Büchi automata and temporal logics.
We generalize symbolic automata to support 𝜔-regular
languages via symbolic transition terms and symbolic derivatives,
bringing together a variety of classic automata and
logics in a unified framework that provides all the necessary
ingredients to support symbolic model checking modulo A.
In particular, we define: (1) alternating Büchi automata modulo
A (ABWA) as well (non-alternating) nondeterministic
Büchi automata modulo A (NBWA); (2) an alternation elimination
algorithm that incrementally constructs an NBWA
from an ABWA, and can also be used for constructing the
product of two NBWA; (3) a definition of linear temporal
logic (LTL) modulo A that generalizes Vardi’s construction
of alternating Büchi automata from LTL, using (2) to go from
LTL modulo A to NBWA via ABWA.
Finally, we present a combination of LTL modulo A with
extended regular expressions modulo A that generalizes
the Property Specification Language (PSL). Our combination
allows regex complement, that is not supported in PSL but can
be supported naturally by using symbolic transition terms.