Reactive Synthesis Empowered by Logical Reasoning

on YouTube ↗45m

" summary

Overview of SAT-based reactive synthesis with concrete encodings and results: bounded synthesis searches for finite-state implementations up to a given size via SMT/QBF/DQBF or explicit SAT encodings and is used to produce concrete arbiters and a “patient arbiter” prototype; the bounded maximum-realizability formulation reduces to partial weighted MaxSAT (instances enter MaxSAT competition sets); Strix (explicit method) outperforms many symbolic tools on SYNTCOMP benchmarks; quantitative goals and approximations require maximum model counting and other reasoning beyond SAT to get useful, graded implementations.

AI-written summary · about

" chapters (12)

1. 0:00Intro
2. 3:08SAT-Based Model Checking
3. 5:11Bounded Model Checking for Safety Properties
4. 8:20Bounded Model Checking for Unbounded Verification
5. 9:41Bounded Model Checking: Impact
6. 10:59Beyond Verification: Synthesis
7. 14:40A Classic Example: Arbiter
8. 16:42Synthesis of Reactive Systems: Theoretical Developments
9. 19:30Synthesis of Reactive Systems: Tools
10. 22:42Bounded Synthesis for LTL Specifications
11. 27:15The Challenge of Writing Specifications
12. 32:10Example: A "Patient" Arbiter