# 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.

 vars a,b; init 0; labels 0:; 1:a; 2:; 3:a,b; 4:; 5:a; 6:a; 7:; 8:a; 9:b; transitions 0->1; 0->3; 0->8; 1->2; 2->2; 3->4; 4->5; 5->6; 6->7; 7->7; 8->9; 9->8; 9->9; // states with infinite outgoing paths nu x. <>x; // states with infinite "a"-paths nu x.(a&<>x); // states that have a path to an "a"-state nu x.(a|<>x); // states with a possible finite path to an "a"-state mu x.(a&<>x); // the following is just "a" since <>false is false mu x.(a|<>x); // states that can be reached from an "a" state mu x.(a|<:>x); // states where after some time always "a" holds mu y. ((nu x.(a&<>x)) | <>y); // states with a path where ∞ often "a" holds nu y. <>(mu x.(y & a | <>x)); // CTL formulas E F E G (a|b); E G A F a; A[a WB b] global model checking local model checking converting model checking to parity game (under development)