Embedded Systems Group (ES)

Model Checking μ-Calculus and CTL

This tool can be used to check whether a Kripke structure satisfies a μ-calculus or CTL formula. To this end, the tool first applies global model checking to compute all states that satisfy the given formula and then checks whether all initial states are included in this set. As an alternative to this global model checking, a local model checking proof tree is generated provided that the formula is in guarded normal form and alternation free.

The CTL operators are thereby considered as macro operators of the μ-calculus that are accordingly replaced during model checking. The fixpoint calculations are explained step-by-step. For the syntax of CTL and the μ-calculus formulas, see the Quartz reference card under section proof goals/specifications (or guess it by the example given below as for the Kripke structure). In particular, note that you have to put a blank between CTL path quantifiers and temporal operators like "E G E X a". We also formatted the model checking exercises of previous exams for this tool.

The syntax for the state transition systems (the Kripke structures) should be obvious: states are integers 0,...,n as listed in the labels, and the labels are of the form i:x1,...,xm to denote that variables x1,...,xm hold in state i. Transitions are lists of the form i->j denoting a transition from state i to state j.

global model checking
local model checking
converting model checking to parity game (under development)