Symbolic Automata: Omega-Regularity Modulo Theories

This conference talk from POPL 2025 presents groundbreaking research on Symbolic Automata and their extension to ω-regularity modulo theories. Explore how researchers Margus Veanes, Thomas Ball, Gabriel Ebner, and Ekaterina Zhuchko generalize symbolic automata to support ω-regular languages through symbolic transition terms and symbolic derivatives. Learn about their unified framework that combines classic automata and logics to support symbolic model checking modulo A, including their definitions of Alternating Büchi Word automata modulo A (ABWₐ) and Nondeterministic Büchi Word automata modulo A (NBWₐ). Discover their alternation elimination algorithm and their novel definition of linear temporal logic modulo A (LTLₐ). The presentation also introduces RLTLₐ, which combines LTLₐ with extended regular expressions modulo A, generalizing the Property Specification Language while supporting regex complement. The research is formally verified using the Lean proof assistant, with artifacts available and evaluated as reusable.