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.
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 [
Related Work. We refer to Busard’s PhD thesis [
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 specificationS = 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 specificationS = hS, Σ, Ei is given by a many-sorted Σ-algebra consisting 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 d0 are mapped to ε(d0). 2
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
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
specifications can be compiled automatically is the Linear process equation (LPE) format, see e.g. [
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 ofconditionaction-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.
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 setA 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, →, s0i, where: • S = DL with initial state s0 = [[e]] ∈ S; • A = {a(va) | a ∈ A ct, va ∈ Da} is the (possibly infinite) set ofactions; • →⊆ S×A×S is the set of transitions, where v −a−(v−a→) 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 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) 0 inc dec
1 reset inc dec reset 2 inc dec 3
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 [
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 [
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) hαiϕ ∃d:D.ψ μZ(d:D = e).ϕ ¬(¬ψ1 ∧ ¬ψ2) ¬[α]¬ϕ ¬∀d:D.¬ψ ¬νZ(d:D=e). ¬ϕ[Z := ¬Z] {w∈S | ∀w0∈S ∀a∈A (w →−a w0 ∧ a∈k α kε) ⇒ w0∈[[ϕ]]ρε}
Tv∈D[[ϕ]]ρ(ε[d 7→ v]) = (νΦρε )([[e]]ε), where Φρε :(D → 2S) → (D → 2S) is defined as:
Φρε (F) = λ v ∈ D.[[ϕ]](ρ[Z 7→ F])(ε[d 7→ v]) for F:D → 2S
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 variableZ 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. [
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 parameterisation 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 ). 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
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 [
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.
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 ϕ, 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. [
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. [
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 variableX . 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: 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 ).
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 [
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 [
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. [
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. Consequently, by Theorem 1 we find that alsoL(0) |= νX .hincihdeciX .
In [
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 [
The solution proposed in [
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 constructing proper diagnostics, to the encoding of the decision problem. For instance, if the diagnostics for a model checking problem requires that a weak substructure of the original structures can be reconstructed, 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ϕ): RHSL([α]ϕ) RHSL(hαiϕ) = =
Va∈A ct ∀ea:Ea. (ca(dL, ea) ∧ match(a( fa(dL, ea)), α)) =⇒
RHSL(ϕ)[ga(dL, ea)/dL] ∧ La+(dL, fa(dL, ea), ga(dL, ea)) ∨ La−(dL, fa(dL, ea), ga(dL, ea)) Wa∈A ct ∃ea:Ea. ca(dL, ea) ∧ match(a( fa(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 c equations at the end of the PBES. We denote the updated translation by EL.
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
substitute ‘solved’ equations for their references, see [
Intuitively, the modification in the translation of thehαiϕ and [α]ϕ construction allows for extracting 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 L−. a
Before we formally define how we can extract diagnostic information from a proof graph, we
illustrate 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
which are redundant):
νX (n:N) =
(νLi+nc(n:N, n0:N) = true) (νLd+ec(n:N, n0:N) = true) (νLr+eset(n:N, n0:N) = true)
(μLi−nc(n:N, n0:N) = false) (μLd−ec(n:N, n0:N) = false) (μLr−eset(n:N, n0:N) = false)
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 Li+nc and Ld+ec. Adding
this extra information yields the following proof graph:
(Ld+ec, 1, 0)
The signatures containing the Li+nc and Ld+ec 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 [
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):DL×Da×DL
(eL, ea, e0L) ∈ W (a) → a(ea) · Lw(e0L) | a ∈ A ct } 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 substructure 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. 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 [
We have implemented the modified transformation in the mCRL2 toolset in the existing toollps2pbes.
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 [
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 [
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) 1 2 move(B, d)
move(B, A, s) 4 5 safe(17) 6 0 12 3 5.2
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 [
∀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.
4 3 5 2 6 1 7 0 r e a d ( d 0 ) 16 ) 0 d ( d a e r 8 15 9 14 10 13 11 12 0 1 r e a d ( d 0 ) 2 3 r e a d ( d 0 ) 0 2 read(d0) read(d0) 1 3
All three counterexamples show the presence of an infinite path along which aread(d0) is enabled, but never taken. Note that since this is a typical branching-time property with a strong fairness constraint, the counterexample cannot simply be represented by an infinite path represented by a lasso. 5.3
DIRAC (Distributed Infrastructure with Remote Agent Control) is a grid solution that is designed to
support both production activities as well as user data analysis for the Large Hadron Collider ‘beauty’
experiment. 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
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 [
μ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.
0 1 12
13 state([tStaged]) 17 16 14 15 21 20 18 19 25 24 22 23
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
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
solution is inspired by the LFP-approach outlined (but not implemented) in [
Apart from the model checking problem, PBESs can also be used for checking behavioural
equivalence of processes [