Module 9 — Kripke Structures

Kripke structures as the semantic foundation of model checking. Map RTL state machines to Kripke models and relate LTL and CTL satisfaction to paths in the state graph.

Katas in this module (3)

• Kata 9.1 — The Design Is a Kripke Structure
• Kata 9.2 — A Total Transition Relation
• Kata 9.3 — Atomic Propositions and the Trace

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