Symbolic Automata: omega-Regularity Modulo Theories

on YouTube ↗20m

" summary

Generalizes symbolic automata to omega-regular languages by introducing symbolic transition terms and symbolic derivatives, defines Alternating Buchi (ABW_A) and Nondeterministic Buchi (NBW_A) automata modulo an effective Boolean algebra A, and gives an alternation-elimination algorithm that incrementally builds NBW_A (and products) from ABW_A. Adds LTL_A and RLTL_A (regular expressions with complement over A), formalizes correctness in Lean, and ships reusable artifacts and algorithms aimed at symbolic model checking over large/infinite alphabets.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 0:45Regular languages history
3. 3:41Motivation for symbolic automata
4. 6:05RLTL logic definition
5. 9:18Symbolic model checking
6. 10:42Derivative functions in logic
7. 13:49Simplifying transition terms
8. 15:13Alternating automata
9. 16:37RLTL examples
10. 17:17Formalization in Lean
11. 17:38Question and answer session