Module 5 — Well-Founded Relations & Ranking

Well-founded orders and termination proofs. Use ranking functions to prove liveness properties and show that every execution path eventually reaches a goal state.

Katas in this module (3)

• Kata 5.1 — A Descent That Has to End
• Kata 5.2 — Find the Ranking Function
• Kata 5.3 — The Bound Is the Rank's Maximum

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