Preprocessing of Alternating Automata for Language Emptiness Testing

on YouTube ↗15m

" summary

Preprocessing implements boolean simplifications plus two novel rewrites: basic simplification (structural hashing, absorption, removal of empty-state formulas) and shift transforms up-shifting and down-shifting. Up-shifting and purification rules reduce states by folding pure-state formulas, use a DFS back-edge heuristic to avoid nontermination, and run worst-case quadratic but practically linear. Down-shifting uses min-cut to pick safe merges and never increases states. Benchmarks on email-filtering and synthetic suites show faster emptiness checks, often enabling cases previously timed out; basic+up-shifting+antichain model checking gives the best results, while down-shifting helps IC3 but degrades antichain.

AI-written summary · about

" chapters (12)

1. 0:00Intro
2. 0:22Problem and Motivation
3. 1:27Symbolic Alternating Finite Automato
4. 3:45Removing Final States
5. 5:16Impact of basic simplification on model checking performance
6. 7:13Main contribution to preprocessing Basic simplification is successful but still a common sense
7. 10:05Up-shifting pure formula
8. 10:17WRONG: up-shifting impure formula
9. 10:55GOOD: up-shifting purified formula
10. 11:10Preventing nested substitution
11. 13:03Down-shifting Reverse operation to up-shifting.
12. 14:12The code