Module 10 — Computation Tree Logic

CTL operators and their fixed-point semantics. Verify EF, AG, AF, and EU properties against the Kripke model of an RTL design using symbolic BDD-based model checking.

Katas in this module (3)

• Kata 10.1 — AG and EF
• Kata 10.2 — AX and EX at a Branching State
• Kata 10.3 — The AG / EF Duality

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