Module 8 — ω-Automata, Büchi & Fairness

Büchi automata, ω-regular languages, and fairness constraints. Specify and verify infinite-execution liveness properties over hardware that runs forever.

Katas in this module (3)

• Kata 8.1 — The Run That Loops Forever
• Kata 8.2 — Infinitely Often
• Kata 8.3 — Fairness Rescues the Proof

Part of Mathematical Foundations of Model Checking on formal.org.