Certification for \(\mu \)Calculus with Winning Strategies
 1 Citations
 458 Downloads
Abstract
We define memoryefficient certificates for \(\mu \)calculus model checking problems based on the wellknown correspondence between \(\mu \)calculus model checking and winning certain parity games. Winning strategies can be independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning strategies are computed by fixpoint iteration following the naive semantics of \(\mu \)calculus. We instrument the usual fixpoint iteration of \(\mu \)calculus model checking so that it produces evidence in the form of a winning strategy; for a formula \(\phi \) with fixed alternation depth, these winning strategies can be computed in polynomial time in S and in space \(O(S^2 {\phi }^2)\), where S is the size of the state space and \(\phi \) the length of the formula \(\phi \). On the technical level our work yields a new, simpler, and immediate constructive proof of the correspondence between \(\mu \)calculus and parity games. A prototypical implementation of a \(\mu \)calculus model checker generating these certificates has been developed.
Keywords
Model Check Linear Temporal Logic Label Transition System Computation Tree Logic Positional Strategy1 Introduction
We address the problems (1) of constructing concise certificates for \(\mu \)calculus model checking problems, and (2) for efficiently and independently checking these certificates by means of a trustworthy checker. Our main result here is an effective and low overhead instrumentation of the usual fixpoint iteration of \(\mu \)calculus model checking [3] for generating certificates that are independently checkable in low polynomial time.
There are a number of results and algorithms for constructing witnesses and counterexamples of various forms for different sublogics, including \( LTL \), \( ACTL \), \( CTL \), \( CTL ^*\), or the \(\mu \)calculus [1, 6, 7, 14, 24, 27, 33, 34]. For example, for linear temporal logic (\( LTL \)) restricted to the temporal operators F, U and X, a positive certificate can be given by a finite path. Model checkers for \( CTL ^*\) (for example, SMV) are capable of generating counterexamples [7] in the form of a lasso; that is, infinite sequences of states \(s_0, \dots {}, s_i, (s_{i+1}, \dots {}, s_k)^\omega \) which end up repeating periodically after some prefix of length i. Whereas lassoshaped sequences refute properties assumed for all possible paths, they fail, for example, in falsifying conjectured existence of certain paths. Witnesses for full \( CTL \) have been proposed by Shankar and Sorea [27, 29]. These results are based on a symbolic representation of witnesses that enables the extraction of explicit witnesses (and counterexamples) for full \( CTL \) model checking.
Local model checking procedures for determining whether finitestate systems have properties expressible in the \(\mu \)calculus incrementally construct tableau proofs [8, 31, 35]. These tableaux can be proofchecked independently, but the size of the constructed tableaux may grow exponentially in the number of states of the underlying transition system. Based on the tableau method of local \(\mu \)calculus model checking, Kick [18] proposes an optimized construction by identifying isomorphic subproofs. Namjoshi [20] introduces the notion of a certifying model checker that can generate independently checkable witnesses for properties verified by a model checker. He defines witnesses for properties of labelled transition systems expressed in the \(\mu \)calculus based on parity games over alternating tree automata. These developments rely on \(\mu \)calculus signatures [32] for termination, and are also based on the correspondence between \(\mu \)calculus model checking with winning parity games [12].
The developments in this paper can certify full \(\mu \)calculus model checking problems. Moreover, in order to certify that a given formula does not hold for some state, the result of checking the dual formula (cf. Lemma 1) is certified instead. In this way, certificates of the dual formula may be regarded as generalized counterexamples of the original formula.
Our approach of instrumenting \(\mu \)calculus model checking fixpoint iteration with the computation of witnesses, including the underlying notion and algebra of partial winning strategies, is novel. Moreover, in contrast to the previous work on local \(\mu \)calculus model checking, the witnesses generated by our global model checking algorithm are rather spaceefficient, as they can be represented in space in \(O(S^2 {\phi }^2)\), where S is the size of the state space and \(\phi \) is the length of the formula \(\phi \).
Our constructions build on the wellknown equivalence of model checking for the \(\mu \)calculus with winning corresponding parity games [12, 13, 34]. Because of the determinacy of parity games (see [19]), players of these games may restrict themselves to considering memoryless strategies only. In particular, there are no draws and exactly one of the players has a winning strategy for each vertex of the game graph. Algorithms for generating witnesses for players of parity games and their complexity are described by Jurdziński [17].
On the technical level our work can be seen as a new, simpler, and immediately constructive proof of the correspondence between \(\mu \)calculus and parity games. Winning strategies are computed by fixpoint iteration following the naive semantics of \(\mu \)calculus. No complex auxiliary devices such as signatures [32] or alternating automata [12] are needed. It should be possible to instrument existing implementations (such as the one integrated in the PVS theorem prover [23]) of \(\mu \)calculus based on fixpoint iteration to generate these certificates.
Roadmap. This paper is structured as follows. In Sects. 2 and 3 we summarize some standard developments for the \(\mu \)calculus in order to keep the paper selfcontained. Section 3 also contains a low polynomialtime checker for certificates which is inspired by the standard algorithm for checking for nonemptiness of Streett automata. Section 4 elaborates the correspondence between \(\mu \)calculus and winning parity games and in particular contains a new constructive proof of the correspondence (Theorem 2). Section 5 provides the technical details, first, of the central notion of partial winning strategies, and, second, for instrumenting the usual \(\mu \)calculus fixpoint iteration with the computation of partial winning strategies. For ease of exposition of this algorithm, we choose systems of equations as an alternative representation of \(\mu \)calculus formulas. The corresponding implementation of a witnessgenerating \(\mu \)calculus model checker is presented in Sect. 6, and the feasibility of our approach is demonstrated by means of selected benchmark examples. Concluding remarks, including further applications of our technical results on witnessgeneration and checking, are presented in Sect. 7.
An earlier version of this paper, without implementation and the use of equation systems, has been presented at the VeriSure 2013 workshop (associated with CAV 2013) [16].
2 Syntax and Semantics
We assume variables \(X\in {\mathcal {X}}\), propositions \(p \in {\mathcal {P}}\), and actions \(a \in {\mathcal {A}}\).
2.1 \(\mu \)Calculus Formulas
Definition 1
The set of free variables \({ FV }(\phi ) \subseteq {\mathcal {X}}\), the size \(\phi \) of a formula, and the substitution \(\phi [Z:=\psi ]\) of formula \(\psi \) for any free occurrence \(Z \in { FV }(\phi )\) are defined in the usual way. Note that negation is allowed for propositions only, hence all syntactically valid formulas are monotonic in their free variables and no considerations of polarity need to be taken into account.
The notations \({ Q }\in \{\mu ,\nu \}\), \({ M }\in \{[a], \langle a\rangle \,\, a \in {\mathcal {A}}\}\), \(* \in \{\wedge , \vee \}\) are used to simplify inductive definitions.
Fix a transition system T and put \(S=\mathcal S(T)\). For \(\eta \) a finite partial function from \({\mathcal {X}}\) to \(2^S\) with \({ FV }(\phi ) \subseteq \text {dom}(\eta )\) we define \(\llbracket {\phi }\rrbracket {\eta } \subseteq S\) as in Fig. 1.
Proposition 1
\(\llbracket {{ Q }X.\phi }\rrbracket {\eta } = \llbracket {\phi [X:={ Q }X.\phi ]}\rrbracket {\eta }\).
Therefore, in case S is finite, the iterative algorithm in Fig. 2 computes \(\llbracket {\phi }\rrbracket {\eta }\).
Proposition 2
\(\llbracket {\phi }\rrbracket {\eta } = sem (\phi ,\eta )\).
Lemma 1
2.2 Ordered Systems of Equations
We now use an alternate representation of \(\mu \)calculus formulas considering them to be an ordered system of equations [26]. Under this point of view, a formula \(\phi \) is represented by a set of equations \((X=\phi _X)_{X \in {\mathcal {X}}}\), with one formula \(\phi _X\) for each variable X occurring in \(\phi \), together with a strict partial order of variables \(\succ \,\,\subseteq {\mathcal {X}}\times {\mathcal {X}}\).
To do this, we assume that every fixpoint quantifier binds a different variable; if needed this can be ensured by \(\alpha \)renaming. For example, we replace \(\mu X.X \wedge \nu X.X\) with \(\mu X.X \wedge \nu Y.Y\). For each variable X we denote \(q_X\in \{\mu ,\nu \}\) the kind of quantifier that it stems from.
We then replace each fixpoint formula by the (unique) variable it introduces and thereafter give for each fixpoint formula a defining equation. Formally, for any subformula \(\psi \) of \(\phi \) let \(\hat{\psi }\) denote the formula obtained by replacing each fixpoint subformula by the variable it binds. The equation system then contains one equation \(X=\hat{\psi }\) for each fixpoint subformula \(QX.\psi \), with \(q_X=Q\).
In parallel, we build the strict partial order \(\succ \) of variables. For each variable X bound by a fixpoint subformula \(QX.\psi \) and each variable Y bound by a fixpoint subformula of \(\psi \), i.e. all Y bound below X, we set \(X \succ Y\).
In case the formula does not start with a quantifier, a fresh variable needs to be introduced and bound to the formula in the first place. Since this variable is not used anywhere else, either \(\mu \) or \(\nu \) can be chosen.
This representation is advantageous for our implementation as it avoids the need for syntactic substitution of fixpoint formulas for their variables.
Lemma 2
Let \(\phi \) be a formula and let X be the toplevel variable of the representation of \(\phi \) as an equation system. Then \(\llbracket {X}\rrbracket {}=\llbracket {\phi }\rrbracket {}\).
Remark. It is possible to extend the semantics to the case where the relations \(\mathop {\longrightarrow }\limits ^{a}\) are not necessarily total: The semantics carries over without changes.
The restriction to total relations is a standard one and it is vindicated by the following translation from the general case to the one treated here:
Given a LTS T with a not necessarily total \(\mathop {\longrightarrow }\limits ^{a}\) we build a new LTS \(T'\) with an additional distinguished state, \(\mathcal S(T') = \mathcal S(T)\cup {\{\mho \}}\), then extend \(\mathop {\longrightarrow }\limits ^{a}\) with extra edges from any state to \(\mho \) (\(\mathop {\mathop {\longrightarrow }\limits ^{a}}\nolimits _{{T'}} = \mathop {\mathop {\longrightarrow }\limits ^{a}}\nolimits _{T} \cup \{\, (s,\mho ) \mid s \in \mathcal S(T') \,\}\)) so that \(\mathop {\mathop {\longrightarrow }\limits ^{a}}\nolimits _{{T'}}\) now is total. We also add a proposition \(p_\mho \) which is true at state \(\mho \) and nowhere else.
3 Parity Games

a (finite or infinite) set of positions \( Pos \) partitioned into proponent’s (Player 0) and opponent’s (Player 1) positions: \( Pos = Pos _0 + Pos _1\);

a lefttotal edge relation \({\rightarrow }\subseteq Pos {\times } Pos \);

a function \(\varOmega \in Pos \rightarrow \mathbb {N}\) with a finite range; we call \(\varOmega (p)\) the priority of position p.
The players move a token along the edge relation \(\rightarrow \). When the token is on a position in \( Pos _0\) then proponent decides where to move next and likewise for opponent.
In order to formalize the notion of “to decide” we must introduce strategies. Formally, a strategy for a player \(i\in \{0,1\}\) is a function \(\sigma \) that for any nonempty string \(\vec p = p(0)\ldots p(n)\) over \( Pos \) such that \(p(k)\rightarrow p(k+1)\) for \(k=0 \ldots n1\) and \(p(n)\in Pos_i\) associates a position \(\sigma (\vec p) \in Pos \) such that \(p(n) \rightarrow \sigma (\vec p)\).
The play is won by proponent (Player 0) if the largest number that occurs infinitely often in the sequence \(\varOmega ( play (p,\sigma _0,\sigma _1))\) is even and it is won by opponent if that number is odd. Note that \(\varOmega ()\) is applied componentwise and that a largest priority indeed exists since \(\varOmega \) has finite range.
Player i wins from position p if there exists a strategy \(\sigma _i\) for Player i such that for all strategies \(\sigma _{1i}\) of the other player (Player \(1i\)) Player i wins \( play (p,\sigma _0,\sigma _1)\). We write \(W_i\) for the set of positions from which Player i wins.
A strategy \(\sigma \) is positional if \(\sigma (p(0)\dots {}p(n))\) only depends on p(n). Player i wins positionally from p when the above strategy \(\sigma _i\) can be chosen to be positional.
The following is a standard result [19].
Theorem 1
Every position p is either in \(W_0\) or in \(W_1\) and Player i wins positionally from every position in \(W_i\).
Example 1
Figure 3 contains a graphical display of a parity game. Positions in \( Pos _0\) and \( Pos _1\) are represented as circles and boxes, respectively, and labelled with their priorities. Formally, \( Pos =\{a,b,c,d,e,f,g,h,i\}\); \( Pos _0=\{b,d,f,h\}\); \( Pos _1=\{a,c,e,g,i\}\); \(\varOmega (a)=3\), ..., and \({\rightarrow }=\{(a,b), (b,f),\dots \}\).
In the right half of Fig. 3 the winning sets are indicated and corresponding positional winning strategies are given as fat arrows. The moves from positions that are not in the respective winning set are omitted but can of course be filledin in an arbitrary fashion.
3.1 Certification of Winning Strategies
Given a parity game with finitely many positions, presented explicitly as a finite labelled graph, and a partition of \( Pos \) into \(V_0\) and \(V_1\) we are now looking for an easytoverify certificate as to the fact that \(V_0 = W_0\) and \(V_1 = W_1\).
In essence, such a certificate will consist of a positional strategy \(\sigma _i\) for each Player i such that i wins using \(\sigma _i\) from every position p in \(V_i\). Clearly, this implies \(V_i=W_i\) and the above theorem asserts that in principle such certificates always exist when \(V_i=W_i\). However, it remains to explain how we can check that a given positional strategy \(\sigma _i\) wins from a given position p.
We first note that for this it is enough that it wins against any adversarial positional strategy because the “optimal” counterstrategy, i.e., the one that wins from all adversarial winning positions is positional (by Theorem 1). Thus, given a positional strategy \(\sigma _i\) for Player i we can remove all edges from positions \(p'\in Pos _i\) that are not chosen by the strategy and in the remaining game graph look for a cycle whose largest priority has parity \(1i\) and is reachable from p. If there is such a cycle then the strategy was not good and otherwise it is indeed a winning strategy for Player i.
Naive enumeration of all cycles in the graph will result in having to check exponentially many cycles in the worstcase. However, the check can be performed in polynomial time [17], using the standard algorithm for nonemptiness of Streett automata [2] of which the problem at hand is actually an instance. This algorithm uses a decomposition of the graph into nontrivial strongly connected components (SCC).
If every reachable SCC only has positions whose priority has parity i then obviously the strategy is good for Player i. Next, if there is a reachable SCC where the highest priority has parity \(1i\), the strategy is bad, since this particular position can be reached infinitely often.
Otherwise, the highest priority in each SCC has parity i and of course player \(1i\) can win only if it is possible for them to avoid those nodes. Thus, we remove those nodes and decompose the resulting graph in SCCs again and start over.
For our implementation, we use a variant of this algorithm based on Dijkstra’s algorithm for SCC as presented by [9, 10]. In contrast to other efficient algorithms for this problem (such as [15]), it has the benefit of being onthefly and does not require precomputation of the parity game graph. The checking algorithm is described in more detail in Sect. 6.
Example 2
Likewise, adopting the viewpoint of Player 1, after removing the edges not taken by their strategy we obtain
4 GameTheoretic Characterization of \(\mu \)Calculus
Fix an LTS T and a \(\mu \)calculus formula \(\phi \). We first translate \(\phi \) into an equation system (as explained in Sect. 2.2) over the variables \({\mathcal {X}}\) written as \(X=\phi _X\) where \(X\in {\mathcal {X}}\) and \(q_X\in \{\mu ,\nu \}\).

\(q_X=\mu \Rightarrow \varOmega (X)\) odd;

\(q_X=\nu \Rightarrow \varOmega (X)\) even;

\(X \succ Y\Rightarrow \varOmega (X)> \varOmega (Y)\).
If in addition \(\eta \) is an environment with \(\mathop {\text {dom}}(\eta )\subseteq {\mathcal {X}}\) we define the game \(G(T,\phi ,\eta )\) as follows:
The variables \(X\not \in \mathop {\text {dom}}(\eta )\) on the other hand are understood as abbreviations of the fixpoint formula they represent. Upon reaching such a position the fixpoint is unrolled and such unrolling is signalled by the priority \(\varOmega (X)\).
Example 3
Let \(\phi = \mu X.\, p \vee \langle a\rangle X \) which asserts that a state where p is true can be reached.
The priorities of the positions labelled (s, X), (t, X), (s, p) are 1; the priorities of the four other positions are 0.
Player 0 wins from every position except (s, p). The winning strategy moves to \((s,\langle a\rangle X)\) and then (t, X) and then (t, p). Note that a strategy that moves from \((s,\langle a\rangle X)\) to (s, X) loses even though it never leaves the winning set \(W_0\). Thus, in order to compute winning strategies it is not enough to choose any move that remains in the winning set.
Theorem 2
Fix a formula \(\phi _0\) and an environment \(\eta \).
If \(s \in \llbracket {\phi _0}\rrbracket {\eta }\) then proponent wins \(G(T,\eta )\) from \((s,\phi _0)\).
Before proving this, we note that the converse is in this case actually a relatively simple consequence.
Corollary 1
If proponent wins \(G(T,\eta )\) from \((s,\phi )\) then \(s \in \llbracket {\phi }\rrbracket {\eta }\).
Proof
Suppose that proponent wins \(G(T,\eta )\) from \((s,\phi )\) and \(s \not \in \llbracket {\phi }\rrbracket {\eta }\). We then have \(s \in \llbracket {\phi ^*}\rrbracket {\eta '}\) using Lemma 1 for the formal dualisation for formulas and complementation for environments. Thus, by the theorem, proponent wins \(G(T,\eta ')\) from \((s,\phi ^*)\). However, it is easy to see that a winning strategy for proponent in \(G(T,\eta ')\) from \((s,\phi ^*)\) is tantamount to a winning strategy for opponent in \(G(T,\eta )\) from \((s,\phi )\); so we get a contradiction using Theorem 1. \(\square \)
Proof
(of Theorem 2 ). The proof of Theorem 2 now works by structural induction on the equation system generated by \(\phi _0\). We note that this induction preserves the invariant \(\{\, X \mid X \succ Y, Y \in { FV }(\phi ) \,\} \subseteq \mathop {\text {dom}}(\eta )\), such that \(\llbracket {\phi }\rrbracket {\eta }\) is always welldefined.
For a variable X, there are three cases, the latter ones are the interesting ones, as X denotes a fixpoint there:
(i) \(X \in \mathop {\text {dom}}(\eta )\), then obviously \(G(T,\eta )\) agrees with \(\llbracket {X}\rrbracket {\eta }\).
Call the corresponding winning strategy \(\sigma \). We should prove that proponent also wins from (t, X). We move to \((t,\phi _X)\) and then play according to \(\sigma \). If we never reach a position \((t',X)\), then by the definition of \(G(T,\eta [X\mapsto U])\) we actually have won \(G(T,\eta )\).
The first time, if ever, that we reach a position \((t',X)\), we know by the definition of U that \(t' \in U\) and therefore we win \(G(T,\eta )\) from \((t',X)\), so we abandon \(\sigma \) and continue play according to the strategy embodied in the latter statement. This then ensures winning from (t, X) since finite prefixes do not affect the winning condition.
(iii) \(X \notin \mathop {\text {dom}}(\eta )\) and \(q_X=\nu \). Let \(U := \llbracket {X}\rrbracket {\eta }~(= \llbracket {\nu X.\phi _X}\rrbracket {\eta })\). We define a winning strategy for positions of the form (t, X) where \(t\in U\) as follows. First, we move (forcedly) to \((t,\phi _X)\). We know that \(t \in \llbracket {\phi _X}\rrbracket {\eta [X \mapsto U]}\) by unwinding so that, inductively, we have a strategy that allows us to either win right away, or move to another position \((t',X)\) where \(t' \in U\) and all priorities encountered on the way are smaller than the one of X due to the definition of priorities, and since all higher occurring priorities are bound in \(\eta \), thus not resulting in a loop.
We start over and unless we eventually do win right away at some point we would have seen the priority of X itself infinitely often which is the largest and even. \(\square \)
We remark that while the previous result is wellknown the proof presented here is quite different from the ones in the standard literature, e.g. [4], which use the ordertheoretic concept of signatures, also known as rankings. Those proofs are less compositional than ours, in the sense that they do not proceed directly by structural induction on formulas but rather on the global development of all the fixpoints.
It is essentially this new compositional proof which allows us to instrument the usual fixpoint iteration so as to compute winning strategies alongside as we now detail.
5 Computing Winning Strategies via Fixpoint Iteration
5.1 Fixpoint Iteration
It is wellknown that the fixpoint iteration in Fig. 2 computes \(\llbracket {\phi }\rrbracket {\eta }\) in the finite case. Our goal is to somehow instrument this algorithm so that it produces evidence in the form of a winning strategy. In instrumenting this algorithm to produce evidence in the form of a winning strategy it is not enough to simply compute the winning sets using \(\textsc {sem}(,)\) and then simply choose moves that do not leave the winning set. This is because of Example 3 which show that a strategy that never leaves the winning set may nonetheless be losing.
Instead we will use the construction from the proof of Theorem 2. Some care needs to be taken with the exact setup of the input and output data formats; in particular, our algorithm will return partial winning strategies (that win on a subset of the whole winning set) but only require sets of states (rather than partial winning strategies) as the values of free variables.
5.2 Partial Winning Strategies

STAR. If \(\varSigma (\phi ,s) = *\) then all immediate successors of \((\phi ,s)\) are in \(\text {dom}(\varSigma )\);

OR. If \(\varSigma (\phi ,s) = i \in \{1,2\}\) then \(\phi \) is of the form \(\phi _1 \vee \phi _2\) and \((\phi _i,s)\in \text {dom}(\varSigma )\);

DIA. If \(\varSigma (\phi ,s) = s' \in S\) then \(\phi \) is of the form \(\langle a\rangle \psi \) and \(s\,\mathop {\longrightarrow }\limits ^{a}\, s'\) and \((\psi ,s') \in \text {dom}(\varSigma )\).

WIN. Player 0 wins from all the positions in \(\text {dom}(\varSigma )\) and the obvious strategy induced by \(\varSigma \) is a winning strategy for Player 0 from those positions.
Lemma 3
\(\varSigma +\varSigma '\) is a partial winning strategy and \(\mathrm{dom}(\varSigma +\varSigma ') = \mathrm{dom}(\varSigma ) \cup \mathrm{dom}(\varSigma ') \)
Proof
A play following \(\varSigma +\varSigma '\) will eventually remain in one of \(\varSigma \) or \(\varSigma '\); this, together with the fact that initial segments do not affect the outcome of a game implies the claim. \(\square \)
5.3 Computing Winning Strategies by Fixpoint Iteration
Note how the fixpoint iteration in \(\textsc {iter}_X\) stops when the domain of the partial winning strategy does not change anymore. Since the greatest fixpoint for \(\nu X.\phi \) cannot be calculated from above in terms of winning strategies (which can only grow according to our definitions), the winning set (and thus, domain of the winning strategy) is computed using the set semantics \( sem (,)\) instead.
The following Lemma and Theorem are now immediate from these definitions and Lemma 3.
Lemma 4
\(\{\,s \,\, (\phi ,s) \in \mathrm{dom}({\textsc {sem}}(\phi )_{\eta })\,\} = \llbracket {\phi }\rrbracket {\eta }.\)
Theorem 3
\({\textsc {sem}}(\phi )_{\eta }\) is a winning strategy for \(G(T,\phi ,\eta )\).
Proposition 3
Given a formula \(\phi \) with fixed alternation depth, \({\textsc {sem}}(\phi )_{\eta }\) can be computed in polynomial time in S and in space \(O(S^2 {\phi }^2)\), where S is the size of the state space and \(\phi \) the length of the formula \(\phi \).
Proof
The computation of \({\textsc {sem}}(\phi )_{\eta }\) follows the one of \(\llbracket {\phi }\rrbracket {\eta }\) hence the time bound. Just like in the usual implementations of fixpoint iteration one only needs to remember the result of the last iteration. Storing a single partial winning strategy requires space \(O(S^2 \phi )\) (associating at most one state to each pair of state and subformula) and the recursion stack during traversal of subformulas is limited by \(\phi \) thus requiring us to store \(O(\phi )\) partial winning strategies at any one time. This yields the announced space bound. \(\square \)
6 Implementation and Evaluation
We have developed an implementation [22] of both computation and checking of certificates in OCaml. Winning strategies are kept abstract, only exposing an assoc function to look up a possible move given a model and particular state. Computation of winning strategies happens by fixpoint iteration using a recursive function, just like presented in Sect. 5.3.
Two algorithms for checking certificates are implemented: “Check”, a naive, recursive one with worstcase exponential time, and “Check SCC”, a more intricate one using stronglyconnected components to detect cycles. Both algorithms operate onthefly and do not need to precompute or even keep the parity game graph in memory.
The algorithm “Check SCC” is a variant of Dijkstra’s algorithm for detecting strongly connected components and can be found in [9, 10].
This algorithm works as follows [25]: During a depthfirst search of the graph, we keep a stack of strongly connected components that have been found. Upon finding an edge back into a SCC that closes a cycle, we merge all SCC that are part of the cycle, since using the cycle we can now move from every SCC into any other, i.e. their union is actually one SCC.
We provide three benchmarks that give insight into the algorithms at work.
The “Flower” benchmark is a parity game (from [5]) translated into a \(\mu \)calculus formula, which shows the exponential runtime of fixpoint iteration for \(\mu \)calculus. However, the certificates can be checked in polynomial time.
The “Circle” benchmark measures the overhead of the algorithms. It consists of a single cycle that needs to be traversed to check for a reachability property. In this case, runtime is linear, and checking is very fast.
Runtimes on a AMD Phenom II X4 920 (2.80 GHz)
Problem  States  sem [s]  SEM [s]  Check [s]  Check SCC [s] 

Flower 8  16  0.179  0.203  0.009  0.040 
Flower 10  20  3.166  1.960  0.071  0.419 
Flower 12  24  32.269  11.688  0.287  2.061 
Flower 14  28  320.931  61.733  1.298  10.829 
Flower 16  32  3196.043  326.666  6.131  58.871 
Circle 100  100  0.003  0.001  0.001  0.001 
Circle 1000  1000  0.109  0.018  0.005  0.006 
Circle 10000  10000  15.763  3.398  0.054  0.057 
Circle 100000  100000  2027.584  811.041  0.581  0.582 
Braid 6  12  0.001  0.005  1.282  0.009 
Braid 8  16  0.002  0.003  31.062  0.013 
Braid 10  20  0.002  0.006  711.002  0.020 
Braid 100  200  0.663  0.993  —  3.674 
7 Conclusion
Our main result is an effective and low overhead instrumentation of the usual fixpoint iteration of \(\mu \)calculus model checking [3] for generating certificates or counterexamples that are independently checkable in low polynomial time. The notion of partial winning strategies is central to our developments and also seems to be novel.
We have implemented our witnessgenerating algorithms and demonstrated the feasibility of our approach by means of a collection of benchmark examples. For simple formulas, manual inspection of the generated certificates yields counterexamples similar to those generated by SMV, but algorithmic approaches for extracting explicit counterexamples in general needs further investigation.
There are numerous applications for our certifying \(\mu \)calculus model checker. In particular, it should be possible to generate checkable certificates for the bisimulation between programs and for model checking problems for both linear time temporal logics and computation tree logics [11] as the basis for assurance cases and certification arguments for safetycritical systems. Moreover, certificates for \(\mu \)calculus model checking might also be used as the basis of symmetric abstractionrefinementbased model checking engines for the full \(\mu \)calculus based on refining overapproximations using spurious counterexamples and relaxing underapproximations using dubious witnesses along the lines of [29, 30], for sending code together with proofs of arbitrary safety and liveness properties, which are then checked by code consumers according to the proofcarrying code paradigm of [21], and for synthesizing correctbyconstruction controllers from these certificates [30].
Our developments may also form the underpinning for a sound integration of \(\mu \)calculus model checking into other verification systems such as PVS [23]. Using Shankar’s kernel of truth [28] approach, which is based on checking the verification and on verifying the checker, certificates are generated using an untrusted implementation of our \(\mu \)calculus model checking algorithms, and certificates are then checked by means of an executable PVS function, which itself is verified in a trusted kernel of PVS.
Footnotes
 1.
Lefttotal means for all \(s\in S\) there exists \(s' \in S\) with \(s \rightarrow s'\).
References
 1.Biere, A., Zhu, Y., Clarke, E.: Multiple state and single state tableaux for combining local and global model checking. In: Olderog, E.R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 163–179. Springer, Heidelberg (1999)CrossRefGoogle Scholar
 2.Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in \(n\) log \(n\) symbolic steps. Formal Methods Syst. Des. 28(1), 37–56 (2006)CrossRefzbMATHGoogle Scholar
 3.Bradfield, J., Stirling, C.: Modal mucalculi. Stud. Logic Pract. Reasoning 3, 721–756 (2007)CrossRefzbMATHGoogle Scholar
 4.Bradfield, J., Stirling, C.: Modal logics and mucalculi: an introduction. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 293–330. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
 5.Buhrke, N., Lescow, H., Vöge, J.: Strategy construction in infinite games with streett and rabin chain winning conditions. In: Margaria, T., Steffen, B. (eds.) TACAS. LNCS, vol. 1055, pp. 207–225. Springer, Heidelberg (1996)CrossRefGoogle Scholar
 6.Clarke, E., Jha, S., Lu, Y., Veith, H.: Treelike counterexamples in model checking. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 19–29. IEEE (2002)Google Scholar
 7.Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of the 32nd Annual ACM/IEEE Design Automation Conference, pp. 427–432. ACM (1995)Google Scholar
 8.Cleaveland, R.: Tableaubased model checking in the propositional mucalculus. Acta Informatica 27(8), 725–747 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
 9.DuretLutz, A.: Contributions à l’approche automate pour la vérification de propriétés de systèmes concurrents. Ph.D. thesis, Université Pierre et Marie Curie (Paris 6) July 2007. https://www.lrde.epita.fr/~adl/th.html
 10.DuretLutz, A., Poitrenaud, D., Couvreur, J.M.: Onthefly emptiness check of transitionbased streett automata. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 213–227. Springer, Heidelberg (2009)CrossRefGoogle Scholar
 11.Emerson, E., Jutla, C., Sistla, A.: On modelchecking for fragments of \(\mu \)calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)CrossRefGoogle Scholar
 12.Emerson, E., Jutla, C.: Tree automata, mucalculus and determinacy. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS 1991), pp. 368–377. IEEE (1991)Google Scholar
 13.Grädel, E.: Back and forth between logic and games. In: Apt, K., Grädel, E. (eds.) Lectures in Game Theory for Computer Scientists, pp. 99–138. Cambridge University Press, Cambridge (2011)CrossRefGoogle Scholar
 14.Gurfinkel, A., Chechik, M.: Prooflike counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160–175. Springer, Heidelberg (2003)CrossRefGoogle Scholar
 15.Henzinger, M.R., Telle, J.A.: Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: Karlsson, R., Lingas, A. (eds.) SWAT 1996. LNCS, vol. 1097, pp. 16–27. Springer, Heidelberg (1996)CrossRefGoogle Scholar
 16.Hofmann, M., Rueß, H.: Certification for \(\mu \)calculus with winning strategies. ArXiv eprints, January 2014Google Scholar
 17.Jurdziński, M.: Algorithms for solving parity games. In: Apt, K., Grädel, E. (eds.) Lectures in Game Theory for Computer Scientists, pp. 74–98. Cambridge University Press, Cambridge (2011)CrossRefGoogle Scholar
 18.Kick, A.: Generation of counterexamples for the \(\mu \)calculus. Technical report iratr199537, Universität Karlsruhe, Germany (1995)Google Scholar
 19.Martin, D.A.: Borel determinacy. Ann. Math. 102(2), 363–371 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
 20.Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)CrossRefGoogle Scholar
 21.Necula, G.: Proofcarrying code. In: Proceedings of the 24th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 106–119. ACM (1997)Google Scholar
 22.Neukirchen, C.: Computation of winning strategies for \(\mu \)calculus by fixpoint iteration. Master’s thesis, LudwigMaximiliansUniversität München, November 2014Google Scholar
 23.Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)Google Scholar
 24.Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001)CrossRefGoogle Scholar
 25.Renault, E., DuretLutz, A., Kordon, F., Poitrenaud, D.: Three SCCbased emptiness checks for generalized Büchi automata. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 668–682. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 26.Seidl, H.: Fast and Simple Nested Fixpoints. Universität Trier, Mathematik/Informatik, Forschungsbericht 9605 (1996)Google Scholar
 27.Shankar, N., Sorea, M.: Counterexampledriven model checking (revisited version). Technical report SRICSL0304, SRI International (2003)Google Scholar
 28.Shankar, N.: Rewriting, inference, and proof. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 1–14. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 29.Sorea, M.: Dubious witnesses and spurious counterexamples. UK Model Checking Days, York (2005). http://www.cs.man.ac.uk/~msorea/talks/york.pdf
 30.Sorea, M.: Verification of realtime systems through lazy approximations. Ph.D. thesis, University of Ulm, Germany (2004)Google Scholar
 31.Stirling, C., Walker, D.: Local model checking in the modal mucalculus. In: Díaz, J., Orejas, F. (eds.) TAPSOFT 1989. LNCS, vol. 351, pp. 369–383. Springer, Heidelberg (1989)Google Scholar
 32.Streett, R.S., Emerson, E.A.: The propositional mucalculus is elementary. In: Paredaens, J. (ed.) Automata, Languages and Programming. LNCS, vol. 172, pp. 465–472. Springer, Heidelberg (1984)CrossRefGoogle Scholar
 33.Tan, L., Cleaveland, W.R.: Evidencebased model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002)CrossRefGoogle Scholar
 34.Vardi, M., Wilke, T.: Automata: from logics to algorithms. In: WAL, pp. 645–753 (2007)Google Scholar
 35.Winskel, G.: A note on model checking the modal \(\nu \)calculus. Theor. Comput. Sci. 83(1), 157–167 (1991)CrossRefzbMATHGoogle Scholar