Symbolic Automata: ω-Regularity Modulo Theories

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 theories), an alphabet is represented by an effective Boolean algebra, 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"uchi 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, NBWA. In particular, we define: (1) alternating B"uchi automata modulo A, ABWA as well (non-alternating) non-deterministic B"uchi 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's; (3) a definition of linear temporal logic (LTL) modulo A that generalizes Vardi's construction of alternating B"uchi 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.