Module 4 — Monotone Functions & Fixed-Point Theory

Tarski's fixed-point theorem and Kleene iteration. How reachability sets, invariants, and μ-calculus formulas are computed as fixed points of monotone operators.

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