Evidence Extraction from Parameterised Boolean Equation Systems Wieger Wesselink and Tim A.C. Willemse Eindhoven University of Technology, Eindhoven, The Netherlands {j.w.wesselink,t.a.c.willemse}@tue.nl Abstract Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples. 1 Introduction The complexity of the average computer-controlled system has reached a point at which it has become impossible to fully understand a system. By modelling a system and subsequently analysing whether the crucial safety and liveness requirements of the system are upheld, some confidence in the system’s correctness can be obtained. The complexity of the average system, however, precludes that such an analysis can be conducted manually. Model checking is an automated technique for assessing whether a requirement holds for a model of a system. This technique requires as input a mathematical description of the behaviour of a system, often given in terms of (a high-level description of) a Kripke Structure or Labelled Transition System, and a logical formula, often given in some appropriate temporal logic. By feeding both artefacts to a tool, colloquially referred to as the model checker, the yes or no verdict produced by the tool states whether (the model of) the system meets the requirement. Knowing that a system fails to meet a requirement, however, does not help to improve on the system design. For that, richer feedback in the form of evidence (i.e. a counterexample or a witness) of the model checker is required. Depending on the logic that is required to perform the verification, however, it is not always clear what type of evidence must be extracted from a negative model checking exercise. While for linear time logic (LTL), a lasso, or a prefix of a lasso typically suffices, the problem becomes more pronounced for branching time logics such as CTL, CTL∗ or the modal µ-calculus. The reason for this is that the formulae over such logics are essentially interpreted over infinite computation trees. In this paper, we describe how evidence can be constructed for an extension of the modal µ-calculus, viz. the first-order modal µ-calculus [12], within the context of the analysis toolset mCRL2 [5]. This logic extends the standard modal µ-calculus by adding first-order quantification and parameterised fix- points. We draw inspiration from previous work [7] explaining how, in theory, evidence can be extracted from decision problems encoded in the logic of Least Fixed Point (LFP). The main idea is that a coun- terexample or witness for the model checking problem is a ‘submodel’ of the original model, which can be used to reconstruct the proof of the original negative model checking result. ARQNL 2018 86 CEUR-WS.org/Vol-2095 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse One obstacle in applying the techniques outlined for LFP is that the model checker in mCRL2 uses parameterised Boolean equation systems (PBESs) [13] to solve the model checking problem. While LFP and PBESs have much in common, they differ in exactly those aspects used for evidence extrac- tion. Our first contribution is therefore to show how this problem can effectively be overcome without changing the underlying theory for PBESs. Our second contribution is an implementation of our so- lution, illustrating the feasibility and appeal of the approach. As far as we are aware, ours is the first work demonstrating the feasibility of constructing diagnostics in this way for the full (first-order) modal µ-calculus with arbitrary alternation. Related Work. We refer to Busard’s PhD thesis [3] for a thorough overview of literature on generating diagnostics for model checking for the modal µ-calculus, but also other logics such as CTL and epis- temic logics; we here give a concise overview of the most relevant related works. There are several works that address the problem of constructing diagnostics for the modal µ-calculus model checking problem. In [20], diagnostics is presented as a game played on the model checking game for the modal µ-calculus. A related approach is given by [14] who essentially suggests to generate tableaux as wit- nesses to the model checking problem. In [17], diagnostics are defined as explanations for the truth values of the underlying Boolean equation system that is used to solve a model checking problem for the alternation-free fragment of the modal µ-calculus. This technique is closely related to [20]. In contrast to our work, these approaches require the user conducting the verification to understand the underlying mechanism for conducting the verification. Finally, in the work by Tan and Cleaveland [21], which can be seen as a generalisation of [17], evidence is presented as information extracted from (dec- orated) support sets. These are closely related to the proof graphs underlying [6] and the idea of using decorations is reminiscent of the idea underlying [7] to allow first-order relations in proof graphs. Outline. We give a cursory overview of the necessary background in Section 2; i.e. we briefly address the underlying theory for modelling data and system behaviours, the first-order modal µ-calculus, and we formalise the model checking problem. In Section 3, we introduce PBESs, we explain how the model checking problem can be converted to the problem of solving a PBES, and we illustrate the problem of extracting evidence from a PBES encoding a model checking problem. In Section 4, we illustrate how we can extract evidence from a PBES by modifying the encoding of the model checking problem and in Section 5, we illustrate how our solution works on practical examples. We conclude in Section 6. 2 Preliminaries Our work is set in a context in which we rely on abstract data types to describe (and reason about) data. That is, we assume a given algebraic specification S = hS, Σ, Ei where S is a set of sorts, Σ is a family of operation(s) and E is a family of equations. As a convention, we write data sorts using letters D, E, etcetera. We have a set D of data variables, with typical elements d, d1 , . . . The semantics of an algebraic specification S = hS, Σ, Ei is given by a many-sorted Σ-algebra con- sisting of data domains corresponding to S and operations corresponding to Σ, satisfying the identities of E. We here adopt an initial algebra semantics point of view. For every sort D, E,. . . , we denote the domains they represent by D, E,. . . . For a closed term t of a given sort, say D (denoted t:D), we assume an interpretation function [[t]] that maps t to a value of D it represents. For open terms we use a data environment ε that maps each variable from D to a value of the proper domain. If we wish to indicate which variables may occur freely within a term t, we add these as ‘parameters’ to t; i.e. we write t(d) to indicate that d is the only free variable in t. The interpretation of an open term t, denoted as [[t]]ε is obtained in the standard way. We write ε[d 7→ v] for the environment that maps variable d to value v and all other variables d 0 are mapped to ε(d 0 ). 2 87 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse We require the presence of a sort B representing the Booleans B = {true, false}. For convenience we also assume the existence of the sort N representing the natural numbers N. For both sorts we assume the usual operators are available and we do not write constants or operators in the syntactic domain any different from their semantic counterparts. For example, the Boolean value true is represented by the constant true and the value false is represented by the constant false. The syntactic operator ∧ :B × B → B corresponds to the usual, semantic conjunction ∧ :B × B → B; etcetera. Note that for readability, and without loss of generality, we use a single—possibly compound—data type in our definitions and formal statements. 2.1 Processes The behaviours of software and hardware systems can be adequately modelled using labelled transition systems (LTSs). Modelling languages, such as process algebras and I/O-automata, provide language constructs such as conditional choice, interleaving parallelism and sequential composition through which one can compactly specify such systems. A useful normal form to which many such specifi- cations can be compiled automatically is the Linear process equation (LPE) format, see e.g. [11]. An LPE typically models the (global) state of a (software or hardware) system by means of a finite vector of formal data parameters, ranging over adequately chosen sorts. The behaviours are described by a non-deterministic choice (denoted by the + operator) among rules taken from a finite set of condition- action-effect rules, prescribing under which condition an action (modelling a message exchange or an event) is enabled, leading to an update of the vector of formal parameters. A formal definition of an LPE, employing syntax that stays true to its process-algebraic heritage, is given below. Definition 1. A linear process equation is an equation of the following form: L(dL :DL ) = + { ∑ ca (dL , ea ) → a( fa (dL , ea )) · L(ga (dL , ea )) | a ∈ A ct} ea :Ea The sort DL is used to represent the set of states and variable dL represents a state; a is a (typed) action label taken from a finite set A ct of (typed) action labels. Each action label a is associated with a local variable ea of sort Ea , an expression ca :B, which acts as a condition, an expression fa :Da , which yields an argument emitted along a when executed, and an operation ga :DL , which yields a new state. We require that dL and eL are the only free variables occurring in these expressions. The interpretation of L with an initial state represented by closed term e:DL , denoted by L(e), is a labelled transition system M = hS, A, →, s0 i, where: • S = DL with initial state s0 = [[e]] ∈ S; • A = {a(va ) | a ∈ A ct, va ∈ Da } is the (possibly infinite) set of actions; a(va ) • →⊆ S×A×S is the set of transitions, where v −−−→ w holds if and only if for some u ∈ Ea and environment ε: – [[ fa (dL , ea )]]ε[dL 7→ v, ea 7→ u] = va and [[ga (dL , ea )]]ε[dL 7→ v, ea 7→ u] = w, – [[ca (dL , ea )]]ε[dL 7→ v, ea 7→ u] evaluates to true. Throughout this paper, whenever we refer to an LPE L we implicitly mean the LPE as given by Def. 1, with dL being the state parameter of sort DL of process L. Note that an LPE L compactly expresses that in a state, represented by parameter dL , whenever condition ca (dL , da ) holds (for some non-deterministically chosen value for variable da ), then action a carrying data parameter fa (dL , da ) can be executed, effectively changing the global state to ga (dL , da ). Notation 1. In our examples we permit ourselves to be less strict in following the LPE format and allow for multiple summands ranging over the same action label. Moreover, in case a summand binds a local 3 88 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse variable da which does not occur in the expressions ca , fa and ga , we omit the ∑-symbol altogether. In our examples, action labels can carry zero or more arguments. Whenever condition ca is the constant true, we omit both the condition and the → symbol. Example 1. As a running example, we consider a small system modelling a simple counter that can increase and decrease a parameter n, reset that parameter to 0 when it has a positive value, and show the current value. The system is described by L(0), where LPE L is given below. L(n:N) = inc · L(n + 1) + (n > 0) → dec · L(n − 1) + (n > 1) → reset · L(0) + show(n) · L(n) Parts of the (infinite) labelled transition system associated to the LPE are depicted below; the dashed edges indicate the presence of one (or more) edges. show(0) show(1) show(2) show(3) inc inc inc 0 dec 1 dec 2 dec 3 reset reset 2.2 First-Order Modal µ-Calculus Model checking is concerned with checking whether a modal property holds for a given system or not. The first-order modal µ-calculus (µ-calculus for short) of [18, 12] is a highly-expressive language for stating such properties. This logic is based on the standard modal µ-calculus [2], extended with first- order quantification and parameterised fixpoints, adding data as a first-class citizen. We briefly review its syntax and semantics, and we demonstrate its use by means of several small examples. Definition 2. The µ-calculus, ranging over a set of (typed) action labels A ct is given by the following BNF grammar; formula ϕ represents a state formula and formula α represents an action formula: ϕ ::= b | Z(e) | ¬ϕ | ϕ1 ∧ ϕ2 | [α]ϕ1 | ∀d:D. ϕ | νZ(d:D = e). ϕ α ::= a(ea ) | b | ¬α1 | α1 ∧ α2 | ∀d:D. α1 b is an expression of sort B; e is a data expression of type D; Z:D → B is a fixpoint variable from a set of fixpoint variables P; for simplicity, we assume all fixpoint variables range over the same sort D. Expressions of the form (νZ(d:D = e). ϕ) are subject to the restriction that any free occurrence of Z in ϕ must be within the scope of an even number of negation symbols ¬. Finally, a is an action label from the set A ct and expression ea of sort Da is a parameter of a. For reference we include the semantics of a µ-calculus formula in Table 1. Note that the ordered set h[D → 2S ], vi is a complete lattice, where [D → 2S ] is the set of functions from D to subsets of S and v is defined as f v g iff for all v ∈ D, we have f (v) ⊆ g(v). Since the functionals Φρε are monotonic over this lattice, the interpretation of fixpoint expressions is then justified [22]. In the remainder of this paper, we use the following standard abbreviations for µ-calculus formulae ϕ, action formulae α and (both µ-calculus formulae and action formulae) ψ. (ψ1 ∨ ψ2 ) = ¬(¬ψ1 ∧ ¬ψ2 ) hαiϕ = ¬[α]¬ϕ ∃d:D.ψ = ¬∀d:D.¬ψ µZ(d:D = e).ϕ = ¬νZ(d:D=e). ¬ϕ[Z := ¬Z] 4 89 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse Table 1: The interpretation of a µ-calculus formula ϕ and action formula α, denoted by [[ϕ]]ρε and k α kε, respectively, in the context of environments ε and ρ and an LTS M = hS, A, →, s0 i. ( S if [[b]]ε is true [[b]]ρε = 0/ otherwise [[Z(e)]]ρε = ρ(Z)([[e]]ε) [[¬ϕ]]ρε = S \ [[ϕ]]ρε [[ϕ1 ∧ ϕ2 ]]ρε = [[ϕ1 ]]ρε ∩ [[ϕ2 ]]ρε a [[[α]ϕ]]ρε = {w∈S | ∀w0 ∈S ∀a∈A (w → − w0 ∧ a∈k α kε) ⇒ w0 ∈[[ϕ]]ρε} T [[∀d:D.ϕ]]ρε = v∈D [[ϕ]]ρ(ε[d 7→ v]) [[νZ(d:D=e). ϕ]]ρε = (νΦρε )([[e]]ε), where Φρε :(D → 2S ) → (D → 2S ) is defined as: Φρε (F) = λ v ∈ D.[[ϕ]](ρ[Z 7→ F])(ε[d 7→ v]) for F:D → 2S ( A if [[b]]ε is true k b kε = 0/ otherwise k a(ea ) kε = {a([[ea ]]ε)} k ¬α kε = A \ k α kε k α1 ∧ α2 kε = k α1 kε ∩ k α2 kε T k ∀d:D.α kε = v∈D k α kε[d 7→ v] A µ-calculus formula (in the language enriched with the above abbreviations) is in Positive Normal Form (PNF) whenever negation only occurs at the lowest level and all bound variables are distinct. We only consider formulae in PNF. Note that this is no restriction as every µ-calculus formula can be converted to PNF using suitable α-renaming and logical rules such as De Morgan. Moreover, we only consider µ-calculus formulae that are closed: data variables d only occur in the scope of a quantifier or a fixpoint binding it, and each fixpoint variable Z only occurs in the scope of a fixpoint that binds it. Since the semantics of closed formulae is independent from the environments ε and ρ, we typically write [[ϕ]] rather than [[ϕ]]ρε for closed ϕ. A formula ϕ is normalised whenever none of its subformulae of the form σ X(d:D = e). ψ contain unbound data variables. Every closed formula can be converted (in linear time) to an equivalent normalised formula, see e.g. [16]. We are mainly concerned with the problem of deciding (and explaining) whether a given LPE L(e) meets a logical specification ϕ given by a µ-calculus formula; this is known as the model checking problem. That is, we wish to decide whether [[e]] ∈ [[ϕ]]; we write L(e) |= ϕ to denote just this. We finish this section with a few illustrative examples of the use of data in formulae and parameter- isation of fixpoints. Example 2. Consider the LPE modelling the counter. Below are some simple properties of the counter, expressed in the µ-calculus. 1. the counter is deadlock-free: νX.([true]X ∧ htrueitrue); 2. the counter can be incremented ad infinitum: νX.hinciX; 3. the counter can alternatingly increase and decrease ad infinitum: νX.hincihdeciX; 4. the counter can be decreased infinitely often: νX.µY.(hdeciX ∨ hinciY ); 5. the counter can take on any natural number: ∀n:N.µX.(hshow(n)itrue ∨ htrueiX). 5 90 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse Table 2: The semantics [[ϕ]]ηε of a predicate formula ϕ is a truth assignment given in the context of a data environment ε and a predicate environment η:X → (DX → B). [[b]]ηε = [[b]]ε [[X(e)]]ηε = η(X)([[e]]ε) [[ϕ1 ∨ ϕ2 ]]ηε = [[ϕ1 ]]ηε or [[ϕ2 ]]ηε [[ϕ1 ∧ ϕ2 ]]ηε = [[ϕ1 ]]ηε and [[ϕ2 ]]ηε [[∃d:D.ϕ]]ηε = [[ϕ]]η(ε[d 7→ v]) for some v ∈ D [[∀d:D.ϕ]]ηε = [[ϕ]]η(ε[d 7→ v]) for all v ∈ D 6. on all paths, the counter can decrease as often as it has increased: νX(m:N = 0).([inc]X(m + 1) ∧ [dec]X(m − 1) ∧ [¬inc ∧ ¬dec]X(m) ∧ (m = 0 ∨ hdecitrue)); Note that all of the above properties hold for the initial state of the counter except for the last one: due to the reset action that can take place at any moment, the system may return to the initial state in which it can no longer perform a dec action. 3 Model Checking using Parameterised Boolean Equation Sys- tems Solving the first-order modal µ-calculus model checking problem can be done in various ways. We here focus on the use of an intermediate formalism called parameterised Boolean equation systems [13]. These equation systems underlie several verification toolsets for specifying and analysing software and hardware systems, such as the CADP and mCRL2 toolsets. The advantage of using an intermediate formalism is that it allows for building dedicated techniques for that formalism [13, 12]. Parameterised Boolean Equation Systems are sequences of fixpoint equations where each equation is of the form νX(d:D) = ϕ or µX(d:D) = ϕ. A parameterised Boolean equation is, in a sense, a simplified and equational variant of a first-order µ-calculus formula, lacking modal operators. We refer to the left-hand side variable of a parameterised Boolean equation as a predicate variable, whereas the right-hand side formula is called a predicate formulae. Definition 3. A parameterised Boolean equation system E is a system of equations defined by: E ::= 0/ | (µX(dX :DX ) = ϕ) E | (νX(dX :DX ) = ϕ) E ϕ ::= b | X(e) | ϕ ∨ ϕ | ϕ ∧ ϕ | ∃d:D.ϕ | ∀d:D.ϕ b is an expression of sort B, X is a predicate variable taken from some sufficiently large set of typed predicate variables X , dX is a data parameter of sort DX , d is a data variable of sort D and e is a data expression of the appropriate sort. Again for simplicity, we assume that all predicate variables range over the same sort DX . We only consider well-formed, closed PBESs in this paper. A PBES E is said to be well-formed iff every predicate variable X ∈ bnd(E ), where bnd(E ) is the set of bound variables (those predicate variables occurring at the left-hand side of the equations), occurs at the left-hand side of precisely one equation of E . A PBES E is said to be closed iff (1) for each right-hand side predicate formula ϕ occurring in E we have occ(ϕ) ⊆ bnd(E ), where occ(ϕ) contains all predicate variables occurring in 6 91 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse ϕ, and, (2) whenever the only free data variable occurring in ϕ is the data parameter occurring at the left-hand side of ϕ’s equation. The interpretation of predicate formulae is listed in Table 2; for the fixpoint semantics of a PBES we refer to e.g. [13]. Instead of the fixpoint semantics we here focus on the equivalent proof graph semantics provided in [6]. This semantics is both more accessible (operational) and better suits our needs of computing counterexamples and witnesses. The proof graph semantics of a PBES explains the value, or truth assignment for each bound predicate variable by means of a directed graph with vertices ranging over the signatures of a PBES. A signature is a tuple (X, v) for X ∈ bnd(E ) and v ∈ DX a value taken from the domain underlying the type of X; that is, we set sig(E ) = {(X, v) | v ∈ DX , X ∈ bnd(E )}. We order each pair of variables X,Y ∈ bnd(E ) as follows: X ≤ Y iff the equation for Y follows that of X and we write X < Y iff X ≤ Y and X 6= Y . Moreover, we say that a variable X is a ν-variable whenever X occurs at the left-hand side of a greatest fixpoint equation; otherwise, X is a µ-variable. Definition 4. A graph G = (V, E), for V ⊆ sig(E ) and E ⊆ V ×V is a proof graph iff: 1. for all equations (σ X(dX :DX ) = ϕ) in E for which (X, v) ∈ V , [[ϕ]]Θ(X,v) ε[dX 7→ v] holds for some ε and where Θ(X,v) is the environment defined as follows: Θ(X,v) (Y ) = {w ∈ DX | h(X, v), (Y, w)i ∈ E} for all Y ; 2. for all infinite paths (X1 , v1 ) (X2 , v2 ) . . . through G , the smallest variable (w.r.t. the ordering <) occurring infinitely often on that path is a ν-variable. The semantics (often referred to as the (partial) solution) of a PBES is as follows; the correspondence with the more traditional fixpoint semantics follows from, e.g. [6]. Definition 5. Let E be a PBES. The semantics of E is a predicate environment [[E ]] defined as follows: v ∈ [[E ]](X) iff X ∈ bnd(E ) and there is a proof graph G = (V, E) such that (X, v) ∈ V . The dual of a proof graph is called a refutation graph. Such a graph explains that a value v does not belong to the set of values defined by some variable X. The notion of a refutation graph is defined analogously to a proof graph, using complementation for Θ(X,v) in condition 1 and requiring that the least variable occurring on any infinite path in the graph is a µ-variable. A proof graph containing a vertex (X, v) provides evidence that the value v belongs to the set of values defined by X in the PBES. In that case, the first condition essentially states that v belongs to X because all successors of (X, v) together yield an environment that makes the right-hand side formula for X hold when parameter dX is assigned value v. The second condition ensures that the graph respects the parity condition typically associated with (nested) fixpoint formulae. Example 3. Consider the PBES (νX(n:N) = Y (n)) (µY (n:N) = (n > 0 ∧ X(n − 1)) ∨ Y (n + 1)). A proof graph for this PBES is given below: (X, 0) (Y, 0) (Y, 1) Note that there are an infinite number of proof graphs containing (X, 0). An alternative proof graph is, e.g. the following: (X, 0) (Y, 0) (Y, 1) (Y, 2) (X, 1) From the first proof graph it follows that {0} ⊆ [[E ]](X), whereas from the second proof graph it follows that {0, 1} ⊆ [[E ]](X) and {0, 1, 2} ⊆ [[E ]](Y ). Note that it is straightforward to show, by extending the given proof graphs, that for any natural number k ∈ N, we have k ∈ [[E ]](X) and k ∈ [[E ]](Y ). 7 92 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse A proof graph is minimal if leaving out vertices or edges yields a graph that violates the proof graph conditions. We here note that the problem of computing a minimal proof graph (i.e. a subgraph of a proof graph that is as small as possible), is NP hard [6]. However, some techniques for computing a proof graph, such as solving a parity game induced by a PBES and using the winning strategies to filter unreachable vertices, yield minimal proof graphs by definition. Note that minimality of a proof graph does not imply the non-existence of a proof graph that is strictly smaller, see the example below. Example 4. Consider the two proof graphs of Example 3. The first graph is a minimal proof graph and it is also the smallest possible proof graph. The second proof graph is clearly not minimal; however, by omitting the edge from (Y, 1) to (X, 0) we obtain another minimal proof graph. The thus obtained proof graph is clearly not the smallest possible proof graph. There are numerous ways in which a PBES E can be partially solved, i.e. for which we can decide, for a given bound predicate variable X ∈ bnd(E ) and value v, whether v ∈ [[E ]](X). For instance, one can use Gauß Elimination and symbolic approximation [12], or by constructing and solving a parity game that is induced by a PBES [18]. As we remarked at the start of this section, the usefulness of PBESs lies in the observation that there is a linear-time reduction of the first-order modal µ-calculus model checking problem for LPEs to PBESs, see e.g. [12]. This transformation generalises the reduction of the (standard) modal µ-calculus for LTSs to Boolean equation systems [15]. For reference, we provide the details for this reduction in Table 3; in the next section, we present our modifications to this transformation. The correctness of the original transformation is given by the following theorem, taken from [12]. Theorem 1. Let formula σ X(d:D = e0 ). ψ be a closed, normalised first-order modal µ-calculus formula and L(e) be an LPE. Then L(e) |= σ X(d:D = e0 ). ψ iff ([[e]], [[e0 ]]) ∈ [[EL (σ X(d:D = e0 ). ψ)]](X). Example 5. We illustrate the transformation on the counter modelled by LPE L(0) of Example 1. Say that we wish to analyse whether the counter can be decreased infinitely often, i.e. property (4) of Example 2: νX.µY.(hdeciX ∨ hinciY ). The PBES resulting from the transformation (after logical simplification, eliminating all subformulae obtained from summands not matching the action labels in the modal operators) is the PBES of Example 3. Note that, per Theorem 1, the proof graphs given there illustrate that the property holds for L(0). Next, suppose we wish to verify the property that we can infinitely often alternatingly increase and decrease parameter n, i.e. property (3) of Example 2. Recall that this is formalised by the following µ- calculus formula νX.hincihdeciX. The PBES E we obtain from this property (again after some logical simplification) is as follows: νX(n:N) = n + 1 > 0 ∧ X((n + 1) − 1) It follows, by definition, that 0 ∈ [[E ]](X), see the proof graph given below. (X, 0) Consequently, by Theorem 1 we find that also L(0) |= νX.hincihdeciX. In [6], proof graphs and refutation graphs for PBESs were introduced in an effort to provide a meaningful explanation of the answer to a decision problem encoded in a PBES. While at the level of a PBES these graphs indeed meet their objective, as they provide the exact reasoning underlying the (partial) solution of a PBES, they do not aid in understanding the solution at the level of the decision problem that is encoded in the PBES. This is clearly illustrated in, e.g. the last proof graph for the PBES underlying the model checking problem of Example 5: the single vertex with a self-loop, constituting the proof graph, does not explain which transitions of the LTS of Example 5 are involved. 8 93 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse Table 3: Translation scheme for encoding the problem L |= σ X(d:DX = e0 ). ψ into an equation system. Recall that parameter dL of sort DL , occurring in the rules, originates from LPE L of Def. 1; likewise, the expressions ca , fa and ga originate from this LPE. EL (b) = ε EL (X(e)) = ε EL (ϕ ⊕ ψ) = EL (ϕ) EL (ψ) for ⊕ ∈ {∧, ∨} EL (Q d:D.ϕ) = EL (ϕ) for Q ∈ {∀, ∃} EL ([α]ϕ) = EL (ϕ) EL (hαiϕ) = EL (ϕ) EL (σ X(d:DX = e). ψ) = (σ X(dL :DL , d:DX ) = RHSL (ψ)) EL (ψ) RHSL (b) = b RHSL (X(e)) = X(dL , e) RHSL (ϕ ⊕ ψ) = RHSL (ϕ) ⊕ RHSL (ψ) for ⊕ ∈ {∧, ∨} RHSL (Q d:D.ϕ) = Q d:D. RHSL (ϕ) for Q ∈ {∀, ∃} V RHSL ([α]ϕ) = a∈A ct ∀ea :Da . (ca (dL , ea ) ∧ match(a( f a (dL , ea )), α)) =⇒ (RHSL (ϕ)[ga (dL , ea )/dL ]) W RHSL (hαiϕ) = a∈A ct ∃ea :Da . (ca (dL , ea ) ∧ match(a( f a (dL , ea )), α) ∧ (RHSL (ϕ)[ga (dL , ea )/dL ])) RHSL (σ X(d:DX = e). ϕ) = X(dL , e) match(a(v), b) = b match(a(v), a0 (e0 )) = (v = e0 ) ∧ (a = a0 ) match(a(v), ¬α) = ¬match(a(v), α) match(a(v), α ∧ β ) = match(a(v), α) ∧ match(a(v), β ) match(a(v), ∀d:D. α) = ∀d:D. match(a(v), α) 4 Evidence Extraction from PBESs Whenever a model checking problem yields an unexpected verdict, evidence in the form of a witness or counterexample supporting that verdict can be helpful in analysing the root cause. Following [7], such a witness or counterexample is a fragment of the original labelled transition system (or LPE) that can be used to reconstruct the model checking verdict. However, a proof graph underlying a PBES that encodes a model checking problem lacks some essential information about the LPE to extract a counterexample or witness, see Example 5. This issue was recognised and further studied in [7] in a slightly different setting, viz. in the setting of the logic Least Fixed Point (LFP). The solution proposed in [7] is to extend the proof graphs with information about first-order relation symbols from the structures involved in the encoded decision problem. Using proof graphs enriched in this way, evidence (e.g. counterexamples or witnesses) can be extracted from the proof graphs by projecting onto the vertices referring to the relational symbols of the desired structure(s). The thus obtained structures are weak substructures of the original structures that allow for reconstructing the proof graph underlying the original PBES. Porting the proposed solution to the setting to PBESs is, however, not straightforward. The reason for this is that, unlike in LFP formulae, one cannot refer to first-order relational symbols; one can essentially only refer to Boolean expressions and predicate variables. Consequently, proof graphs for PBESs cannot be enriched in a similar fashion. We propose to solve this problem by adding the information from the structures, relevant for con- structing proper diagnostics, to the encoding of the decision problem. For instance, if the diagnostics 9 94 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse for a model checking problem requires that a weak substructure of the original structures can be recon- structed, then we add information about that structure to our encoding. The extra information is added in the form of additional equations and by adding predicate variables that refer to those equations. For the model checking problem, this only requires changing the rules for RHSL ([α]ϕ) and RHSL (hαiϕ): V RHSL ([α]ϕ) = a :Ea . (ca (dL , ea ) ∧ match(a( f a (dL , ea )), α)) a∈A ct ∀e  RHSL (ϕ)[ga (dL , ea )/dL ] ∧ La+ (dL , fa (dL , ea ), ga (dL , ea )) =⇒  ∨ La− (dL , fa (dL , ea ), ga (dL , ea )) W  RHSL (hαiϕ) = a∈A ct ∃ea :Ea . ca (dL , ea ) ∧ match(a( f a (dL , ea )), α)   ∧ RHSL (ϕ)[ga (dL , ea )/dL ] ∨ La− (dL , fa (dL , ea ), ga (dL , ea ))  ∧ La+ (dL , fa (dL , ea ), ga (dL , ea )) All remaining rules remain as before. The two additional equations that must be added to the translation for each action label a, are as follows: (νLa+ (dL :DL , da :Da , dL0 :DL ) = true) (µLa− (dL :DL , da :Da , dL0 :DL ) = false) Note that their exact position in the resulting PBES does not matter (their solutions are independent of other equations as they are simple constants, so in a proof graph or refutation graph, vertices of the form (La+ , v, va , w) or (La− , v, va , w) never need to be part of an infinite path); for simplicity, we add these equations at the end of the PBES. We denote the updated translation by EcL . Theorem 2. Let formula σ X(d:D = e0 ). ψ be a closed, normalised first-order modal µ-calculus formula and L(e) be an LPE. Then L(e) |= σ X(d:D = e0 ). ψ iff ([[e]], [[e0 ]]) ∈ [[EcL (σ X(d:D = e0 ). ψ)]](X). Proof. The correctness of the new transformation follows immediately from the fact that we can sub- stitute ‘solved’ equations for their references, see [13]. That is, by replacing La+ by the constant true and replacing La− by the constant false we can effectively reduce the new rules for translating [α]ϕ and hαiϕ to the ones from Table 3. Intuitively, the modification in the translation of the hαiϕ and [α]ϕ construction allows for extract- ing evidence from a proof graph because whenever the proof graph records information about which predicate variables are required to make ϕ hold true, also information about the transition, encoded by the predicate variable La+ must be recorded in the proof graph. This follows from the fact that, e.g. in the new translation for hαiϕ, the expression La+ is added as a conjunct in the new translation. For similar reasons, whenever there is no α-matching transition leading to a state satisfying ϕ, the proof graph will contain all α-matching transitions, encoded by the predicate variable La− . Before we formally define how we can extract diagnostic information from a proof graph, we illus- trate the basic idea by showing how to solve the problem we encountered in Example 5. Example 6. Reconsider the second model checking problem of Example 5, i.e. the problem of deciding whether the counter system satisfies property νX.hincihdeciX. Whereas the standard transformation yields a PBES consisting of only one equation, we now obtain a PBES E with seven equations (two of 10 95 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse which are redundant):  νX(n:N) = n + 1 > 0 ∧  + − ((X((n + 1) − 1) ∧ Ldec (n + 1, (n + 1) − 1)) ∨ Ldec (n + 1, (n + 1) − 1)) + ∧Linc (n, n + 1)   − ∨ Linc (n, n + 1) + + (νLinc (n:N, n0 :N) = true) (νLdec (n:N, n0 :N) = true) (νLreset+ (n:N, n0 :N) = true) − − (µLinc (n:N, n :N) = false) (µLdec (n:N, n :N) = false) (µLreset (n:N, n0 :N) = false) 0 0 − Note that the smaller proof graph of Example 5 we could use to demonstrate that 0 ∈ [[E ]](X) now no + + longer is appropriate since it misses relevant information about the signatures for Linc and Ldec . Adding this extra information yields the following proof graph: + (X, 0) + (Ldec , 1, 0) (Linc , 0, 1) + + The signatures containing the Linc and Ldec predicate variables encode information about the transitions in the LPE that were involved in constructing the proof that the property we verify holds. Following the basic ideas outlined in [7], we extract the relevant information by filtering the relevant vertices from the proof graph and construct an LPE. In our case, we can extract the following LPE L+ : L+ (n:N) = (n = 0) → inc · L+ (1) + (n = 1) → dec · L+ (0) The LTS induced by L+ (0), providing diagnostics at the level of the system, is as follows: inc 0 dec 1 Note that the LTS is a subgraph of the LTS underlying L(0) (see the original LTS of Example 1), which, moreover, provides a compact and intuitive argument why the property holds. Moreover, the proof graph underlying the PBES encoding the same µ-calculus model checking problem on L+ (0) is isomorphic to the one we provided above. We next formalise the notions of witness and counterexample. Definition 6. Let L be an LPE and ϕ a µ-calculus formula. Let G = (V, E) be a finite, minimal proof graph proving L(e) |= ϕ. Let W (a) = {(eL , ea , e0L ) | (L+ , [[eL ]], [[ea ]], [[e0L ]]) ∈ V }. The witness extracted from G is the LPE Lw defined as follows: Lw (dL :DL ) = + { ∑ (eL , ea , e0L ) ∈ W (a) → a(ea ) · Lw (e0L ) | a ∈ A ct } (eL ,ea ,e0L ):DL ×Da ×DL In a similar vein, a counterexample LPE Lc is obtained by filtering all Lc signatures from V in the refutation graph. We note that the LTS underlying LPE Lw (and, likewise, the LTS underlying LPE Lc ) is a substruc- ture of the LTS underlying L; this follows from minimality of the proof graph from which these LPEs are extracted, plus the fact that the conditions under which the transitions are present are enforced in the translations of RHSL ([α]ϕ) and RHSL (hαiϕ). The theorem below states that the witness extracted from the PBES indeed contains enough information to reconstruct the proof graph from which it was extracted; a dual result holds for counterexamples extracted from a refutation graph. 11 96 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse Theorem 3. Let L be an LPE and ϕ a µ-calculus formula. Let G = (V, E) be a finite, minimal proof graph proving L(e) |= ϕ, and let Lw be the witness LPE extracted from G . Then any proof graph proving Lw (e) |= ϕ is isomorphic to some proof graph proving L(e) |= ϕ. Proof. This follows essentially from the observation that the LTS underlying the LPE Lw , extracted from G , is a substructure of the LTS underlying L. The bijection that maps all vertices of the form (Lw+ , v) to (L+ , v) and all other vertices to their identities in the proof graph proving Lw (e) |= ϕ then yields an isomorphic proof graph proving L(e) |= ϕ; see also Theorem 10 in [7]. 5 Applications We have implemented the modified transformation in the mCRL2 toolset in the existing tool lps2pbes. Moreover, we have developed a new tool, called pbessolve, which extracts evidence from a PBES that is obtained via the new transformation. The latter tool uses instantiation to a parity game (much like the technique outlined in [23, 18]), which is then solved using Zielonka’s recursive algorithm [24, 10] and from which we extract a witness or counterexample as per Def. 6. We illustrate the effectiveness of the techniques we outlined in this paper through three examples taken from the mCRL2 repository. The first example is a scheduling problem sometimes referred to as the bridge-crossing puzzle. Our second example concerns three communication protocols. The third example we consider is the Storage Management System [19] of the DIRAC Community Grid Solution for the LHCb experiment at CERN. 5.1 Bridge Crossing The bridge-crossing puzzle centres around a scheduling problem with limited access to resources. The problem is essentially as follows. A family of four people (person A, B, C and D), chased by a pack of wolves, needs to cross a narrow bridge at night. The bridge can only hold two persons at a time and the damages to the bridge require the persons to carry a torch to avoid falling off the bridge. Unfortunately, there is only one torch; its battery is running out and can only last another 18 minutes. Persons A and B can cross the bridge in 1, resp. 2 minutes but person C requires 5 minutes and D even requires 10 minutes to cross the bridge. The problem is whether they have a strategy to safely cross the bridge before the battery of the torch runs out. We model the puzzle as an LPE, where we model the state space by keeping track of the positions of the four persons (i.e. which side of the bridge they are), and the time that has passed since switching on the torch. We consider two types of move actions: move(p1 , l), modelling the person p1 who is carrying a torch to move to location l (which can be s for safe, or d, for dangerous) and move(p1 , p2 , l), modelling the person p1 who is carrying a torch, crossing the bridge together with p2 . Moreover, action safe(i) signals that the family managed to safely cross the bridge, taking i minutes; action fail indicates that the family did not manage to cross the bridge before the battery of the torch ran out. To verify whether the family has a strategy to safely cross the bridge, we verify the following formula: µX.(htrueiX ∨ h∃i:N.safe(i)itrue) The witness proving the formula holds is depicted below, with 0 being the initial state. It shows a schedule by which the family can safely cross the bridge. move(B, A, s) move(A, d) move(D,C, s) move(B, d) move(B, A, s) safe(17) 0 1 2 3 4 5 6 12 97 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse 5.2 Communication Protocols Communication protocols allow for exchanging information between devices through networks using strict rules and conventions. In general, the communication medium (i.e. the network) may not be perfectly reliable: it may re-order, scramble or even lose data that it transports. Part of the problem solved by a communication protocol is to disassemble and reassemble messages sent via such a network, working around the assumed characteristics of the network to achieve reliable information exchange. A variety of communication protocols exist; we here consider the classic Alternating Bit Protocol (ABP), the One Bit Sliding Window Protocol, which is a simple bidirectional sliding window protocol with piggy backing and window sizes as the receiving and sending side of size 1 [1], and the full Sliding Window Protocol [9]. The property that we check for all three protocols is the following: there are no paths on which reading of a datum d is enabled infinitely often, but occurs only finitely often. Assuming that the data domain we range over is D and read(d) models reading datum d, this can be formalised as follows (see also, e.g. [2]): ∀d:D.νX.µY.νZ.([read(d)]X ∧ ([read(d)]false ∨ [¬read(d)]Y ) ∧ [¬read(d)]Z) None of the three protocols satisfy the property for |D| > 1. The counterexamples we can extract all have a similar flavour but differ in the number of actions involved and the underlying reason for violating the property. We depict these counterexamples in Figure 1; we have omitted all other involved actions in these counterexamples. 0 1 15 2 14 read(d0 ) read(d0 ) 3 13 0 2 0 1 read(d0 ) read(d0 ) 4 16 12 read(d0 ) 5 11 1 3 2 3 read(d0 ) 6 10 7 9 8 Figure 1: Counterexamples for the if reading of a datum is infinitely often enabled then it occurs infinitely often requirement. Left: counterexample for the ABP, middle: counterexample for the One Bit protocol, right: counterexample for the Sliding Window Protocol. In all cases, state 0 indicates the initial state; non-read(0) edge-labels have been omitted from our graphs. All three counterexamples show the presence of an infinite path along which a read(d0 ) is enabled, but never taken. Note that since this is a typical branching-time property with a strong fairness con- straint, the counterexample cannot simply be represented by an infinite path represented by a lasso. 5.3 The DIRAC Storage Management System DIRAC (Distributed Infrastructure with Remote Agent Control) is a grid solution that is designed to sup- port both production activities as well as user data analysis for the Large Hadron Collider ‘beauty’ ex- periment. It consists of distributed services that cooperate with light-weight agents that deliver workload to the grid resources: services accept requests from running jobs and agents, whereas agents actively 13 98 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse work towards specific goals. The logic of each individual agent is fairly simple but the main source of complexity arises from their cooperation. Agents communicate using the services’ databases as a shared memory for synchronising the state transitions. A formal model and analysis of two critical subsystems of DIRAC is described in [19]; one of these is the Storage Management System (SMS). In [19], it was shown that this system violated several requirements. Most of these requirements were safety require- ments. A violation of such a requirement is a simple trace in the system, which is fairly easy to generate and visualise. A requirement that defied such a simple approach is the following liveness requirement: νX.([true]X∧ [state([tStaged]) ∨ state([tFailed])]νY.([¬state([tDeleted])]Y ∧ µZ.(htrueiZ ∨ hstate([tDeleted])itrue))) The requirement essentially states that each task that is in a terminating state (i.e. in state tFailed or tStaged) is eventually removed from the DIRAC system (i.e. tDeleted). The only action of concern is the state(s) action, which emits the current state s of a task. The counterexample to the property is depicted in Figure 2; the original LTS contains 142 states, which can be further reduced (without affecting the behaviours encoded by the LTS) to the depicted 26 states. 17 21 25 0 1 12 13 14 18 22 16 20 24 state([tStaged]) 15 19 23 Figure 2: Counterexamples for the requirement that each task in a terminating state is eventually re- moved for the Storage Management Systems. State 0 indicates the initial state; we omitted all edge labels except for the trigger state([tStaged]). The dashed line between state 1 and 12 indicates a single path through states 2, 3,. . . , 12; the dotted transitions are 3D artefacts. The counterexample clearly indicates a path towards a part of the system where the task, once staged (in state 13), will never be removed from the system. 6 Conclusions and Future Work We studied and implemented the extraction of useful evidence from parameterised Boolean equation systems (PBESs) encoding the model checking problem for the first-order modal µ-calculus. Our so- lution is inspired by the LFP-approach outlined (but not implemented) in [7]. Our solution, which we have also implementation and which is made available through the mCRL2 [5] toolset, shows the appeal of the technique even when used for explaining the failure for complex requirements to hold. Apart from the model checking problem, PBESs can also be used for checking behavioural equiva- lence of processes [4]. Diagnostics for such problems are typically presented in the form of a game [8]. We expect to be able to apply the ideas outlined in the current paper to such problems as well, leading to evidence in the form of substructures for both input models, which, combined, explain the differences between both models. Implementing this problem and investigating whether such a solution would provide intelligible feedback to the user is left for future work. 14 99 Evidence Extraction from Parameterised Boolean Equation Systems Wesselink, Willemse References [1] M. Bezem and J.F. Groote. A correctness proof of a one-bit sliding window protocol in µCRL. Comput. J., 37(4):289–307, 1994. [2] J. Bradfield and C. Stirling. Modal logics and mu-calculi. In Handbook of Process Algebra, pages 293–332. Elsevier, North-Holland, 2001. [3] S. Busard. Symbolic Model Checking of Multi-Modal Logics: Uniform Strategies and Rich Explanations. PhD thesis, Université catholique de Louvain (UCL), 2017. [4] T. Chen, B. Ploeger, J. van de Pol, and T.A.C. Willemse. Equivalence checking for infinite systems using parameterized Boolean equation systems. In CONCUR, volume 4703 of LNCS, pages 120–135. Springer, 2007. [5] S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, W. Wesselink, and T.A.C. Willemse. An overview of the mCRL2 toolset and its recent advances. In TACAS, volume 7795 of LNCS, pages 199–213. Springer, 2013. [6] S. Cranen, B. Luttik, and T.A.C. Willemse. Proof graphs for parameterised Boolean equation systems. In CONCUR, volume 8052 of LNCS, pages 470–484. Springer, 2013. [7] S. Cranen, B. Luttik, and T.A.C. Willemse. Evidence for fixpoint logic. In CSL, volume 41 of LIPIcs, pages 78–93. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. [8] D. de Frutos-Escrig, J.J.A. Keiren, and T.A.C. Willemse. Games for bisimulations and abstraction. Logical Methods in Computer Science, 13(4), 2017. [9] W. Fokkink, J.F. Groote, J. Pang, B. Badban, and J. van de Pol. Verifying a sliding window protocol in µCRL. In AMAST, volume 3116 of LNCS, pages 148–163. Springer, 2004. [10] M. Gazda and T.A.C. Willemse. Zielonka’s recursive algorithm: dull, weak and solitaire games and tighter bounds. In GandALF, volume 119 of EPTCS, pages 7–20, 2013. [11] J.F. Groote and M.R. Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2014. [12] J.F. Groote and T.A.C. Willemse. Model-checking processes with data. Sci. Comput. Program., 56(3):251– 273, 2005. [13] J.F. Groote and T.A.C. Willemse. Parameterised Boolean equation systems. Theor. Comput. Sci., 343(3):332– 369, 2005. [14] A. Kick. Tableaux and witnesses for the µ-calculus, 1995. Tech. Rep. 44/95, University of Karlsruhe. [15] A. Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Uni- versität München, 1997. [16] R. Mateescu. Vérification des propriétés temporelles des programmes parallèles. PhD thesis, Institut National Polytechnique de Grenoble, 1998. [17] R. Mateescu. Efficient diagnostic generation for Boolean equation systems. In TACAS, volume 1785 of LNCS, pages 251–265. Springer, 2000. [18] B. Ploeger, W. Wesselink, and T.A.C. Willemse. Verification of reactive systems via instantiation of parame- terised Boolean equation systems. Inf. Comput., 209(4):637–663, 2011. [19] D. Remenska, T.A.C. Willemse, K. Verstoep, J. Templon, and H.E. Bal. Using model checking to analyze the system behavior of the LHC production grid. Future Generation Comp. Syst., 29(8):2239–2251, 2013. [20] P. Stevens and C. Stirling. Practical model-checking using games. In TACAS, volume 1384 of LNCS, pages 85–101. Springer, 1998. [21] L. Tan and R. Cleaveland. Evidence-based model checking. In CAV, volume 2404 of LNCS, pages 455–470. Springer, 2002. [22] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math., 5(2):285–309, June 1955. [23] A. van Dam, B. Ploeger, and T.A.C. Willemse. Instantiation for parameterised Boolean equation systems. In ICTAC, volume 5160 of LNCS, pages 440–454. Springer, 2008. [24] W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135–183, 1998. 15 100