On the Verification of Weighted Kripke Structures Under Uncertainty

Abstract

We study the problem of checking weighted CTL properties for weighted Kripke structures in presence of imprecise weights. We consider two extensions of the notion of weighted Kripke structures, namely (i) parametric weighted Kripke structures, having transitions weights modelled as affine maps over a set of parameters and, (ii) weight-uncertain Kripke structures, having transition labelled by real-valued random variables as opposed to precise real valued weights.

We address this problem by using extended parametric dependency graphs, a symbolic extension of dependency graphs by Liu and Smolka. Experiments performed with a prototype tool implementation show that our approach outperforms by orders of magnitude an adaptation of a state-of-the-art tool for WKSs.

Work supported by the Advanced ERC Grant nr. 867096 (LASSO).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The rapid diffusion of cyber-physical systems (CPSs) poses the challenge of handling their growing complexity, while meeting requirements on correctness, predictability, performance without compromising time- and cost-to-market. In this respect, model-driven development is a promising approach that allows for early design and verification and may be used as the basis for systematic testing of a final product. The verification of cyber-physical systems should not only address functional properties but also a number of non-functional properties related to the quantitative aspects that are typical of such systems.

In the area of model checking, a number of modelling formalisms have emerged, allowing for quantitative aspects to be expressed. Among these, Weighted Kripke structures (WKSs) were proposed as a natural extension of the usual notion of Kripke structures with a (real-valued) weighted transition relation [8].

Interesting properties of WKSs may be expressed by means of quantitative extensions of CTL. There are different ways of extending CTL with quantitative information. Fahrenberg et al. [8] proposed to generalise the classical Boolean interpretation of CTL to a map that assigns to states and temporal formulas a real-valued distance describing the degree of satisfaction. This paper considers weighted CTL (WCTL), an extension of CTL with weight-constrained modalities, because it is an expressive logic with efficient tool support for WKSs [9].

Fig. 1.

(Left) A lawn mower example from [9]; (Right) the lawn mower model with weights parametric in p, q and, r.

Consider the WKS in Fig. 1(left) representing a grass field with different routes a lawn mower can take from the starting state $s_0$ to $s_6$ where the grass can be dumped. The weights on the transitions represent the amount of grass that is accumulated in the container when selecting a particular route. Assume that the lawn mower breaks when it is forced to store more than 6.5 units of grass, then the property “the grass is always dumped before the lawn mower breaks, irrelevant of the selected route” is expressed in WCTL as $\forall ( mow \mathbin {\mathcal {U}_{\le 6.5}} dump )$.

The above example models the accumulated grass by means of precise weight values. This is an unrealistic simplification, since the amount of mowed grass may vary depending on different factors (e.g., distribution of the grass in the field, meteorologic conditions, etc.) that cannot be modelled with precise values. The same argument applies to CPSs, that typically rely on sensor measurements which are inherently imprecise.

Typically, there are two ways for dealing with uncertain sensor measurements: (i) determine the precision of the instrument and associate an error $\epsilon$ with each measurement, or (ii) perform estimation statistics (e.g., by recursive Bayesian estimation [14]) and associate a probability distribution with each measurement.

In this paper we aim at providing adequate formal basis and tool-support for the verification of WKSs in presence of imprecise weights. We consider two extensions of the notion of WKS: (i) parametric weighted Kripke structures (pWKSs), having weights depending on a set of parameters (cf. Fig. 1(right)) and, (ii) weight-uncertain Kripke structures (WUKSs), having as weights real-valued random variables as opposed to precise real values. On the one hand, verification of pWKSs is done by inferring constraints over its parameters characterising the valuations that ensure correctness then, verify the robustness of the model within the given precision. On the other hand, verifying WUKSs consists of measuring the degree of satisfaction of the model w.r.t. the given specification.

Our contribution is twofold. First, we extend and improve the model checking algorithm of [5] for pWKSs. In contrast with [5], our method supports negation and implements an efficient termination condition. In line with [5, 6, 9], our algorithm uses an extension of dependency graphs by Liu and Smolka [11] to model-check pWKSs. Specifically, we integrate cover-edges from [9] and negation-edges from [6] and, lift the computation of fixed points from the boolean domain to that of non-negative real-valued maps to cope with parametric weights and the non-monotonic reasoning necessary to deal with negation.

As for our second contribution, we introduce the notion of weight-uncertain Kripke structures and address two natural problems related to their analysis: (i) checking whether the expected behaviour of the model satisfies a given specification and, (ii) measuring the probability that a concrete realisation of the model satisfies a given WCTL formula.

The proposed model checking framework has been implemented on a prototype tool. Experiments show that our approach considerably improves w.r.t. the PVTool from [5] and outperforms an adaptation of the WKTool from [9].

We refer to the full version of this paper [2] for the omitted proofs.

Related Work. Our paper fits within the area of weighted automata [7] where weights come as elements of a semi-ring. By combining the tropical and the probability semi-rings, one obtains probabilistic weighted automata (PWA) [1, 4]. There, transitions are labelled with a cost and a probability and the weight that the PWA assigns to a word is the expected accumulated costs of the runs producing the word. A similar approach is seen with Markov reward models whose analysis consider the computation of the expected reward for reachability properties or their verification against probabilistic reward CTL [3]. In contrast to PWAs and Markov reward models, where transitions are executed probabilistically and the weights are fixed, WUKSs choose transitions non-deterministically and generate weights according to the given probability distributions.

Fahrenberg et al. [8] consider the verification of WKSs with respect to two interpretations of WCTL where the satisfaction of a formula by a model is no longer interpreted in the Boolean domain, but rather assigns to a state a truth value in the domain of extended non-negative reals where a smaller value means a better match of the specified weights in the formula. Differently from [8], we keep the classical boolean interpretation of WCTL and measure how likely is the model to be correct. In this respect, our approach resembles that of probabilistic LTL model checking for Markov chains [3, 15].

2 Weighted Kripke Structures and Weighted CTL

In this section we present weighted Kripke structures (WKSs) as an expressive modelling formalism for quantitative systems, and weighted CTL (WCTL), an extension of computation tree logic (CTL) with weight-constrained modalities, interpreted with respect to WKSs.

We denote by $\mathbb {R}$, $\mathbb {Q}$, and $\mathbb {N}$ respectively the sets of real numbers, rational numbers, and natural numbers. We write $\mathbb {R}_{\ge 0}$ (resp. $\mathbb {Q}_{\ge 0}$) to denote the set of non-negative real (resp. rational) numbers.

Definition 1

(WKS). A weighted Kripke structure is a tuple $\mathcal {K} = (S, R, \ell )$, where S is a finite nonempty set of states, $R \subseteq S \times \mathbb {R}_{\ge 0}\times S$ is a finite weighted transition relation and $\ell :S \rightarrow 2^{\mathcal {AP}}$ is a function labelling the states with subsets of $\mathcal {AP}$, where $\mathcal {AP}$ is a fixed set of atomic propositions.

Let $\mathcal {K} = (S, R, \ell )$ be a $\text {WKS}$. We write $s \xrightarrow {w} s'$ to indicate that $(s,w,s') \in R$ and, we denote with $\omega (\mathcal {K}) \in \mathbb {R}_{\ge 0}^m$ the vector of weighs of $\mathcal {K}$, where $m = |R|$. A run in $\mathcal {K}$ from $s_0 \in S$ is a (finite or infinite) sequence $\pi = (w_i, s_i)_{i \in I}$, such that $w_0 = 0$ and I is an interval of $\mathbb {N}$ containing 0 where, for all $i \in I \setminus \{0\}$, $s_{i-1} \xrightarrow {w_i} s_i$. The accumulated weight of a run $\pi = (w_i, s_i)_{i \in I}$ at position $j \in I$ is defined as $\mathcal {W}(\pi ,j) = \sum _{i = 0}^j w_i$.

We write $|\pi |$ for the length of $\pi$ (the cardinal of I); and, for $i \in I$, we write $\pi [i]$ for the i-th state in $\pi$, i.e., $\pi [i] = s_i$. A run is maximal if it has infinite length ($|\pi | = \omega$) or its last state has no outgoing transitions. $Run (\mathcal {K},s_0)$ denotes the set of all maximal runs from $s_0$ in $\mathcal {K}$.

We can now define WCTL with upper-bounds on weights. WCTL allows for state formulas describing properties about states in the system and path formulas describing properties about runs in a WKS. State formulas $\Phi , \Psi$ and path formluae $\varphi$ are constructed over the following abstract syntax

where $a \in \mathcal {AP}$ and $q \in \mathbb {Q}_{\ge 0}$.

Given a WKS $\mathcal {K} = (S, R, \ell )$, a state $s \in S$, and a run $\pi \in Run (\mathcal {K},s)$, we denote by $\mathcal {K},s \models \Phi$ (resp. $\mathcal {K},\pi \models \varphi$) the fact that the state s satisfies the state formula $\Phi$ (resp. the path $\pi$ satisfies the path formula $\varphi$). Formally, the satisfiability relation $\models$ is inductively defined as:

As usual, we can derive the logical operators , $\vee$ and $\rightarrow$ as follows: , $\Phi \vee \Psi \overset{def}{=}\lnot (\lnot \Phi \wedge \lnot \Psi )$ and, $\Phi \rightarrow \Psi \overset{def}{=}\lnot \Phi \vee \Psi$.

Example 2

Consider the WKS $\mathcal {K}$ in Fig. 1(left) described before. The WCTL state formulas $\Phi = \forall ( mow \mathbin {\mathcal {U}_{\le 6}} dump )$ and $\Phi ' = \exists ( mow \mathbin {\mathcal {U}_{\le 4}} dump )$ express respectively the properties “the grass is always dumped before the lawn accumulates more that 6 grass units, irrelevant of the selected route” and “there exists a mowing route that accumulates at most 4 grass units before dumping”. Clearly $\mathcal {K}, s_0 \models \Phi$ holds true because all paths from $s_0$ to $s_6$ accumulate at most 6 grass units, whereas $\mathcal {K}, s_0 \models \Phi '$ doesn’t hold true, because each path from $s_0$ to $s_6$ accumulates at least 5 grass units.    $\square$

3 Parametric Weighted Kripke Structures

In this section we present parametric weighted Kripke structures and demonstrate how they can be employed for verifying the robustness of WKSs in presence of imprecise weights.

Parametric weighted Kripke structures (pWKSs) model families of WKSs that rely on the same graph structure, but differ in the concrete transition weights, which are specified as expressions built over a set of parameters.

Let $\mathbf {x} = (x_1, \ldots , x_k)$ be a vector of real-valued parameters. We denote by $\mathcal {E}$ the set of affine maps $f :\mathbb {R}^k \rightarrow \mathbb {R}$ of the form $f(\mathbf {x}) = \mathbf {a} \cdot \mathbf {x} + b$, with $\mathbf {a} = (a_1, \dots , a_k) \in \mathbb {Q}_{\ge 0}^k$ and $b \in \mathbb {Q}_{\ge 0}$, i.e., $f(x_1, \ldots , x_k) = (\sum _{i=1}^{k} a_i x_i) + b$. Hereafter we may denote the map f by means of the augmented vector¹ $(\mathbf {a},b) \in \mathbb {N}^{k+1}$. Accordingly, for $f,g \in \mathcal {E}$ the map addition $(f+g)(\mathbf {x}) = f(\mathbf {x}) + g(\mathbf {x})$ is encoded as the vector addition.

Definition 3

A parametric weighted Kripke structure is a tuple $\mathcal {P} = (S, R, \ell )$, where S is a finite nonempty set of states, $R \subseteq S \times \mathcal {E} \times S$ is a finite parametric weighted transition relation and $\ell :S \rightarrow 2^{\mathcal {AP}}$ is a labelling function.

Intuitively, a $\text {pWKS}$ $\mathcal {P} = (S, R, \ell )$ defines a family of WKSs arising by plugging in concrete values for the parameters. A parameter valuation $\mathbf {v} \in \mathbb {R}^k$ is said to be admissible for $\mathcal {P}$ if for each transition $(s,f,s') \in R$ we have $f(\mathbf {v}) \ge 0$. Let $\mathcal {V}_{\mathcal {P}}$, or just $\mathcal {V}$ when $\mathcal {P}$ is clear from the context, denote the set of admissible valuations for $\mathcal {P}$. Given $\mathbf {v} \in \mathcal {V}$, we denote $\mathcal {P}(\mathbf {v})$ the WKS associated with $\mathbf {v}$. In this respect, it will be convenient to think at $\mathcal {P}$ as a partial function $\mathcal {P} :\mathbb {R}^k \rightharpoonup \text {WKS}$ with domain $\mathcal {V}_{\mathcal {P}}$. The semantics of $\mathcal {K}$, written $[\mathcal {P}]$, is defined as the image of $\mathcal {P}$, i.e., $[\mathcal {P}] = \{ \mathcal {P}(\mathbf {v}) \mid \mathbf {v} \in \mathcal {V} \}$.

A task typically addressed in the analysis of parametric Kripke structures is that of finding symbolic representations of the set of parameter valuations for which a given WCTL formula holds [5].

Formally, given a $\text {pWKS}$ $\mathcal {P} = (S, R, \ell )$, a state $s \in S$ and a state formula $\Phi$, the set of admissible valuations for which $\Phi$ holds at s is

$$\begin{aligned} \llbracket \mathcal {P},s \models \Phi \rrbracket \overset{def}{=}\big \{ \mathbf {v} \in \mathcal {V} \mid \mathcal {P}(\mathbf {v}),s \models \Phi \big \}. \end{aligned}$$

(1)

Example 4

Consider the pWKS $\mathcal {P}$ depicted in Fig. 1(right) representing a family of lawn mower models parametric in p, q and, r. Its parameters represent the amount of grass measured in different parts of the field. The admissible valuations for $\mathcal {P}$, i.e., $\mathcal {V}_{\mathcal {P}}$, are represented by the constraint

$$\begin{aligned} \alpha (p,q,r) = p \ge 0 \wedge q \ge 0 \wedge r \ge 0 \,. \end{aligned}$$

(2)

Let $\Phi = \forall ( mow \mathbin {\mathcal {U}_{\le 6.5}} dump )$ be our specification. The set of valuations satisfying $\Phi$, i.e., $\llbracket \mathcal {P},s \models \Phi \rrbracket$, is represented by the following constraint

$$\begin{aligned} \beta (p,q,r) = \alpha (p,q,r) \wedge p + 4q \le 6.5 \wedge 2p + 2q + r \le 6.5. \end{aligned}$$

(3)

Assume that we have measured $p \cong 2 \pm \epsilon$, $q \cong 1 \pm \epsilon$ and, $r \cong 0 \pm \epsilon$ where $\epsilon > 0$ is the measurement error. One can determine if $\mathcal {P}$ is robust w.r.t. $\Phi$ by checking that all possible measurement values lay in $\llbracket \mathcal {P},s \models \Phi \rrbracket$, formally

$$\begin{aligned} \mathcal {V}_{\mathcal {P}} \cap \{ (p,q,r) \mid |p - 2| \le \epsilon ,\, |q - 1| \le \epsilon ,\, |r| \le \epsilon \} \subseteq \llbracket \mathcal {P},s \models \Phi \rrbracket . \end{aligned}$$

The above can be expressed as first-order formula in theory of linear real arithmetic

$$\begin{aligned} \forall p \in [0, 2 + \epsilon ] .\, \forall q \in [0, 1 + \epsilon ].\, \forall r \in [0, \epsilon ] .\, \beta (p,q,r). \end{aligned}$$

(4)

By performing quantifier elimination (e.g., using mjollnir [12]) we reduce (4) to $\epsilon \le 0.1$, indicating that robustness for $\mathcal {P}$ is ensured iff $\epsilon$ does not exceed 0.1.

In Example 4 we showed how to exploit pWKSs to verify a simple WKSs against a given specification up-to some error.

Clearly, with an increasing complexity of the model (or the formula) it becomes necessary to have an automatic procedure to resolve (1). The following two sections are devoted to present a generalization of the model checking algorithm presented in [5] that can also accept WCTL formulas with negation.

4 Extended Parametric Dependency Graphs

Dependency graphs as originally introduced by Liu and Smolka [11] can be applied to model-checking of the alternation-free modal $\mu$-calculus, including its sub-logics like CTL. Jensen et al. [9] proposed to extend the dependency graphs framework using cover-edges and weighted hyper-edges for the verification of WKSs against negation-free WCTL formulas. Later, Christoffersen et al. [5] further generalised their approach to pWKSs by using parametric hyper-edges and cover-edges.

In this section we present an extension of the parametric dependency graph framework by incorporating a new type of edges, called negation-edges. Negation-edges were originally used in [6] for extending the applicability of dependency graphs w.r.t. CTL model checking of Petri Nets.

Definition 5

An Extended Parametric Dependency Graph (EPDG) is a tuple $\mathcal {G} = (V,H,N,C)$ where V is a nonempty set of configurations and

• $H \subseteq V \times 2^{\mathcal {E} \times V}$ is a set of hyper-edges,

• $N \subseteq V \times V$ is a set of negation-edges, and

• $C \subseteq V \times \mathbb {Q}_{\ge 0}\times V$ is a set of cover-edges.

For $v, u \in V$, we write $v \xrightarrow {f} u$ if $(v,T) \in H$ and $(f,u) \in T$; $v \Rightarrow u$ if $(v,u) \in N$; if $(v,q,u) \in C$ and v and u are said resp. the source and the target configurations of the edge. We write $v \rightsquigarrow u$ if v and u are respectively the source and target configurations of some edge in $\mathcal {G}$ and, $\rightsquigarrow ^*$ for the reflexive and transitive closure of $\rightsquigarrow$.

We identify a class of EPDGs having some convenient structural properties.

Definition 6

Let $\mathcal {G} = (V,H,N,C)$ be an EPDG. $\mathcal {G}$ is safe if

• (i) its components are finite and for all $(v,T) \in H$, T is finite.

• (ii) for all $v \in V$ $| \{ (v,u) \in N \} \cup \{ (v,q, u) \in C \} | \le 1$ and if $| \{ (v,u) \in N \} \cup \{ (v,q, u) \in C \} | = 1$ then $\{ (v,T) \in H \} = \emptyset$.

• (iii) there are no $u,v \in V$ such that and $u \rightsquigarrow ^* v$, or $v \Rightarrow u$ and $u \rightsquigarrow ^* v$.

Intuitively, to be safe an EPDG $\mathcal {G}$ needs to have (i) finitely many configurations and edges, and each hyper-edge needs to be finitely branching; (ii) each of its configurations admits at most one type of outgoing edges and no cover edges or negation edges share the same source configuration; (iii) finally, no loop in $\mathcal {G}$ shall have any cover- or negation-edges.

In the rest of the section we fix $\mathcal {G} = (V,H,N,C)$ to be a safe EPDG.

We assign to each configuration $v \in V$ a distance $d(v) \in \mathbb {N}$ counting the maximum number of negation- and cover-edges in the paths starting from v

Notice that the distance is bounded because $\mathcal {G}$ is assumed to be safe.

We define $d(\mathcal {G}) = \max _{v \in V} d(v)$. The distance value is used to identify some components $\mathcal {C}_0, \dots , \mathcal {C}_{d(\mathcal {G})}$, where $\mathcal {C}_i = (V_i, H_i, N_i, C_i)$ is the sub-EPDG of $\mathcal {G}$ induced by the configurations $V_i = \left\{ v \in V \mid d(v) \le i \right\}$. Note that by construction $N_0 = C_0 = \emptyset$.

A valuation $\mathbf {v} \in \mathbb {R}^k$ is said admissible for $\mathcal {G}$ if whenever $v \xrightarrow {f} u$ we have $f(\mathbf {v}) \ge 0$. We denote by $\mathcal {V}_{\mathcal {G}}$ the set of admissible valuations for $\mathcal {G}$.

Definition 7

An assignment A of $\mathcal {G}$ is a function $A: V \rightarrow (\mathcal {V}_{\mathcal {G}} \rightarrow \overline{\mathbb {R}}_{\ge 0})$ where $\overline{\mathbb {R}}_{\ge 0}= \mathbb {R}_{\ge 0}\cup \{\infty \}$. The set of all assignments of $\mathcal {G}$ is denoted $\mathcal {A}^{\mathcal {G}}$.

We equip $\mathcal {A}^{\mathcal {G}}$ with the partial order ${\sqsubseteq } \subseteq \mathcal {A}^{\mathcal {G}} \times \mathcal {A}^{\mathcal {G}}$ defined as

$$\begin{aligned} A_1 \sqsubseteq A_2 \quad \quad \mathrm {iff}\quad \quad \forall v \in V.\; \forall \mathbf {v} \in \mathcal {V}_{\mathcal {G}}.\; A_1(v)(\mathbf {v}) \ge A_2(v)(\mathbf {v}) \, . \end{aligned}$$

$(\mathcal {A}^{\mathcal {G}}, \sqsubseteq )$ forms a complete lattice, with bottom element $A_\bot$ and top element $A_\top$ respectively defined as $A_\bot (v)(\mathbf {v}) = \infty$ and $A_\top (v)(\mathbf {v}) = 0$ for all $v \in V$ and $\mathbf {v} \in \mathcal {V}_{\mathcal {G}}$. Given $E \subseteq \mathcal {A}^{\mathcal {G}}$ such that $E \ne \emptyset$ the greatest lower bound $\bigsqcap E$ and least upper bound $\bigsqcup E$ are defined, for arbitrary $v \in V$ and $\mathbf {v} \in \mathcal {V}_{\mathcal {G}}$, as²

$$\begin{aligned} \textstyle (\bigsqcap E)(v)(\mathbf {v}) = \textstyle \sup _{A \in E} A(v)(\mathbf {v}) \, ,&\textstyle (\bigsqcup E)(v)(\mathbf {v}) = \textstyle \inf _{A \in E} A(v)(\mathbf {v}). \end{aligned}$$

We are now ready to define the least fixed-point assignment of an EPDG $\mathcal {G}$.

Definition 8

The least fixed-point assignment for $\mathcal {G}$, denoted $A_{min}^{\mathcal {G}}$, is defined inductively on its components $\mathcal {C}_0,\ldots ,\mathcal {C}_{d(\mathcal {G})}$. For $0 \le i \le d(\mathcal {G})$, $A_{min}^{\mathcal {C}_i}$ is the least fixed-point of the function $F_i: \mathcal {A}^{\mathcal {C}_i} \rightarrow \mathcal {A}^{\mathcal {C}_i}$, defined as

where $\chi (p) = 0$ if the predicate p holds, $\infty$ otherwise. We assume that $\max \emptyset = 0$ and $\min \emptyset = \infty$.

Lemma 9

Let $i \in \{0,\dots ,d(\mathcal {G})\}$ and $\{A_j \}_{j \in \mathbb {N}} \subseteq \mathcal {A}^{\mathcal {C}_i}$ be an ascending chain. Then, $F_i(\bigsqcup _{j \in \mathbb {N}} A_j) = \bigsqcup _{j \in \mathbb {N}} F_i(A_j)$, i.e., $F_i$ is $\omega$-continuous.

Corollary 10

$F_i$ is monotonic for all $i \in \{0,\dots ,d(\mathcal {G})\}$.

By Knaster-Tarski’s fixed-point theorem, $A^{\mathcal {C}_i}_{min}$ exists for all $i \le d(\mathcal {G})$, moreover, by Kleene’s fixed-point theorem, it is the limit of the ascending chain $A_\bot \sqsubseteq F_i(A_\bot ) \sqsubseteq F_i(F_i(A_\bot )) \sqsubseteq \cdots \sqsubseteq F_i^n(A_\bot ) \sqsubseteq \cdots$, i.e., $\bigsqcup _{n \in \mathbb {N}} F_i^n(A_\bot )$.

The following result states that the limit of the above chain is reached within steps. This result is essential for our algorithm.

Lemma 11

Let $i \in \{0,\dots ,d(\mathcal {G})\}$ and . Then, $F_i^k(A^{\mathcal {C}_i}_{\bot }) = A^{\mathcal {C}_i}_{min}$.

By Lemma 11, we can compute $A^{\mathcal {G}}_{min}$ symbolically by repeated application of F until we are sure that the fixed-point has been reached. It is worth noting that our termination condition only depends on the number of configurations of the EPDG. Therefore, in contrast with [5], we don’t need to perform any symbolic comparison of the assignments to check whether a fixed-point has been reached. Not only does it simplifies the algorithm, but it also reduces the overhead caused by symbolic comparison.

Lemma 12

For any safe EPDG $\mathcal {G} = (V, H, N, C)$ and component $\mathcal {C}_i$ of $\mathcal {G}$, the symbolic computation of the least fixed-point assignment, $A^{\mathcal {C}_i}_{min}$, by repeated application of the function $F_i$ on $A^{\mathcal {C}_i}_{\bot }$ runs in time .

5 Model Checking Parametric WKSS Using EPDGs

In this section we present a reduction from the model checking problem of WCTL on pWKSs to the computation of least fixed-point assignments for EPDGs. Then, we show how to obtain from those assignments a symbolic representation of (1) as a (quantifier-free) first-order formula in the linear theory of the reals.

Given a pWKS $\mathcal {P} = (S, R, \ell )$, a state $s \in S$ and a WCTL formula $\Phi$, we construct an EPDG $\mathcal {G}$ where every configuration is a pair consisting of a state and a formula. Starting from the initial pair $\langle s, \Phi \rangle$, $\mathcal {G}$ is constructed according to the rules given in Fig. 2.

Fig. 2.

EPDG construction rules. Here $Q \in \{\exists , \forall \}$ and hyper-edges without labels shall be assumed to be labelled with the constant weight map $\mathbf {0}$.

It is worth noting that the size of $\mathcal {G}$ does not depend on the actual weight values of $\Phi$ or $\mathcal {P}$ but only on the size of $\mathcal {P}$ and the number of sub-formulas of $\Phi$.

The following result ensures that the EPDG framework described in Sect. 4 can be applied to the EPDGs constructed according to the rules in Fig. 2.

Lemma 13

The EPDG $\mathcal {G}$ rooted at $\langle s, \Phi \rangle$ is safe.

In $\mathcal {G}$ we distinguish two types of configurations: concrete configurations have concrete WCTL formulas, while symbolic configurations have symbolic formulas of the form $Q\! \mathbin {\mathcal {X}_{\le ?}} \Phi$ or $Q\Phi \mathbin {\mathcal {U}_{\le ?}} \Psi$ where $Q \in \{\exists , \forall \}$ and $\Phi ,\Psi$ are concrete WCTL formulas. Given a symbolic formula $\Phi$ and $q \in \mathbb {Q}_{\ge 0}$, we denote by $\Phi _q$ the corresponding concrete formula with bound q.

Lemma 14

Let $v = \langle s, \Phi \rangle$ be a concrete configuration of $\mathcal {G}$ and $\mathbf {v} \in \mathcal {V}_{\mathcal {G}}$ an admissible valuation. Then, $A^{\mathcal {G}}_{min}(v)(\mathbf {v}) \in \{0, \infty \}$.

The next theorem states that the set of correct valuations $\llbracket \mathcal {P},s \models \Phi \rrbracket$ corresponds to the set $\{ \mathbf {v} \in \mathcal {V}_{\mathcal {G}} \mid A^{\mathcal {G}}_{min}(\langle s, \Phi \rangle )(\mathbf {v}) \le 0 \}$. This reduces the model checking problem to the computation of least fixed-point assignments for EPDGs.

Theorem 15

Let $v = \langle s, \Phi \rangle$ be a configuration of $\mathcal {G}$ and $\mathbf {v} \in \mathcal {V}_{\mathcal {G}}$ an admissible valuation. Then, the following hold

• (1) if v is concrete, then $A^{\mathcal {G}}_{min}(v)(\mathbf {v}) = 0$ iff $\mathcal {P}(\mathbf {v}),s \models \Phi$ and,

• (2) if v is symbolic, then for all $q \in \mathbb {Q}$, $A^{\mathcal {G}}_{min}(v)(\mathbf {v}) \le q$ iff $\mathcal {P}(\mathbf {v}),s \models \Phi _{q}$.

We showed that $A^{\mathcal {G}}_{min}(\langle s, \Phi \rangle )$ can be computed symbolically as a partially evaluated expression. During the computation one can perform some simplifications (e.g., $\min \emptyset = \infty$ or $\max \emptyset = 0$), nevertheless, the parts of the expression that depend on the actual value of the parameters are left unevaluated.

By Theorem 15 we are interested in a symbolic representation of the valuations $\mathbf {v}$ such that $A^{\mathcal {G}}_{min}(\langle s, \Phi \rangle )(\mathbf {v}) \le 0$. As anticipated in Example 4, this can be done by means of a (quantifier-free) first-order formula in the linear theory of the reals. In practice, such a formula is obtained as $\Gamma \big (A^{\mathcal {G}}_{min}(\langle s, \Phi \rangle ) \le 0\big )$ where $\Gamma$ is defined by cases as follows³, for ${\bowtie } \in \{\le , >\}$, $\text {m} \in \{\min , \max \}$ and, $q \in \mathbb {Q}_{\ge 0}$

Fig. 3.

EPDG rooted at $\langle s_0, \forall ( mow \mathbin {\mathcal {U}_{\le 6.5}} dump ) \rangle$ (cf. Example 16).

Example 16

Consider the pWKS $\mathcal {P}$ and the formula $\Phi = \forall ( mow \mathbin {\mathcal {U}_{\le 6.5}} dump )$ from Example 4. In Fig. 3 is depicted the EPDG $\mathcal {G}$ rooted at $\langle s_0, \Phi \rangle$. By running our symbolic algorithm we obtain the following expression

$$\begin{aligned} A^{\mathcal {G}}_{min}(\langle s_0, \Phi \rangle ) = \chi (\max \{ p + q + \max \{p+r, 2q\}, p+ 2q + \max \{p+r, 2q\}, 2p +q \} \le 6.5) \,. \end{aligned}$$

The above expression can be then turned into the following formula

$$\begin{aligned} 2 p+q+r\le 6.5\wedge p+3 q\le 6.5\wedge 2 p+2 q+r\le 6.5\wedge p+4 q\le 6.5\wedge 2 p+q\le 6.5, \end{aligned}$$

that, in conjunction with $p \ge 0 \wedge q \ge 0 \wedge r \ge 0$ (cf. (2)) simplifies to (3).    $\square$

6 Weight-Uncertain Kripke Structures

In Sect. 3 we have seen how to use pWKSs for modelling and verifying the robustness of WKSs when the imprecision of the weights is quantified by means of an absolute accuracy error $\epsilon$. However, for an experimental weight value w, not all values in the interval $w \pm \epsilon$ are equally likely to occur in practice.

It’s common practice to model experimental measurements by means of real-valued random variables distributed according to well studied family of distribution (e.g., normal or student’s T). In this section we introduce the notion of weight-uncertain Kripke structures (WUKSs), where weights are modelled as random variables and present a WCTL model checking framework for them.

Before we start let us recall some notions from measure theory.

Measure Theory. Let $\Omega$ be a set. A family $\Sigma \subseteq 2^\Omega$ is called $\sigma$-algebra if it contains the empty set $\emptyset$ and is closed under complement and countable unions, in this case $(\Omega ,\Sigma )$ is said measurable space and elements of $\Sigma$ measurable sets. If $\Omega$ is given a topology then $\mathcal {B}(\Omega )$ denotes the Borel $\sigma$-algebra of $\Omega$, i.e., the smallest $\sigma$-algebra having all open subsets of $\Omega$. We say that $\Omega$ is a Borel space to indicate the measurable space $(\Omega , \mathcal {B}(\Omega ))$, and elements of $\mathcal {B}(\Omega )$ are called Borel sets. As an example, $\mathbb {R}$ is assumed to have the usual Euclidean topology and $\mathcal {B}(\mathbb {R})$ denotes the induced Borel $\sigma$-algebra which makes $\mathbb {R}$ a Borel space.

A measure on $(\Omega , \Sigma )$ is a $\sigma$-additive function $\mu :\Sigma \rightarrow \mathbb {R}$, i.e, a map satisfying $\mu (\bigcup _{i \in I} E_i) = \sum _{i \in I} \mu (E_i)$ for any countable family of pairwise disjoint measurable sets $(E_i)_{i \in I}$, in this case $(\Omega ,\Sigma , \mu )$ is said measure space. If $\mu$ additionally satisfies $\mu (\Omega ) = 1$, it is called probability measure and $(\Omega ,\Sigma , \mu )$ probability space.

For $(\Omega , \Sigma )$ and $(Y, \Theta )$ measurable spaces, the map $f :\Omega \rightarrow Y$ is measurable if for all $E \in \Theta$, $f^{-1}(E) = \{x \mid f(x) \in E\} \in \Sigma$. Given a measurable map $f :\Omega \rightarrow Y$ and a measure $\mu$ on $(\Omega ,\Sigma )$ we define the measure $\mu [f]$ on $(Y,\Theta )$ as $\mu [f](E)= \mu (f^{-1}(E))$, for $E \in \Theta$, a.k.a. the push forward of $\mu$ under f.

A real-valued random variable $X :\Omega \rightarrow \mathbb {R}$ is a measurable function from a probability space $(\Omega ,\Sigma , P)$ to the Borel space $\mathbb {R}$. Intuitively, X can be understood as the outcome value of an experiment (e.g., measuring some sensor value). Given a “test” $A \in \mathcal {B}(\mathbb {R})$, we write $P[X \in A]$ for the probability that X has value in A, i.e., $P[X \in A] = P[X](A)$. A random variable X is associated with its cumulative distribution function (CDF) $F_X :\mathbb {R}\rightarrow [0,1]$ defined as $F_{X}(x) = P[X \in (\infty ,x]]$; and a probability density function (PDF) $f_X$, a non-negative Lebesgue-integrable function satisfying $P[X \in [a,b]] = \int _{a}^{b} f_X(x) \text {d}x$. The expected value of X, written $\text {E}[X]$ is intuitively understood as the long-run average value of repetitions of the experiment X, formalised by the Lebesgue integral $\int _{\Omega } X \;\text {d} P$ (corresponding to $\int _{\mathbb {R}} f_X(x) \text {d}x$ when X admits density function $f_X$).

In the rest of the section we fix the probability space $(\Omega ,\Sigma , P)$ representing the environment where the experiments are performed, and we use $\mathbb {Y}$ to denote the set of real-valued random variables of the form $Y :\Omega \rightarrow \mathbb {R}$.

We are now ready to define the concept of weight-uncertain Kripke structure.

Definition 17

A weight-uncertain Kripke structure is a tuple $\mathcal {J} = (S, R, \ell )$, where S is a finite nonempty set of states, $R \subseteq S \times \mathbb {Y} \times S$ is a finite random weighted transition relation and $\ell :S \rightarrow 2^{\mathcal {AP}}$ is a labelling function.

Consider the WUKS $\mathcal {J} = (S, R, \ell )$. We denote by $\text {WKS}_{\mathcal {J}}$ the set of all $\text {WKS}$s having the same underlying graph as $\mathcal {J}$. We construct the $\sigma$-algebra $\Sigma _{\mathcal {J}}$ as the family of sets $A \subseteq \text {WKS}_{\mathcal {J}}$ whose corresponding set of weights is Borel measurable in $\mathbb {R}^m$ ($m = |R|$). Formally,

$$\begin{aligned} A \in \Sigma _{\mathcal {J}} \quad \text {iff} \quad A \subseteq \text {WKS}_{\mathcal {J}} \text { and } \{\omega (\mathcal {K}) \mid \mathcal {K} \in A\} \in \mathcal {B}(\mathbb {R}^m). \end{aligned}$$

$\mathcal {J}$ can be seen as a measurable function $\mathcal {J} :\Omega \rightarrow \text {WKS}_{\mathcal {J}}$, where $\mathcal {J}(\omega )$ is the $\text {WKS}$ associated with $\omega \in \Omega$, justifying the intuition the it represents an experiment whose outcomes are WKSs. Accordingly, the semantics of $\mathcal {J}$ is the probability space $(\text {WKS}_{\mathcal {J}}, \Sigma _{\mathcal {J}}, P[\mathcal {J}])$.

Given a WUKS $\mathcal {J}$, a state $s \in S$, and a WCLT property $\Phi$, two natural model checking questions are (i) whether the expected behaviour of $\mathcal {J}$ satisfies $\Phi$ at s, informally “$E[\mathcal {J}], s \models \Phi$”, (ii) and how likely is that a concrete instance of $\mathcal {J}$ satisfies $\Phi$ at s, denoted by $P[\mathcal {J},s \models \Phi ]$.

We address the above problems for a subclass of WUKSs having random variables $(Y :\Omega \rightarrow \mathbb {R}) \in \mathcal {E}_{\mathbf {X}}$ of the form $Y(\omega ) = \mathbf {a} \cdot \mathbf {X}(\omega ) + b$, with $\mathbf {a} \in \mathbb {Q}_{\ge 0}^k$, $b \in \mathbb {Q}_{\ge 0}$ and, where $\mathbf {X} = (X_1, \ldots , X_k)$ is vector of pairwise independent non-negative real-valued random variables⁴. Observe that, elements in $\mathcal {E}_{\mathbf {X}}$ may not be independent from each other.

From here on we consider the WUKS $\mathcal {J} = (S,\mathcal {E}, R, \ell )$ with $R \subseteq S \times \mathcal {E}_{\mathbf {X}} \times S$, and we use $\mathcal {P}$ to refer to the $\text {pWKS}$ obtained by replacing the random variables $X_i$ in $\mathcal {J}$ with the parameters $x_i$ (for $i = 1..k$).

Let’s consider the first question, namely “$E[\mathcal {J}], s \models \Phi$”. There, $E[\mathcal {J}]$ was informally denoting the WKS obtained by replacing each transition weight in $\mathcal {J}$ with the corresponding expected value. Formally, $E[\mathcal {J}]$ is defined as the unique $\mathcal {K} \in \text {WKS}_{\mathcal {J}}$ such that $\omega _i(\mathcal {K}) = \int _{\text {WKS}_{\mathcal {J}}} \omega _i \;\text {d} P[\mathcal {J}]$ for all $i \in \{1,\dots ,m\}$ where $\omega _i :\text {WKS}_{\mathcal {J}} \rightarrow \mathbb {R}_{\ge 0}$ is the function that returns the i-th weight from a given WKS.

The assumption made on the weights in $\mathcal {J}$ allows us to rephrase $E[\mathcal {J}], s \models \Phi$ as a model checking problem for $\mathcal {P}$.

Lemma 18

$E[\mathcal {J}], s \models \Phi$ if and only if $E[\mathbf {X}] \in \llbracket \mathcal {P},s \models \Phi \rrbracket$.

We are now ready to address the second question, that is formalised as follows

$$\begin{aligned} P[\mathcal {J},s \models \Phi ] \overset{def}{=}P[\mathcal {J}](\{ \mathcal {K} \in \text {WKS}_{\mathcal {J}} \mid \mathcal {K},s \models \Phi \}) \,. \end{aligned}$$

(5)

For the above definition to be well-defined the set $\{ \mathcal {K} \in \text {WKS}_{\mathcal {J}} \mid \mathcal {K},s \models \Phi \}$ needs to be a measurable event in $\Sigma _{\mathcal {J}}$. The following result ensures that.

Lemma 19

$\{ \mathcal {K} \in \text {WKS}_{\mathcal {J}} \mid \mathcal {K},s \models \Phi \} \in \Sigma _{\mathcal {J}}$

The following theorem characterizes the model checking problem for the WUKS $\mathcal {J}$ in terms of the model checking problem of its associated pWKS $\mathcal {P}$.

Theorem 20

$P[\mathcal {J},s \models \Phi ] = P[\mathbf {X} \in \llbracket \mathcal {P},s \models \Phi \rrbracket ]$.

Remark 21

For the sake of clarity, so far we have assumed that $\mathbf {X}$ is non-negative real-valued random vector. However, provided that $P[\mathbf {X} \in \mathcal {V}_{\mathcal {P}}] > 0$, the non-negativity assumption can be dropped by replacing the probability distribution $P[\mathbf {X}]$ with the conditional probability $P[\mathbf {X} | \mathbf {X} \in \mathcal {V}_{\mathcal {P}}]$.

By Theorem 20 we can estimate the value p of (5) by applying Monte Carlo simulation techniques. For this, we sample n independent repetitions of $\mathbf {X}$, associating with each repetition a Bernoulli random variable $B_i$. A realisation $b_i$ of $B_i$ is 1 if the corresponding sampled value of $\mathbf {X}$ lays in $\llbracket \mathcal {P},s \models \Phi \rrbracket$, and 0 otherwise. Finally, we estimate p by means of the observed relative success rate $\tilde{p} = (\sum _{i = 1}^n b_i ) / n$. The absolute error $\varepsilon$ of the estimation can be bound with a certain degree of confidence $\delta \in (0,1]$ by tuning the number of required simulations based on the inequality $P(|\tilde{p} - p| \ge \varepsilon ) \le \delta$ where $\delta = e^{-2 n \varepsilon ^2}$ (cf. [10, 13]). Therefore the required number n of samples is obtained as

$$\begin{aligned} n = \left\lceil - \frac{\ln (\delta )}{2 \varepsilon ^2} \right\rceil . \end{aligned}$$

(6)

Example 22

Consider the WUKS $\mathcal {J}$ depicted in Fig. 1(right), where p, q and, r shall now be interpreted as real-valued random variables distributed as $p \sim \mathcal {N}(2,\epsilon )$, $q \sim \text {unif}(1 - \epsilon , 1 + \epsilon )$, and $r \sim \mathcal {N}(0,\epsilon )$ for $\epsilon = 0.1$. We can estimate $P[\mathcal {J},s_0 \models \Phi ] = 0.959$ with an error $\varepsilon = 0.003$ and confidence of $99,9 \%$ (i.e., $\delta = 0.001$) by generating $n = 383765$ samples.

7 Experimental Results

To evaluate the performance of the algorithms discussed in this paper, we developed a prototype tool suite for WCTL model checking of WKSs under uncertain weights. The tool suite consists of two parts: a back-end, called PVTool2⁵ and a front-end, called UVTool⁶. UVTool supports the verification of pWKSs and WUKSs as described in Sects. 5 and 6 making use of the PVTool2 which implements the EPDG construction and the symbolic fixed-point computation.

We have evaluated the PVTool2 and the UVTool separately.

Evaluation of the PVTool2. We compared the performance of the PVTool2 with the PVTool from [5]. For a fair comparison we used as benchmarks the vacuum cleaner models from [5] checking them against the WCTL formula $\exists (\forall dirty \, \mathcal {U}_{\le 10} clean )\, \mathcal {U}_{\le 1000} \, done$. The table depicted in Fig. 4a reports the results obtained by increasing the number of rooms in the vacuum cleaning model. The first and the second columns respectively present the number of states of the model and the number of configurations of the resulting EPDG, while the last two columns present respectively the computation time and the memory consumption of the two tools. The results of the experiments show that the PVTool2 performs worse than the PVTool on small models but it scales way better than the PVTool both in terms of computation time and memory consumption. This may be due to the fact that our algorithm does not perform any comparison of the symbolic assignments during the fixed-point computation. The improvement is measured when the overhead of the symbolic comparison exceeds the cost of the additional iterations required by the PVTool2.

Figure 4b shows how the computation time and memory consumption of the PVTool2 grows linearly in the number of configurations of the EPGD.

Fig. 4.

Experiments on an Intel i7 ($5^{\text {th}}$ gen.) 2.6 GHz processor with 12 GB RAM

Evaluation of the UVTool. For the verification of WUKS, our algorithm first samples valuations from $\mathbf {X}$, then estimates the relative number of valuation-samples that are correct in the sense of (1). Alternatively, one could first sample WKSs from the given WUKS and then estimate the relative number of models that satisfy the specification. In the second approach one could employ the WKTool⁷ and exploit the efficient local algorithm from [9].

We compared the two approaches on the WUKS of Example 22 and performed the evaluation with increasing precision and accuracy of the estimation. The results are presented in Table 1. The first three columns report the error, the confidence and the number of generated samples (cf. Eq. (6)), and the last two columns present the computation time respectively for the UVTool and the adaptation of the WKTool. It is worth mentioning that the values reported in the last column do not consider the time required to sample and generate the models, but only the total time used for the model checking. The results clearly show that our approach outperforms the second one by several orders of magnitude, showing that computing the symbolic representation of the correct valuations in advance gives a huge speed-up in the overall computation time.

Table 1. Experiments on an Intel Core i5 3.1 GHz with 8 GB RAM.

8 Conclusion and Future Work

We addressed the model checking problem of weighted Kripke structures under uncertainty. We proposed to employ parametric weighted Kripke structures and weight-uncertain Kripke structures for modelling WKSs with imprecise real-valued weights. For the verification of pWKSs against WCTL formulas we developed a model checking algorithm that, compared with [5], implements an improved termination condition and accepts formulas with negation. The algorithm, given a pWKS and a WCTL formula, and produces a quantifier free first-order formula in the linear theory of the reals representing the set of parameter valuations satisfying the specification. The outcome formula is then used as underlying ingredient for verifying the robustness of WKSs. If the imprecision of the weights by means of an absolute accuracy error the verification can be performed via quantifier elimination (cf. Example 4). Otherwise, if the imprecision is quantified by mean of random variables, the probability of satisfying the specification in estimated via Monte Carlo simulation techniques (cf. Example 22).

In the future we plan to consider an alternative semantic interpretation for WUKSs where the random weights are dynamically sampled while unfolding the model, thus modelling WKSs with an infinite state space. This alternative semantics would fit well in the contexts of reactive systems that respond to external stimuli whose values are uncertain. Another direction for future work would be to consider the model checking of weighted LTL properties under uncertainty.