Das Kapitel untersucht die automatisierte Technik der Modellüberprüfung, mit der überprüft wird, ob benutzerdefinierte Anforderungen an ein Systemmodell gelten. Sie konzentriert sich auf die Modalrechnung, bei der Anforderungen in Formeln ausgedrückt werden und Modellüberprüfer Beweise liefern, die das Verifizierungsergebnis erklären. Die Kerninnovation ist ein neuer Ansatz zur Beweisgenerierung aus parametrisierten Booleschen Gleichungssystemen (PBESs), die zur Kodierung des Problems der Modellüberprüfung verwendet werden. Dieser Ansatz beinhaltet zunächst die Lösung einer PBES ohne zusätzliche Beweisinformationen und dann die Verwendung dieser Lösung zur Vereinfachung der Lösung der PBES, die Beweisinformationen enthält. Das Kapitel zeigt die Korrektheit dieses Ansatzes und seine Implementierung im mCRL2-Toolset auf und zeigt signifikante Leistungsverbesserungen, insbesondere bei der symbolischen Modellüberprüfung. Die experimentelle Bewertung umfasst eine Vielzahl von Modellen, von akademischen Beispielen bis hin zu industriellen Anwendungen, die die praktische Relevanz und Effizienz der vorgeschlagenen Methode unterstreichen. In diesem Kapitel werden auch verwandte Arbeiten diskutiert und zukünftige Richtungen für die Integration dieses Ansatzes mit anderen Optimierungen in PBES-Lösern und statischen Analysetechniken skizziert.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Model checking is a technique to automatically establish whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its requirements is essential for the user to understand the model checking result. Willemse and Wesselink showed that parameterised Boolean equation systems (PBESs), an intermediate format for \(\mu \)-calculus model checking, can be extended with information to generate such evidence. Solving the resulting PBES is much slower than solving one without additional information, and sometimes even impossible. In this paper we develop a two-step approach to solving a PBES with additional information: we first solve its core and subsequently use the information obtained in this step to solve the PBES with additional information. We prove the correctness of our approach and we have implemented it, demonstrating that it efficiently generates evidence using both explicit and symbolic solving techniques.
1 Introduction
Model checking [1, 8] is an automated technique for establishing whether user-defined requirements hold for (a model of) a system. The behaviour of the system is typically specified using a modelling language whose semantics is represented in terms of a labelled transition system or a Kripke structure. Requirements are expressed as formulas in LTL (linear temporal logic), or branching-time logics such as CTL (computation tree logic), CTL\(^*\), or the modal \(\mu \)-calculus.
Given the description of the system and a temporal logic formula, a model checker answers the decision problem: ‘Does (the model of) my system meet its requirement?’. The yes / no answer alone does not explain why the requirement is (not) satisfied. To this end, model checkers can provide evidence (often referred to as a witness or a counterexample) explaining the answer.
Anzeige
Model checking tools such as CADP [13] and mCRL2 [4] use parameterised Boolean equation systems (PBESs) to encode the \(\mu \)-calculus model checking problem [16]. In mCRL2, PBESs are first instantiated to a parity game (or Boolean equation system) [11, 19, 30] using a process similar to state space exploration. The resulting parity game is solved using standard algorithms such as the recursive algorithm [36]. Inspired by the work of Cranen et al. [10], Wesselink and Willemse showed that the encoding of the model checking problem to PBES can be extended with additional information such that evidence explaining the solution can be extracted [35]. The evidence subsequently allows for constructing a subgraph of the original state space that gives a minimal explanation of the outcome of the verification.
A fundamental problem in model checking is the state-space explosion problem: the size of the state space underlying a system model grows exponentially in the number of (parallel) components and state variables. Symbolic model checking [5, 27] addresses this problem by using symbolic representations such as binary decision diagrams to compactly store the state space. These ideas have been extended to symbolically explore and solve the parity game underlying a PBES [3, 4, 19, 24]. Symbolic PBES solvers are routinely used to solve the \(\mu \)-calculus model checking problem for large models. For instance, the Workload Management System (WMS) model described in [31] and the Mechanical Lung Ventilator (MLV) model from [12] could only be verified using symbolic algorithms. However, in practice, the running time of solving PBESs with evidence information is so high that waiting for a solution is not an option.
Contributions. Our main contribution in this paper is a new approach for evidence generation from PBESs. Our approach first solves a PBES without additional information. As a second step, the solution of this PBES is used to simplify the solving of the PBES that does have additional information needed for evidence generation. We establish the correctness of the approach.
We have implemented our approach in the explicit PBES solver in mCRL2 [4], and added a hybrid approach, in which the first step is performed symbolically. This solution is then used to inform the explicit PBES solver in the second step.
Anzeige
We experimentally demonstrate the effectiveness of our new approaches. In particular, our experiments show that when the first step is done using the explicit solver, the performance is comparable with the original approach in [35]. When using the symbolic solver for the first step, our approach is able to efficiently generate evidence, also in the cases where this was not feasible before.
Related work. For a comprehensive overview of diagnostics for model checking, we refer to Busard’s thesis [6]. We limit ourselves to the closest approaches providing evidence or diagnostics for the modal \(\mu \)-calculus model checking problem. Such diagnostics have for instance been described using tableaux [21] and as two-player games [32]. There are several graph-based approaches describing evidence in the literature. Mateescu [26] describes evidence for the alternation free \(\mu \)-calculus as a subgraph of an extended Boolean graph. Cranen et al. [9] describe proof graphs, that are an extension of support sets [34].
Symbolic solving of PBESs and parity games was studied in the context of LTSmin [19] and mCRL2 [24]. Symbolic model checking with evidence generation has been implemented for (Probabilistic) CTL in NuSMV [7] and PRISM [23].
Outline. Sect. 2 introduces the necessary background about the \(\mu \)-calculus, PBESs, evidence generation, and a running example. In Sect. 3 we introduce a new approach to generate evidence from PBESs and prove its correctness. We evaluate the approach in Sect. 4 and conclude in Sect. 5.
2 Preliminaries
Our work is embedded in the context in which abstract data types are used to describe and reason about data, and we distinguish their syntax and semantics. We write data sorts with letters \(D,E, \ldots \) and the semantics counterpart with \(\mathbb {D}, \mathbb {E}, \ldots .\) We require the presence of Booleans and natural numbers along with their usual operators. We use B to denote Booleans and N to denote natural numbers \(\{0,1,2,3, \dots \}\), with semantic counterparts \(\mathbb {B}= \{ true , false \}\) and \(\mathbb {N}\) respectively. For both sorts we use their semantics operation such as \(\wedge \) and \(+\) also for the syntactic counterparts. We use \(\approx \) to syntactically represent equality. Furthermore, we have a set \(\mathcal {D}\) of data variables \(d, d_1, \ldots .\) If a term is open we use the data environment\(\delta \) that maps each variable in \(\mathcal {D}\) to a value of the proper semantic domain. Given a term t, the interpretation function, under the context of a data environment \(\delta \), is denoted as \(\llbracket t \rrbracket \delta \) which is evaluated in the standard way. We write \(\delta [v/d]\) to denote that value v has been assigned to variable d, i.e., \(\delta [v/d](d') = v\) if \(d' = d\), and \(\delta [v/d](d') = \delta (d')\) otherwise. We assume that every value \(v \in \mathbb {D}\) can be represented by a closed term. With a slight abuse of notation, we also use v syntactically for this closed term.
2.1 Processes
In this paper, the behaviour of systems is modelled using linear process equations (LPEs) [15]. An LPE consists of a single process definition, parameterised with data, and condition-action-effect rules that may refer to local variables.
Definition 1
A linear process equation is an equation of the following form:
where \(+\) denotes a non-deterministic choice among the rules, \(d :D\) is the state, \(\alpha \in \mathcal {A}\) is an action label to which we associate local variable \(e_\alpha \) of sort \(E_\alpha \); \(c_\alpha (d,e_\alpha )\) is a condition, and term \(g_\alpha (d, e_\alpha )\) describes the next state.
An LPE represents the (non-deterministic) choice to perform action \(\alpha \in \mathcal {A}\) from a state represented by d, if condition \(c_\alpha (d,e_\alpha )\) evaluates to \( true \) for some value \(e_\alpha \), which when executed updates the state to \(g_\alpha (d,e_\alpha )\).
We typically write L instead of \(L(d :D)\) when referring to an LPE and omit the sum when there is no local variable. The semantics of an LPE, with a closed term e as initial state, is a labelled transition system (LTS) denoted by L(e).
Example 1
As a running example we consider a system whose behaviour is modelled by LPE L (left), where \(a,b,c \in \mathcal {A}\), and its associated LTS (right), assuming the constant \(M \approx 3\):
\(\square \)
2.2 Modal \(\mu \)-calculus
In this paper we consider requirements expressed as formulas in the modal \(\mu \)-calculus [22].
Definition 2
A \(\mu \)-calculus formula \(\varphi \) is defined by the following grammar:
where b is a Boolean constant, \(X, Y \in \mathcal {F}\) are fixpoint variables of some countable set \(\mathcal {F}\), \(\sigma \in \{\mu , \nu \}\) is a fixpoint, and \(\alpha \in \mathcal {A}\) is an action.
We only consider formulas that are closed. That is, formulas in which no fixpoint variable Y occurs outside the scope of its binder. For instance, \(\mu X. [ a ]X\) is allowed, but \(\mu X. [ a ]Y\) is not allowed. For the denotational semantics of the \(\mu \)-calculus we refer to the literature; see for instance [22].
Example 2
Consider the following \(\mu \)-calculus formula:
$$ \mu V . (\langle a \rangle V \vee \langle b \rangle V \vee \nu W . \langle c \rangle W). $$
This formula expresses that there is a finite path of a and b actions that ultimately ends with an infinite sequence of c-transitions. Intuitively, this formula holds for our running example: by executing action a to state 3 and subsequently executing the self-loop in state 3, such a path is produced. \(\square \)
2.3 Parameterised Boolean Equation Systems
Parameterised Boolean equation systems (PBESs) are systems of fixpoint equations parameterised with data, where the right-hand side is a predicate formula.
Definition 3
Parameterised Boolean equation systems (PBESs)\(\mathcal {E}\) and predicate formulas \(\varphi \) are syntactically defined as follows:
where \(\epsilon \) is the empty PBES, \(\sigma \in \{\mu , \nu \}\) is a fixpoint sign, \(X \in \mathcal {X}\) are predicate variables, d are data variables, and b and e are terms over data variables, where b is of sort B.
For equation \(\sigma X(d :D_\mathcal {X}) = \varphi \), we write \(d_X\) and \(\varphi _X\) to denote parameter d and predicate formula \(\varphi \), respectively. The set \(\textrm{bnd}(\mathcal {E})\) is the set of bound predicate variables occurring at the left-hand side of the equations in \(\mathcal {E}\). We denote the set of predicate variables occurring in formula \(\varphi \) with \(\textrm{occ}(\varphi )\), and the predicate variables occurring in the right-hand sides of \(\mathcal {E}\) with \(\textrm{occ}(\mathcal {E})\). A PBES \(\mathcal {E}\) is well-formed if it has exactly one defining equation for each \(X \in \textrm{bnd}(\mathcal {E})\). It is closed if for every X, \(\textrm{occ}(\varphi _X) \subseteq \textrm{bnd}(\mathcal {E})\), and the only free data variable in \(\varphi _X\) is \(d_X\).
Example 3
Following the encoding of [16], the following PBES encodes whether L(1) of Example 1 satisfies the \(\mu \)-calculus formula of Example 2:
\(\square \)
Predicate formulas are interpreted in the context of a predicate environment \(\eta \) and data environment \(\delta \); see Table 1 for details.
Table 1:
The interpretation function \(\llbracket \varphi \rrbracket \eta \delta \) of predicate formula \(\varphi \) is its truth assignment in the context of \(\delta \) and \(\eta :\mathcal {X}\rightarrow 2^\mathbb {D}\), data and predicate environments.
Dummy
A fixpoint semantics of PBESs is presented in [17]. Instead of the fixpoint semantics we here use the equivalent proof graph semantics provided in [9]. Given PBES \(\mathcal {E}\), \(\textrm{sig}(\mathcal {E}) = \{X(v) \mid X \in \textrm{bnd}(\mathcal {E}), v\in \mathbb {D}\}\) denotes the signature of \(\mathcal {E}\), where \(v \in \mathbb {D}\) is a value taken from the domain underlying the type of X. Every predicate variable \(X \in \textrm{bnd}(\mathcal {E})\) is assigned a number called rank; \(\textrm{rank}_{\mathcal {E}}(X)\) is even if and only if X is labelled with a greatest fixpoint, and \(\textrm{rank}_{\mathcal {E}}(X) \le \textrm{rank}_{\mathcal {E}}(Y)\) if X occurs before Y in \(\mathcal {E}\).
Definition 4
([9]). Let \(\mathcal {E}\) be a PBES and \(\textrm{G}= (V,E)\) be a directed graph, where \(V \subseteq \textrm{sig}(\mathcal {E})\) and \(E \subseteq V \times V\). The graph \(\textrm{G}\) is a proof graph iff:
for every \(X(v) \in V\) and \(\delta \), \(\llbracket \varphi _X \rrbracket \eta _{X(v)} \delta [v/d_X]= true \) with \(\eta _{X(v)}(Y)(w) = true \) iff \(\langle X(v), Y(w) \rangle \in E\) for all Y;
for all infinite paths \(X_1(v_1) X_2(v_2) \ldots \) through \(\textrm{G}\), \(\textrm{min}\{\textrm{rank}_{\mathcal {E}}(X) \mid X \in V^{\infty }\}\) is even, where \(V^{\infty }\) is the set of predicate variables that occur infinitely often in the sequence.
The first condition states that if all successors of \(X(v) \in V\) in \(\textrm{G}=(V,E)\) together yield an environment that makes \(\varphi _X\)\( true \) when parameter \(d_X\) is assigned value v, then \(X(v) = true \). The second condition ensures that the graph respects the parity condition typically associated with nested fixpoint formulas. The semantics of PBES \(\mathcal {E}\) is now defined as follows [9].
Definition 5
The semantics of PBES \(\mathcal {E}\) is a predicate environment \(\llbracket \mathcal {E} \rrbracket \) such that \(\llbracket \mathcal {E} \rrbracket (X)(v){=} true \) iff \(X {\in } \textrm{bnd}(\mathcal {E})\) and \(X(v) {\in } V\) for some proof graph \(\textrm{G}{=} (V,E)\).
We use \(\textrm{PG}(\mathcal {E})\) to refer to a proof graph for PBES \(\mathcal {E}\). An explanation of \(X(v) = false \) is given by means of a refutation graph, denoted as \(\textrm{NG}(\mathcal {E})\) for PBES \(\mathcal {E}\), the dual of a proof graph, see [9]. Because of their duality we here outline our theory using proof graphs only.
PBESs are commonly solved using a process akin to state space exploration to obtain a parity game (or Boolean equation system) [11, 19, 30], and solving the resulting game. In practice, this process uses syntactic simplifications to reduce the number of vertices that are being generated in the parity game. A lower bound of the number of vertices that need to be explored instead relies on semantic dependencies. These are captured by relevancy graphs [25]. A relevancy graph contains a dependency \(X(v) \rightarrow Y(w)\) if changing the truth value of Y(w) can change the truth value of \(\varphi _X[d_X := v]\). In the definition we write \(\eta [ b / X(e) ]\) for the predicate environment satisfying \(\eta [ b / X(e) ](Y)(f) = b\) if \(X = Y\) and \(e = f\), and \(\eta [ b / X(e) ](Y)(f) = \eta (Y)(f)\) otherwise.
Definition 6
([25]). Let \(\mathcal {E}\) be a \(\textrm{PBES}\) and \( RG = (V, \rightarrow )\) be a directed graph, where
\(V \subseteq \textrm{sig}(\mathcal {E})\) is a set of vertices,
\(\rightarrow \subseteq V \times V\) an edge relation such that for any \(X(v) \in V\),
We say that \( RG = (V, \rightarrow )\) is a relevancy graph for X(v) iff \(X(v) \in V\).
In the remainder of the paper, we use the size of the relevancy graph as a proxy for estimating the effort required to solve a PBES.
Example 4
A proof graph for the PBES in Example 3 with initial vertex X(1) is shown in Fig. 1a. It shows that vertices X(1), X(3) and Y(3) are \( true \), with the numbers above these vertices indicating their ranks, and the edges showing the required dependencies explaining this solution. The corresponding relevancy graph is shown in Fig. 1b. \(\square \)
Fig. 1:
Proof graph and relevancy graph for the PBES in Example 3.
2.4 Model Checking and Evidence Generation
A \(\mu \)-calculus model checking problem \(L(e) \models \varphi \) can be encoded into a PBES using the translation proposed by Wesselink and Willemse [35]. Proof graphs and refutation graphs extracted from a PBES obtained by this encoding allow for generating evidence, in contrast to the encoding of [16]. The evidence generated from a proof graph is a witness that explains why the behaviour meets a requirement. Dually, the evidence generated from a refutation graph is a counterexample explaining why the requirement is violated. These two cases are fully symmetric for the \(\mu \)-calculus. The translation scheme of the encoding \(\textbf{E}^c_L\) from [35] is in Table 2. The predicate variables \(Z_{\alpha }^+\) and \(Z_{\alpha }^-\) in the right-hand sides \(\textbf{RHS}^c_L([\alpha ] \varphi )\) and \(\textbf{RHS}^c_L(\langle \alpha \rangle \varphi )\) contain information about the action labels, the transitions. In particular, in a proof graph, a dependency on \(Z_{\alpha }^+\) indicates the \(\alpha \)-transition is required for a \( true \) solution, whereas in a refutation graph, a dependency on \(Z_{\alpha }^-\) indicates the \(\alpha \)-transition is involved in the \( false \) solution.
Table 2.
Translation to encode, given LPE L and \(\sigma Z .\, \varphi \), the model checking problem \(L(e) \models \sigma Z .\, \varphi \) into a PBES [35].
Dummy
In addition to the encoding of Table 2, for each action label \(\alpha \) equations \(\nu Z_{\alpha }^+(d:D, d' :D)= true \) and \(\mu Z_{\alpha }^-(d:D,d ' :D) = false \) are added to the equation system. These equations are solved and typically grouped at the end of the equation system. We write \(\mathcal {Z}^+\subseteq \mathcal {X}\) (resp. \(\mathcal {Z}^-\subseteq \mathcal {X}\)) for the set of predicate variables \(\{ Z_{\alpha }^+\mid \alpha \in \mathcal {A}\}\) (resp. \(\{ Z_{\alpha }^-\mid \alpha \in \mathcal {A}\}\)).
Theorem 1
([35]). Let L(e) be an LPE, and \(\sigma Z.\, \varphi \) be a closed \(\mu \)-calculus formula. Then, \(L(e) \models \sigma Z.\, \varphi \) if and only if \(\llbracket \textbf{E}^c_L(\sigma Z.\, \varphi ) \rrbracket (Z)(\llbracket e \rrbracket ) = true \).
We usually write \(\mathcal {E}\) for the PBES obtained from encoding \(\textbf{E}^c_L\). Specifically, \(\mathcal {E}= {\mathcal {E}_L}\mathcal {E}_{\mathcal {Z}^+} \mathcal {E}_{\mathcal {Z}^-}\), where \(\mathcal {E}_L\) contains the equations introduced by \(\textbf{E}^c_L\) and \(\mathcal {E}_{\mathcal {Z}^+}\) (resp. \(\mathcal {E}_{\mathcal {Z}^-}\)) contains all equations of the shape \(\nu Z_{\alpha }^+(d:D,d' :D) = true \) (resp. \(\mu Z_{\alpha }^-(d:D,d' :D) = false \)).
For the \(\mu \)-calculus model checking problem \(L(e) \models \varphi \), a proof graph allows for constructing an LTS \(L_w(e)\) which is a subgraph of L(e) that provides a minimal explanation of the validity of the model checking problem. This witness contains enough information to reconstruct the proof graph from which it was extracted; this dually holds for counterexamples and refutation graphs.
We show how we can extract a witness for our running example.
Example 5
Recall the LPE and \(\mu \)-calculus formula from Examples 1 and 2. PBES \(\mathcal {E}\) consists of the following equations.
The following proof graph for the PBES is found:
Predicate variables \(Z_{a}^+\) and \(Z_{c}^+\) encode information about which a-transitions and c-transitions in the LPE are involved in proving that the solution to the model checking problem is \( true \). We filter the relevant vertices with information about evidence from the proof graph, here \(Z_{a}^+(1,3)\) and \(Z_{c}^+(3,3)\), and derive the following LPE (left) and witness LTS (right):
We remark that, by construction, this LTS is a subgraph of the LTS in Example 1, underlying the original specification. For the formal definition of witness and counterexample we refer to [35], for the concept of evidence to [10]. \(\square \)
3 Improving Evidence Generation from PBESs
The encoding \(\textbf{E}^c_L\) results in a PBES from which evidence supporting the verdict of the model checking problem can be extracted. However, the additional information added to the right-hand sides of the equations significantly increases the effort needed to solve the PBES. We illustrate this using an example.
Example 6
The relevancy graph for PBES \(\mathcal {E}\) from Example 5 is the following.
Note that it contains dependencies on \(Z_{a}^+(1, n)\) and \(Z_{a}^-(1, n)\) for all \(n = 2, 3\). By increasing the value of M, used in the LPE, to values larger than 3, the number of vertices can be increased to an arbitrary number. For instance, if \(M \approx 1000\) then X(1) will have 1998 dependencies related to action a. The number of dependencies related to action b will increase similarly. \(\square \)
Omitting the information from the PBES that is needed to generate evidence would result in the PBES from Example 3, whose much smaller relevancy graph was shown in Fig. 1b. The relevancy graphs of both PBESs illustrate a trade-off. On the one hand, solving the PBES in which information to generate evidence is omitted, denoted \( core (\mathcal {E})\) (see Sect. 3.1), is (much) more efficient than solving \(\mathcal {E}\). On the other hand, diagnostic information including the transitions is essential for understanding why a formula is (not) satisfied.
In the remainder of this section, we introduce a three-step approach that allows us to efficiently solve PBESs with additional information for evidence generation. An overview of the approach is presented in Fig. 2.
Fig. 2:
Efficient evidence generation approach.
The case in which the solution to the PBES is \( true \), and the one in which the solution is \( false \) are completely symmetric. In Fig. 2, we show the case where the solution is \( false \) in lighter colour. In view of the symmetry, here we focus on presenting the approach for the \( true \) case only. The three steps are as follows.
1.
Remove the additional information from the PBES \(\mathcal {E}\), and solve the resulting PBES \( core (\mathcal {E})\) (see Sect. 3.1).
2.
Use the solution of \( core (\mathcal {E})\) to remove superfluous evidence information from the PBES, obtaining \( true (\mathcal {E})\) (see Sect. 3.2).
3.
Combine the proof graph for \( core (\mathcal {E})\) with \( true (\mathcal {E})\) to obtain a new PBES \( combine ( true (\mathcal {E}), \textrm{PG}( core (\mathcal {E})))\), and solve this PBES (see Sect. 3.3).
The third step results in a solution and proof graph for the original PBES \(\mathcal {E}\). In the remainder of this section, we address each of these steps in more detail.
We first introduce some auxiliary notation. We write \(\lambda d_X :D_X . \varphi \) lifting predicate formula \(\varphi \) to a predicate function with the same parameters as predicate variable \(X(d_X :D_X)\) [29]. The semantics is defined as \(\llbracket \lambda d_X :D_X . \varphi \rrbracket \eta \delta =\)\( \lambda v \in \mathbb {D}_X . \llbracket \varphi \rrbracket \eta \delta [v / d_X].\) We use this lifting to substitute a predicate formula for a predicate variable. Given predicate formulas \(\varphi , \psi \) and predicate variable X, we write \(\varphi [X := \lambda d_X :D_X . \psi ]\) to denote that every occurrence of X is replaced with \(\lambda d_X :D_X . \psi \) in \(\varphi \). We write \(\varphi [X := \psi _X, Y := \psi _Y]\) for the simultaneous substitution of X and Y (\(X \ne Y\)), and generalise this to \(\varphi [X := \psi _X]_{X \in \mathcal {X}}\) to denote the simultaneous substitution of all \(X \in \mathcal {X}\).
3.1 Solving a PBES Without Evidence Information
If we forego evidence, and focus on obtaining a solution for the model checking problem in terms of a true/false answer only, the amount of work can be reduced significantly. This motivates the first step in our approach.
The equations for the predicate variables in \(\mathcal {Z}^+\) and \(\mathcal {Z}^-\) in a PBES \(\mathcal {E}= {\mathcal {E}_L}\mathcal {E}_{\mathcal {Z}^+} \mathcal {E}_{\mathcal {Z}^-}\) with information on evidence are solved. Therefore, \(\mathcal {E}\) can be simplified by substituting in \(\mathcal {E}_L\) all predicate variables in \(\mathcal {Z}^+\) with \( true \) and all predicate variables in \(\mathcal {Z}^-\) with \( false \), without affecting the solution of \(\mathcal {E}\). We refer to this as core PBES, defined as follows.
Definition 7
Let \(\mathcal {E}= {\mathcal {E}_L}\mathcal {E}_{\mathcal {Z}^+} \mathcal {E}_{\mathcal {Z}^-}\). Then
Let PBES \(\mathcal {E}\) be as in Example 5. Then \( core (\mathcal {E})\) is obtained from this PBES by replacing the equations for X and Y by the corresponding equations from Example 3. Note the relevancy graph of the latter (see Fig. 1b) is much smaller than the one for \(\mathcal {E}\) (see Example 6). \(\square \)
It follows immediately from standard results on PBESs [17] that the solution of the equations in \(\mathcal {E}_L\) are preserved by transformation \( core (\mathcal {E})\).
Once we have established that the solution to \( core (\mathcal {E})\), and hence \(\mathcal {E}= {\mathcal {E}_L}\mathcal {E}_{\mathcal {Z}^+} \mathcal {E}_{\mathcal {Z}^-}\), is \( true \), only the information for constructing a witness is relevant. We therefore remove the dependencies on predicate variables needed to construct counterexamples by substituting in \(\mathcal {E}_L\) all predicate variables in \(\mathcal {Z}^-\) with \( false \). We refer to the resulting PBES as \( true (\mathcal {E})\).
Definition 8
Let \(\mathcal {E}= {\mathcal {E}_L}\mathcal {E}_{\mathcal {Z}^+} \mathcal {E}_{\mathcal {Z}^-}\). Then
Recall that the solution of \( core (\mathcal {E})\) of Example 7 is \( true \). We use this to obtain the following PBES \( true (\mathcal {E})\):
We obtain the corresponding relevancy graph by removing all vertices for \(Z_{a}^-, Z_{b}^-\) and \(Z_{c}^-\) and their incoming edges from the relevancy graph in Example 6. \(\square \)
3.3 Simplifying a PBES using Evidence Information
We now show how a proof graph can be used to further simplify the right-hand sides in a PBES. For this, recall that for a vertex X(v) in the proof graph, the successors of X(v) yield a predicate environment that makes \(\varphi _X[d_X := v]\) true. Using this information, we can syntactically remove all dependencies that are not in the proof graph from the right-hand sides in a PBES, without affecting the solution. To achieve this, we define \( combine (\mathcal {E}, \textrm{G})\) as follows.
Definition 9
Let \(\mathcal {E}\) be a PBES, and \(\textrm{G}= (V, E)\) be a proof graph. Then PBES \( combine (\mathcal {E}, \textrm{G})\) is obtained by replacing the right-hand side of every equation \(\sigma X(d_X: D_X) = \varphi _X\) in \(\mathcal {E}\) by the formula
$$ \varphi _X[Y := \lambda e . \bigwedge _{v \in V_X} (d_X \approx v \implies e \in E_{X(v),Y} \wedge Y(e))]_{Y \in \mathcal {X}\setminus (\mathcal {Z}^+\cup \mathcal {Z}^-)} $$
where \(V_X = \{ v \in \mathbb {D} \mid X(v) \in V \}\) contains all values v such that X(v) is a vertex in \(\textrm{G}\), and \(E_{X(v),Y} = \{ w \in \mathbb {D} \mid \langle X(v), Y(w) \rangle \in E \}\) contains all direct dependencies of X(v) on Y in the proof graph.
Intuitively, this retains only those dependencies in \(\varphi _X\) that according to the proof graph are needed to show that X(v) is true, for any v.
Example 9
Recall the equation for X in PBES \( true (\mathcal {E})\) from Example 8.
The proof graph for \( core (\mathcal {E})\) (see Fig. 1a) has vertices \(V = \{ X(1), X(3), Y(3) \}\) and edges \(E = \{ (X(1), X(3)), (X(3), Y(3)), (Y(3), Y(3)) \}\). So, we infer \(V_X = \{ 1, 3 \}\), \(V_Y = \{ 3 \}\), \(E_{X(1),X} = \{ 3 \}\), \(E_{X(1), Y} = E_{X(3), X} = \emptyset \), \(E_{X(3), Y} = \{ 3 \}\), \(E_{Y(3), X} = \emptyset \), and \(E_{Y(3), Y} = \{ 3 \}\).
The right-hand side of the equation for X in \( combine ( true (\mathcal {E}), \textrm{PG}( core (\mathcal {E})))\), after \(\beta \)-reduction and simplification, is as follows.
This simplifies further to
If we also apply the corresponding substitution to the equation for Y and apply some simplification, we obtain the following PBES.
This PBES has the following relevancy graph, that no longer has dependencies on \(Z_{b}^+\) and only a single dependency on \(Z_{a}^+\), and is significantly smaller than the relevancy graph of Example 6:
\(\square \)
In the example we have combined the PBES \( true (\mathcal {E})\) with a proof graph for the strongly related PBES \( core (\mathcal {E})\). Towards establishing the correctness of this transformation, we first prove the following technical lemma, that shows that the substitution of a single predicate variable in a proof graph like context does not change the solution. Proofs that are either sketched or omitted from this section are included in the extended version of this paper [33].
Lemma 3
Let \(V \subseteq \mathbb {D}\) be a set of values, Y a predicate variable, and \(\{ E_{v,Y} \subseteq \mathbb {D} \}_{v \in V}\) be a V-indexed family of sets of values. For every \(v \in V\), predicate environment \(\eta \) such that \(\eta (Y)(w) = true \) iff \(w \in E_{v,Y}\), predicate formula \(\varphi \), data variable d free in \(\varphi \), and data environment \(\delta \), we have
$$ \llbracket \varphi \rrbracket \eta \delta [v/d] \implies \llbracket \varphi [Y := \lambda e . \bigwedge _{w \in V}( d \approx w \implies e \in E_{v, Y} \wedge Y(e)] \rrbracket \eta \delta [v/d] $$
Proof
Fix, V, Y, \(\{ E_{v,Y} \subseteq \mathbb {D} \}_{v \in V}\), v and \(\eta \) as in the statement of the lemma. We proceed by induction on the structure of \(\varphi \). Most cases are immediate, or follow from the induction hypothesis and the semantics of predicate formulas. We focus on the interesting case where \(\varphi = Z(e')\) for some Z and \(e'\). If \(Z \ne Y\), the result is immediate, since the substitution has no effect. So, suppose \(Z = Y\). We have to show that \(\llbracket Y(e') \rrbracket \eta \delta [v/d]\) implies \(\llbracket Y(e')[Y := \lambda e . \bigwedge _{w \in V} (d \approx w \implies e \in E_{v,Y} \wedge Y(e))] \rrbracket \eta \delta [v / d]\).
Assume \(\llbracket Y(e') \rrbracket \eta \delta [v/d]\) is \( true \). Hence, \(\eta (Y)(\llbracket e' \rrbracket \delta [v/d])\) is \( true \), so by assumption, \(\llbracket e' \rrbracket \delta [v/d] \in E_{v,Y}\), and therefore \(\llbracket e'\in E_{v,Y} \rrbracket \delta [v/d]\) is \( true \). Similarly, it immediately follows that \(\llbracket d \approx w \rrbracket \delta [v/d]\) is \( true \) iff \(w = v\). So, it follows that \(\llbracket \bigwedge _{w \in V} (d \approx w \implies e' \in E_{v,Y} \wedge Y(e')) \rrbracket \eta \delta [v / d]\) is \( true \). Using the definition of substitution and \(\beta \)-reduction, it then follows that \(\llbracket Y(e')[Y := \lambda e . \bigwedge _{w \in V} (d \approx w \implies e \in E_{v,Y} \wedge Y(e))] \rrbracket \eta \delta [v / d]\) is also \( true \). \(\square \)
We use this lemma to establish that the proof graph for \( core (\mathcal {E})\) can easily be extended into a proof graph for \( combine ( true (\mathcal {E}), G)\). This shows that for values of interest to the original model checking problem, the result remains unchanged.
Proposition 1
For every proof graph G for \( core (\mathcal {E})\), there is a proof graph \(G'\) for \( combine ( true (\mathcal {E}), G)\) such that G is a subgraph of \(G'\).
Proof sketch
Let \(G = (V, E)\) be a proof graph for \( core (\mathcal {E})\). Define \(G' = (V \cup V_{\mathcal {Z}^+}, E \cup (V \times V_{\mathcal {Z}^+}))\) with \(V_{\mathcal {Z}^+} = \{ Z_{a}^+(e_L, e_a, e'_L) \mid Z_{a}^+\in \mathcal {Z}^+, e_L, e'_L \in \mathbb {D}_L, e_a \in \mathbb {D}_a \}\). Then G is a subgraph of \(G'\).
We show \(G'\) is a proof graph for \( combine ( true (\mathcal {E}), G)\). For \(Z_{a}^+(e_L, e_a, e'_L) \in V_{\mathcal {Z}^+}\), the condition on \(\varphi _{Z_{a}^+}\) follows immediately. So, let \(X(v) \in V\), and \(\varphi _X\) and \(\psi _X = \varphi _X[Y := \lambda e . \bigwedge _{v \in V_X} (d_X \approx v \implies e \in E_{X(v),Y} \wedge Y(e))]_{Y \in \mathcal {X}\setminus (\mathcal {Z}^+\cup \mathcal {Z}^-)}\) be the right-hand sides of X in \( core (\mathcal {E})\) and \( combine ( true (\mathcal {E}), G)\), respectively. As G is a proof graph for \( core (\mathcal {E})\), \(\llbracket \varphi _X \rrbracket \eta _{X(v)} \delta [v/d_X]\) is \( true \), where \(\eta _{X(v)}\) is such that \(\eta _{X(v)}(Y)(w) = true \) iff \(\langle X(v), Y(w) \rangle \in E\). It follows from Lemma 3 that \(\llbracket \psi _X \rrbracket \eta _{X(v)} \delta [v/d_X]\) is \( true \), so \(G'\) is a proof graph for \( combine ( true (\mathcal {E}), G)\). \(\square \)
3.4 Providing Evidence for the Original PBES
The result that every proof graph G for \( core (\mathcal {E})\) can be extended into a proof graph \(G'\) for \( combine ( true (\mathcal {E}), G)\) is sufficient to show that \( combine ( true (\mathcal {E}), G)\) does not change the solution of the PBES. However, \(G'\) may contain too many variables with evidence information, resulting in witnesses that are larger than needed. In practice, we therefore solve \( combine ( true (\mathcal {E}), G)\) again, leading to a proof graph that only contains the necessary dependencies on variables in \(\mathcal {Z}^+\).
Correctness of our approach ultimately follows if a solution and proof graph obtained for PBES \( combine ( true (\mathcal {E}), G)\) are also a correct solution and proof graph for our original PBES \(\mathcal {E}\). We first establish the following result.
Lemma 4
Let \(V \subseteq \mathbb {D}\) be a set of values, Y a predicate variable, and \(\{ E_{v,Y} \subseteq \mathbb {D} \}_{v \in V}\) be a V-indexed family of sets of values. For every \(v \in V\), predicate environment \(\eta \), formula \(\varphi \), data variable d free in \(\varphi \), and data environment \(\delta \),
$$ \llbracket \varphi [Y := \lambda e . \bigwedge _{w \in V}( d \approx w \implies e \in E_{v, Y} \wedge Y(e)] \rrbracket \eta \delta [v/d] \implies \llbracket \varphi \rrbracket \eta \delta [v/d] $$
The proof is similar to that of Lemma 3. Note that where Lemma 3 considers every predicate environment \(\eta \) such that \(\eta (Y)(w) = true \) iff \(w \in E_{v,Y}\), in Lemma 4 there is no assumption on \(\eta \). We now use Lemma 4 to establish that the proof graph computed for PBES \( combine ( true (\mathcal {E}), G)\) is also a proof graph for \(\mathcal {E}\).
Theorem 2
Let G be a proof graph for \( core (\mathcal {E})\). Then every proof graph \(G'\) for \( combine ( true (\mathcal {E}), G)\) is also a proof graph for \(\mathcal {E}\).
Proof sketch
Let \(G = (V, E)\) be a proof graph for \( core (\mathcal {E})\) and \(G' = (V', E')\) be a proof graph for \( combine ( true (\mathcal {E}), G)\).
For every X bound in \( core (\mathcal {E})\), let \(\varphi _X\) be the right-hand side of X in \(\mathcal {E}\). Let \(\varphi ^t_X = \varphi _X[Z_{a}^-:= \lambda d :D_{Z_{a}^-} . false ]_{Z_{a}^-\in \mathcal {Z}^-}\) be the right-hand side of X in \( true (\mathcal {E})\). Also, let \( \psi _X = \varphi ^t_X[Y := \lambda e . \bigwedge _{v \in V_X} (d_X \approx v \implies e \in E_{X(v),Y} \wedge Y(e))]_{Y \in \mathcal {X}\setminus (\mathcal {Z}^+\cup \mathcal {Z}^-)} \) be the right-hand side of X in \( combine ( true (\mathcal {E}), G)\).
Fix \(X(v) \in V'\), then \( \llbracket \psi _X \rrbracket \eta _{X(v)} \delta [v/d_X] \) is \( true \) since \(G'\) is a proof graph for \( combine ( true (\mathcal {E}), G)\). It follows from Lemma 4 that \( \llbracket \varphi ^t_X \rrbracket \eta _{X(v)}\delta [v/d_X] \) is \( true \), so \(G'\) is a proof graph for \( true (\mathcal {E})\). As all variables in \(\mathcal {Z}^-\) are \( false \), any proof graph for \( true (\mathcal {E})\) is a proof graph for \(\mathcal {E}\), so \(G'\) is a proof graph for \(\mathcal {E}\). \(\square \)
Hence, the proof graph computed using our approach is a proof graph for the original PBES \(\mathcal {E}\), and the witness we extract from it is a witness for the model checking problem encoded by \(\mathcal {E}\).
4 Implementation and Evaluation
The mCRL2 toolset [4] supports the original approach to extract evidence from PBESs [35] in the explicit model checking tool pbessolve. We have extended this tool with the approach described in Sect. 3. PBES \( core (\mathcal {E})\) is explored and solved explicitly. Instead of precomputing \( combine ( true (\mathcal {E}), \textrm{PG}( core (\mathcal {E})))\), the corresponding right-hand sides are computed on-the-fly during explicit exploration. Solving is done using an explicit version of the recursive algorithm [36] that results in a minimal proof graph [35].
We have also extended the tool pbessolvesymbolic, that supports symbolic solving of PBESs [24], with a hybrid approach that enables evidence generation for symbolic model checking. In this approach, \( core (\mathcal {E})\) is represented and solved symbolically. This results in a symbolic characterisation of \(\textrm{PG}( core (\mathcal {E}))\). To obtain this proof graph, the symbolic implementation of the recursive algorithm [36] has been extended in such a way that an over-approximation of the proof graph is efficiently computed.1 To reason symbolically about the underlying proof graph, the PBES must be in standard recursive form (SRF) [28], i.e., every right-hand side is either disjunctive or conjunctive. Any PBES can be transformed into this format. Exploring and solving \( combine ( true (\mathcal {E}), \textrm{PG}( core (\mathcal {E})))\) is done explicitly as before. The implementation here instead uses the symbolic proof graph to compute right-hand sides on-the-fly.
4.1 Experimental Setup
We evaluate the effectiveness of our approach using a number of mCRL2 specifications with \(\mu \)-calculus formulas. Each mCRL2 specification is linearised into an LPE, and combined with a \(\mu \)-calculus formula into a PBES encoding the corresponding model checking problem. To evaluate the effect of our improvements we compare the six different approaches to solve PBESs that are available in the mCRL2 toolset. For explicit model checking, we compare directly solving the PBES with information about evidence [35] (n-expl), and our own approach (expl). For symbolic model checking, the comparison is similar, but we use the symbolic algorithms from [24] to directly solve the PBESs with evidence (n-symb). We compare it to the hybrid implementation of our approach (symb). To illustrate the overhead of solving PBESs with information about evidence, we also include directly solving the PBES without that information explicitly [4, 16] (noCE-expl), and symbolically (noCE-symb) [24].
The experiments are run using different types of models. This includes our running example scaled to \(M=1000\) (witness1000). We also use models based on industrial applications: the Storage Management System (SMS) and the Workload Management System (WMS) of the DIRAC Community Grid Solution for the LHCb experiment at CERN [31]; the IEEE 1394 (1394-fin) interface standard that specifies a serial bus architecture for high-speed communications [14]; two versions of the ERTMS Hybrid Level 3 train control system specification each with a different implementation of the Trackside System [2], immediate update (ertms-hl3) and simultaneous update (ertms-hl3su); and a Mechanical Lung Ventilator [12] (MLV). Moreover, we include a model of the onebit sliding window protocol (onebit) with buffers of size 2; and a model of the Hesselink’s handshake register [18] (hesselink). For each of these models we verify requirements that are described in the corresponding papers.
The aforementioned models are selected taking into account different criteria. We include problems that hold (
), and ones that do not hold (
); problems for which the evidence is small, and ones for which it is large. We select problems that are well studied in the literature and for which the explicit and symbolic approach can be compared (SMS, hesselink, 1394-fin, onebit). Also, we include all problems publicly available in mCRL2 that cannot be solved explicitly but only symbolically (ertms-hl3su, ertms-hl3, MLV, WMS). These are representative of the models we encounter in industrial applications.
All experiments are run 10 times, on a machine with 4 Intel 6136 CPUs and 3TB of RAM, running Ubuntu 20.04. We used a time-out of 1 hour (3600 seconds), and a memory limit of 64GB. For models ertms-hl3, WMS and MLV only the cases noCE-symb and symbolic were run 10 times. A preliminary experiment showed that all other cases either time-out or run out-of-memory. A reproduction package is available in https://doi.org/10.5281/zenodo.14616612.
Table 3.
Experimental results for model checking, reporting number of vertices in the relevancy graph, and the mean total time over 10 runs (highlighted). For expl and symb we report the number of vertices in the relevancy graph after the second solving; the first solving results in the numbers reported in noCE-expl and noCE-symb, respectively. For every case, the fastest a) of n-expl and expl, and b) of n-symb and symb are highlighted.
Dummy
4.2 Results and Discussion
The results are presented in Table 3. We highlight the fastest run with evidence information for both the explicit and symbolic cases. We report the number of vertices in the relevancy graph generated to solve the model checking problem and the mean total running time of ten runs in seconds (‘t-o’ for time-out, ‘o-o-m’ for out-of-memory). Standard deviation is typically below 10% of the mean.2
We focus our discussion on the approaches that support evidence generation. For the explicit implementation, our approach (expl) is typically comparable with the original approach (n-expl). In some cases, our approach reduces the running time of the verification in comparison with the original one, e.g., for model onebit and requirement messReadInevSent. In these cases the evidence is small, and the running time is similar to that of solving the PBES without additional information (noCE-expl). In other cases, expl has some overhead, e.g., for model 1394-fin and requirement noDoubleConfirmation. Closer inspection suggests the evidence in these cases comprises most of the state space. Since our expl approach is a two-step approach, essentially the full exploration is performed twice, resulting in a larger running time. This suggests evidence should be typically generated if small; otherwise, a tool option could notify the user.
Moreover, the experiments show that our approach for evidence generation for symbolic model checking (symb) always outperforms the original approach (n-symb), enabling evidence generation for symbolic model checking, which was infeasible so far. Sometimes, the number of vertices after the second solving is larger due to the over-approximation of the proof graph symbolically extracted from \( core (\mathcal {E})\). See, e.g., model onebit and requirement messReadInevSent.
5 Conclusion
In this paper we have described an approach to solving PBESs that allows for efficient evidence generation. Our approach solves a PBES without evidence information and uses its solution to simplify solving the PBES with evidence information described in [35]. We have established correctness of our approach, and implemented it in mCRL2 [4] as part of an explicit and a symbolic model checker. For explicit model checking, the performance is comparable to the original approach to evidence generation from [35]. If the counterexample is small, little overhead is incurred compared to solving the PBES without evidence information. Our approach makes evidence generation from PBESs efficient for symbolic checking, whereas this was not feasible before.
We plan to integrate our approach with other optimisations in the PBES solvers in mCRL2, and to preserve evidence information in static analysis techniques that are often used as preprocessing [20, 29].
Acknowledgements
This work was supported by the National Growth Fund through the Dutch 6G flagship project “Future Network Services”, MACHINAIDE (ITEA3, No. 18030), and Cynergy4MIE (ChipsJU, No. 101140226).
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The edge relation is over-approximated to achieve a compact symbolic representation, but it remains a valid proof graph (that is not necessarily minimal).
The SDs for the only cases where it exceeds 10% of the mean are: case noCE-explSMSeventuallyDeleted and noTransitFromDeleted: 0.1; case noCE-symbhesselink: 3.2, 1394-finnoDoubleConfirmation: 5.3 and noDeadlock: 4.9, WMSnoZombieJobs: 3.0; and case n-symbWMSjobFailedToDone: 6.3 and noZombieJobs: 8.0.
), and ones that do not hold (
); problems for which the evidence is small, and ones for which it is large. We select problems that are well studied in the literature and for which the explicit and symbolic approach can be compared (SMS, hesselink, 1394-fin, onebit). Also, we include all problems publicly available in mCRL2 that cannot be solved explicitly but only symbolically (ertms-hl3su, ertms-hl3, MLV, WMS). These are representative of the models we encounter in industrial applications.
