# Symbolic Automata: ω-Regularity Modulo Theories

arXiv: https://arxiv.org/abs/2310.02393 · HTML: https://mlsanity.com/paper/2310.02393/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Oct 2023.

## Built on by (most cited first, 1 of 1)

- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)

## Abstract (arXiv)

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.