Model Checking Branching Time Properties for Incomplete Markov Chains

Abstract

In this work, we discuss a numerical model checking algorithm for analyzing incompletely specified models of stochastic systems, specifically, Discrete Time Markov Chains (DTMC). Models of a system could be incompletely specified for several reasons. For example, they could still be under development or, there could be some doubt about the correctness of some components. We restrict ourselves to cases where incompleteness can be captured by expanding the logic of atomic propositions to a three valued logic that includes an unknown truth value. We seek to answer meaningful model checking queries even in such circumstances.

The approach we adopt in this paper is to develop the model checking algorithm from first principles. We develop a tool based on the algorithm and compare the performance of this approach with the indirect approach of invoking a binary model checker.

1 Introduction

Probabilistic models are widely used to represent real-world systems that exhibit stochastic behaviour, like cyber-physical systems, biological processes, network and security protocols. Examples of such probabilistic models are Markov chains like Discrete and Continuous Time Markov Chains (DTMC and CTMC respectively) [3], Markov Decision Processes (MDP), Constrained Markov Chains [8] and Probabilistic Automata [13]. Verification of these types of probabilistic models involves asserting whether or not the system design exhibits the required behavior. The required behavior or property is formally specified as statements in logics like Probabilistic Computation Tree Logic (PCTL) [16] and Continuous Stochastic Language (CSL) [4].

Probabilistic Model Checking is a formal technique to analyze and verify the required behaviour of stochastic systems. Given a probabilistic model that describes a stochastic system, and a formal specification of the required behaviour of the system, the goal of probabilistic model checking is to decide whether the system exhibits the required behaviour or not. Probabilistic model checking has been explored in the literature using either numerical [4, 12, 16] or statistical algorithms [22, 23, 25].

Traditionally, systems are analyzed through model checking once the entire information about a model is available, at least in principle. An interesting question is if this analysis can be done when the model has incomplete information. The incompleteness may arise because of either (i) nonavailability of input information about either state space or transitions between states, (ii) if the correctness of some module is in doubt or (iii) loss of information due to abstraction of models, or some combination of the three. To capture incomplete information, a natural choice is to expand binary logic to include a third unknown truth value. We denote this by the question mark “?”. Depending upon the type of incompleteness, different techniques have been reported to verify both stochastic as well as non stochastic incomplete models.

There exists a significant body of work on model checking with three valued logics. Bruns and Godefroid [6, 7] use three valued modal logic to represent models with partial state space. These models are then verified by using model checking algorithms for binary truth values. Similarly, Chechik et al. [11] used multi-valued logic to represent incomplete and inconsistent information in a model. They verified such a model using a symbolic multi-valued CTL model checker. Abstraction is often used to deal with problems of state space explosion in model checking. However, such an approach may cause loss of information in the model. This incompleteness in the abstracted model can be represented using a third truth value. Godefroid et al. [15] and Chechik [10] discussed the verification of abstracted models using three valued LTL and CTL model checkers, respectively. Abstraction is also commonly used in verification of stochastic models like Markov chains, to overcome the problem of state-space explosion [14, 17, 19]. Besides abstraction, incompleteness in stochastic systems may arise from imprecise transition probabilities obtained from statistical experiments. For example, discrete-time Markov chains have been defined wherein transition probabilities are intervals instead of exact values to handle imprecision [18, 20]. Verification of such interval based discrete-time Markov chains works by either reducing it to a class of discrete-time Markov chains or to a Markov decision process [5, 9, 24].

Another way of capturing incomplete information, the one on which this paper is based, is to allow some atomic propositions to assume the “?” truth value in some states [2]. An interesting question is to determine which properties of the system can be verified in the absence of complete information–is there sufficient information in the model to evaluate a particular property to either True or False? It is possible to answer this question by invoking PCTL model checking algorithms twice [2]. We refer to this approach as 2MC.

In this paper, we adopt a direct approach that solves the numerical model checking problem from first principles as exposited in [4, 21]. We call this approach 1MC. While this approach is an adaptation of the standard numerical model checking algorithm, the fact that true and false are no longer complementary to each other raises some complications, which we address. We also show examples to illustrate the approach and practical applications of the problem formulation and the solution.

Intuitively, one expects the 1MC algorithm to perform better in cases when the 2MC algorithm has to invoke the model checker twice and 2MC to perform better when it needs to invoke it only once. We back this intuition up with experimental evidence.

The rest of the paper is arranged as follows. Section 2 discusses the syntax and semantics of the modeling and specification formalism for incomplete models. Section 3 discusses the model checking algorithm. Implementation details, results and comparison with 2MC are discussed in Sect. 4. Section 5 concludes the paper with a brief discussion on future directions.

2 qDTMC and qPCTL

2.1 Discrete Time Markov Chain with Question Marks (qDTMC)

A Discrete Time Markov Chain with question marks (qDTMC) extends the traditional DTMC to account for incomplete information in a model.

Definition 1

A qDTMC is a tuple $\mathcal {M} = (S, i_{init},\mathbb {P},AP,L)$ where

• S is a finite non-empty set of states,

• $i_{init}: S \rightarrow [0,1]$ is the initial distribution, such that $\sum \limits _{s \in S} i_{init} (s)=1$,

• $\mathbb {P}:S\times S \rightarrow [0,1]$ gives the transition probability between two states in S such that:

  $$ \forall s\in S : \sum _{s'\in S} \mathbb {P}(s,s') = 1, $$

• AP is a set of atomic propositions, and

• $L:S\times AP\rightarrow \{T,F,{\varvec{?}}\}$ assigns a truth value from the set $\{T,F,{\varvec{?}}\}$ to each atomic proposition $a \in AP$ in a state $s \in S$.

A qDTMC differs from a DTMC only in terms of its labelling function. The truth values T and F correspond that an atomic proposition being true and false respectively in the state s. If it is not known whether an atomic proposition is true or false in s, then the truth value ? is assigned to the atomic proposition.

Fig. 1.

Example of a qDTMC

Figure 1 illustrates an example qDTMC $\mathcal {M}$ wherein the state $s_0$ is the initial state with probability 1 in the state space $S=\{s_0,s_1,...,s_6\}$. The weight on each transition between the states denotes the probability of the transition. $AP=\{p,q\}$ is a set of atomic propositions in $\mathcal {M}$. The truth value of each atomic proposition in a state is also represented in the qDTMC. For instance, $\lnot p q?$ denotes p is false and q is unknown in the state $s_0$ and pq denotes both p and q are true in the state $s_2$. We consider qDTMC $\mathcal {M}$ as a running example in the paper.

Definition 2

A path $\pi$ in a qDTMC $\mathcal {M}$ is a sequence of states $s_{0}, s_{1}, s_{2}, \ldots$ such that for all $i=0, 1, 2, \ldots \ s_{i}\in S$ and $\mathbb {P}(s_{i},s_{i+1}) > 0$. The $i+1^{th}$ state in a path $\pi$ is denoted by $\pi [i]$. The set Path(s) is the set of all infinite paths starting from state s in $\mathcal {M}$.

Definition 3

A cylinder set $C(\omega )$ is the set of all infinite paths with a common finite prefix $\omega = s_0,s_1,\ldots , s_n$. The probability measure $\mu$ of $C(\omega )$ in the qDTMC $\mathcal {M}$ can be defined as

$$ \mu (C(\omega ))= \prod _{i=0}^{n-1} \mathbb {P}(s_i,s_{i+1}) $$

2.2 qPCTL

Probabilistic Computation Tree Logic with question marks (qPCTL) is an extension of PCTL [16], defined to formally express a property required of a qDTMC model. In what follows, our notational convention will be similar to that of [2]. The syntax of qPCTL is the same as that of PCTL:

Syntax:

where $\varPhi$, $\varPhi _{1}$, and $\varPhi _{2}$ are state formulas, $\psi$ is a path formula, a is an atomic proposition, $\theta \in [0,1]$ defines the probability constraint, $\bowtie \ \in \{\ <, \ >,\ \le ,\ \ge \}$ represents the set of comparison operators, and $k\ \in \ \mathbb {N}\$ is the time bound. The X, U, and $U^{\le k}$ operators are called Next, Until and Bounded Until respectively.

Recall that an atomic proposition a can have one of the three truth values $\{T,F,?\}$ in a qPCTL formula. Thus, in addition to verifying a property as true (T) or false (F), a qPCTL formula can also be evaluated to “unknown” (${\varvec{?}}$). The conditions for which the logic returns ${\varvec{?}}$ are incorporated into the semantics of qPCTL.

For the truth values (T, F, ?) in qPCTL, the logical operations ($\wedge$, $\vee$, $\lnot$) are as defined in Tables 1, 2 and 3.

Table 1. The AND operator

Table 2. The OR operator

Table 3. The NOT operator

Semantics:

Each state formula $\varPhi$ in qPCTL is verified to either T, F, or ${\varvec{?}}$ in a state $s \in S$ that is $(s,\varPhi )=\{T,F,?\}$ as:

• 1. The qPCTL formula $\varPhi$ can trivially be $\top$.

  $$\begin{aligned} \begin{array}{c} (s,\top ) = T; \quad \quad (s,\lnot \top ) = \lnot (s,\top )=\ F. \end{array} \end{aligned}$$

• 2. An atomic proposition a in a qDTMC can have three possible truth values $\{T,F,?\}$. Thus, a qPCTL formula $\varPhi = a$ in a state s is evaluated to $\{T,F,?\}$ if

  $$\begin{aligned} (s, a) = \left\{ \begin{array}{ccc} T &{} \text {iff} &{} L(s,a)=T\\ F &{} \text {iff} &{} L(s,a)=F \\ ? &{} \text {iff} &{} L(s,a)=? \end{array} \right. \end{aligned}$$

• 3. Using the NOT and AND operator from Tables 3 and 1 respectively, we have:

  $$\begin{aligned} (s, \lnot \varPhi ) = \left\{ \begin{array}{ccc} T &{} \text {iff} &{} (s,\varPhi )=F\\ F &{} \text {iff} &{} (s,\varPhi )=T\\ ? &{} \text {iff} &{} (s,\varPhi )=? \end{array} \right. \text {and } (s, \varPhi _{1}\wedge \varPhi _{2}) = \left\{ \begin{array}{rl} T &{} \text {iff }(s,\varPhi _{1})=T \wedge (s,\varPhi _{2})=T \\ F &{} \text {iff }(s,\varPhi _{1})=F \vee (s,\varPhi _{2})= F \\ ? &{} \text {otherwise} \end{array} \right. \end{aligned}$$

• 4. If a qPCTL formula contains a probabilistic operator that is $\varPhi = Pr_{\bowtie \theta }[\psi ]$, then the probability measure of paths starting from state s that evaluate path formula $\psi$ to true or false is calculated separately. The formula $\varPhi$ is then verified as follows:

  $$\begin{aligned}{ (s, Pr_{\bowtie \theta }[\psi ])=\left\{ \begin{array}{rl} T &{} \text {if } \mu \{\pi \in Path(s):(\pi ,\psi )=T\} \bowtie \theta \\ F &{} \text {if } \mu \{\pi \in Path(s):(\pi ,\psi )=F\} \bowtie 1-\theta \\ ? &{} \text {otherwise} \end{array} \right. } \end{aligned}$$

A path formula $\psi$ for a path $\pi \in Path(s)$ has the following semantics:

• 1. Next operator: A path formula of form $\psi = X \varPhi$ is verified to $\{T,F,?\}$ for a path $\pi$ if the state formula $\varPhi$ is evaluated to $\{T,F,?\}$, respectively, in the second state of $\pi$.

  $$\begin{aligned} (\pi , X\varPhi ) = \left\{ \begin{array}{rl} T &{} \text {if } (\pi [1],\varPhi )=T\\ F &{} \text {if } (\pi [1],\varPhi )=F \\ ? &{} \text {if } (\pi [1],\varPhi )=\ ? \end{array} \right. \end{aligned}$$

• 2. Until operator:

  $$\begin{aligned} (\pi , \varPhi _1 U \varPhi _2) = \left\{ \begin{array}{rl} T &{} \text {if } \exists i: (\pi [i],\varPhi _2)=T \ \wedge \ \forall i'< i: (\pi [i'],\varPhi _1)=T\\ F &{} \text {if } (\forall i:( \pi [i],\varPhi _2)=F) \\ &{} \ \vee \ [\exists i : (\pi [i],\varPhi _2)=T \ \wedge \ \exists i'< i :(\pi [i'],\varPhi _1)=F] \\ ? &{} \text {otherwise}. \end{array} \right. \end{aligned}$$

  Thus, $\psi$ evaluates to ? if one of the following occurs:

  • $\varPhi _2$ is ? for all the states in $\pi$.

  • $\varPhi _2$ is ? for at least one state in $\pi$ and is never T in any of the states along the path and $\varPhi _1$ is never F.

  • $\varPhi _2$ is T for some state $\pi [i]$ and $\varPhi _1$ is ? for at least one state $\pi [k]$ with $k<i$ but never F in any of the states upto $\pi [i]$.

• 3. Bounded Until: A path formula of the form $\psi = \varPhi _1 U^{\le k} \varPhi _2$ is verified to $\{T,F,?\}$ same as that for until operator, but only for paths of finite length k.

  $$\begin{aligned} (\pi , \varPhi _1 U^{\le k} \varPhi _2) = \left\{ \begin{array}{rl} T &{} \text {if } \exists i\le k: (\pi [i],\varPhi _2)=T \ \wedge \ \forall i'< i: (\pi [i'],\varPhi _1)=T\\ F &{} \text {if } (\forall i\le k:( \pi [i],\varPhi _2)=F)\\ &{} \ \vee \ [\exists i\le k : (\pi [i],\varPhi _2)=T \ \wedge \exists i'< i :(\pi [i'],\varPhi _1)=F] \\ ? &{} \text {otherwise}. \end{array} \right. \end{aligned}$$

3 qPCTL Model Checking

For a qDTMC $\mathcal {M} = (S,\mathbb {P},i_{init},AP,L)$, a state $s\in S$ and a qPCTL state formula $\varPhi$, we want to determine if $(s,\varPhi ) = T$. We note that if $(s, \varPhi ) \ne T$, then $\varPhi$ need not be false in the state s. Unlike for DTMCs, the two statements are not complementary for qDTMCs. Hence we define three satisfaction sets $Sat_{T}(\varPhi )$, $Sat_{F}(\varPhi )$, and $Sat_{?}(\varPhi )$.

Definition 4

A state $s\in Sat_{T}(\varPhi )$ if and only if $(s, \varPhi ) = T$. A state $s\in Sat_{F}(\varPhi )$ if and only if $(s, \varPhi ) = F$. Finally, $s\in Sat_{?}(\varPhi )$ if and only if $(s, \varPhi ) = ?$.

We now describe an algorithm 1MC, to compute these satisfaction sets $Sat_{T}(\varPhi )$ and $Sat_{F}(\varPhi )$ by performing a bottom-up traversal of the syntax tree of $\varPhi$. The remaining satisfaction set $Sat_{?}(\varPhi )$ can be computed as $Sat_{?}(\varPhi )= S \setminus [Sat_{T}(\varPhi ) \cup Sat_{F}(\varPhi )]$. For a given state formula $\varPhi$, these satisfaction sets will partition the state space S. We now discuss the 1MC algorithm in detail. Algorithm 1 lists the pseudocode.

Non-probabilistic Operators: The satisfaction sets for each of the non-probabilistic operators in the qPCTL is based on the logical operations described in Tables 1, 2 and 3. Cases 1 through 4 of the 1MC algorithm compute the satisfaction sets for non-probabilistic operators. It is easy to see that:

Lemma 1

For the non-probabilistic state formulas, the 1MC Algorithm (cases 1 through 4) is correct.

Probabilistic Operators: Construction of the satisfaction sets for probabilistic operators is somewhat more complicated. We need a few definitions first.

Definition 5

True satisfaction probability for a state s is defined as the probability measure of paths starting from s which evaluate the path formula $\psi$ as T. It is denoted by $Pr((s, \psi )=T)$.

Definition 6

False satisfaction probability for a state s is defined as the probability measure of paths starting from s which evaluate the path formula $\psi$ as F, and is denoted by $Pr((s, \psi )=F)$.

Now, the satisfaction sets can be defined as:

$$\begin{aligned} \begin{array}{ccc} Sat_T(Pr_{\bowtie \theta } [\psi ]) &{} = &{}\{s \in S\ |Pr((s, \psi )=T) \bowtie \theta \}\quad \quad \\ Sat_F(Pr_{\bowtie \theta } [\psi ]) &{} = &{}\{s \in S\ |Pr((s, \psi )=F) \bowtie 1-\theta \}\\ Sat_?(Pr_{\bowtie \theta } [\psi ]) &{}= &{} S \setminus [ Sat_T(Pr_{\bowtie \theta } [\psi ]) \cup Sat_F(Pr_{\bowtie \theta } [\psi ])] \end{array} \end{aligned}$$

To construct these sets, we have to calculate $Pr((s,\psi )=T/F/?)$ for path formula $\psi$. There are three path formulas in qPCTL–Next, Until and Bounded Until. We now discuss the algorithms for computing the satisfaction probabilities for these path formulas:

• 1. Next operator – $[X \varPhi ]$: The satisfaction probabilities for next operator are calculated by adding transition probabilities of the state s to the states which satisfy $\varPhi$ as T, F or ?.

  $$\begin{aligned} \begin{array}{ccc} Pr((s, X \varPhi )=T) &{}=&{} \sum \limits _{s' \in Sat_T(\varPhi )} \mathbb {P}(s,s')\\ Pr((s, X \varPhi )=F) &{}=&{} \sum \limits _{s' \in Sat_F(\varPhi )} \mathbb {P}(s,s') \\ Pr((s, X \varPhi )=\ ?) &{}=&{} \sum \limits _{s' \in Sat_?(\varPhi )} \mathbb {P}(s,s') \end{array} \end{aligned}$$

Based on satisfaction probabilities, each state s in S belongs to only one of the three satisfaction sets $Sat_T(Pr_{\bowtie \theta } [X\varPhi ])$, $Sat_F(Pr_{\bowtie \theta } [X\varPhi ])$ or $Sat_?(Pr_{\bowtie \theta } [X\varPhi ])$. If $Pr((s,X\varPhi )=T) \bowtie \theta$ then $s \in Sat_T(Pr_{\bowtie \theta } [X\varPhi ])$. Else if $Pr((s,X \varPhi )=F) \bowtie 1-\theta$ then $s \in Sat_F(Pr_{\bowtie \theta } [X\varPhi ])$. Otherwise, s belongs to the set $Sat_?(Pr_{\bowtie \theta } [X\varPhi ])$.

Example 1

In Fig. 1, a qDTMC $\mathcal {M}_1$ with state space $S=\{s_0,s_1,\ldots ,s_6\}$ with an initial state $s_0$ is given. If we want to verify a qPCTL state formula $\varPhi = Pr_{\ge 0.5}[Xq]$ for $\mathcal {M}_1$, then the satisfaction sets will be: $Sat_T(\varPhi _1)=\{s_1,s_3,s_6\}$, $Sat_F(\varPhi _1)=\{s_4,s_5\}$ and $Sat_?(\varPhi _1)=\{s_0,s_2\}$. Thus for the initial state $s_0$, the qPCTL state formula $\varPhi _1$ will be evaluated to ?.

• 2. Until operator – $[\varPhi _1 U \varPhi _2]$: Identifying B with the set of states where $\varPhi _2$ is true and C as the set of states where $\varPhi _1$ is true, a graph theoretic notion of constrained reachability is useful:

Definition 7

Constrained reachability in a qDTMC $(s,C\ U\ B)$ is defined as an event of reaching the destination set $B\subseteq S$ from the state s such that all the preceding states in the path belong to a constraint set $C \subseteq S$.

Thus the true satisfaction probability $Pr((s,\varPhi _1 U \varPhi _2)=T)$ can be calculated as the probability of constrained reachability being true for paths starting from state s. We can also denote this probability as $Pr((s, C\ U\ B)=T)$. Similarly, the false satisfaction probability $Pr((s,\varPhi _1 U \varPhi _2)=F) = Pr((s, C\ U\ B)=F)$ is the probability of constrained reachability being false.

Notably, it is possible that constrained reachability for a path in a qDTMC is neither true nor false. For such paths, constrained reachability is evaluated to unknown (?). This requires us to calculate all the reachability probabilities separately for each state in $\mathcal {M}$. For each state s, the probability that the constrained reachability is T/F/? is denoted by $x_{s}^{(T/F/?)}$ respectively, and is defined as:

$$ x_{s}^{(T/F/?)} = Pr((s, C\ U\ B)=T/ F/ ?)= Pr((s, \varPhi _1 U \varPhi _2)=T/ F/ ?). $$

To calculate these constrained reachability probabilities, we first partition the state space S into $\{ S_{=0}$, $S_{=1}$, $S_{=?}$ and $S_{find} \}$. We now define each of these partition sets and discuss how to construct these sets later.

$$\begin{aligned} S_{=0} = \{ s \in S\ |\ Pr((s,C\ U\ B)=F)= 1\} \ \ \ \\ B \subseteq S_{=1} \subseteq \{ s \in S | Pr((s, C\ U\ B)=T) = 1 \} \\ S_{=?}= \{ s \in S\ |\ Pr((s,C\ U\ B)=?)= 1\} \end{aligned}$$

The remaining states in S form the set $S_{find}$:

$$\begin{aligned} S_{find} = S \setminus [S_{=0} \cup S_{=1} \cup S_{=?}] \quad \quad \quad \quad \end{aligned}$$

Thus, for states $s \in S_{=1}$, $x_s^{(T)} =1$, $x_s^{(F)} =0$ and $x_s^{(?)} =0$. Similarly for states $s \in S_{=0}$, $x_s^{(F)} =1$, $x_s^{(T)} =0$ and $x_s^{(?)} =0$ and for states $s \in S_{=?}$, $x_s^{(?)} =1$, $x_s^{(T)} =0$ and $x_s^{(F)} =0$.

For a state s in the set $S_{find}$, the constrained reachability probabilities are neither exactly 1 nor 0. We now identify the paths starting from s that eventually reach the set $S_{=1}$ such that all the preceding states are from set $S_{find}$. These paths will evaluate $C\ U\ B$ (or $\varPhi _1 U \varPhi _2$) to T and the probability measure of these paths gives $x_s^{(T)}$. Similarly, $x_s^{(F)}$ is the probability measure of paths from s that reach $S_{=0}$ through the states from $S_{find}$ and hence evaluate $C\ U\ B$ (or $\varPhi _1 U \varPhi _2$) to F.

The satisfaction probabilities for the path formula $[\varPhi _1 U \varPhi _2]$ is then calculated using the following sets of linear equations.

$$\begin{aligned} x^{(T)}_s =\left\{ \begin{array}{ccc} 1 &{} \text {if} &{} s \in S_{=1}\quad \\ 0 &{} \text {if} &{} s \in S_{=0}\quad \\ 0 &{} \text {if} &{} s \in S_{=?}\quad \\ \sum \limits _{t \in S} \mathbb {P}(s,t).x^{(T)}_t \ &{} \text {if} &{} s \in S_{find} \end{array} \right. \end{aligned}$$

(1)

$$\begin{aligned} x^{(F)}_s = \left\{ \begin{array}{ccc} 0 &{} \text {if} &{} s \in S_{=1}\quad \\ 1 &{} \text {if} &{} s \in S_{=0}\quad \\ 0 &{} \text {if} &{} s \in S_{=?}\quad \\ \sum \limits _{t \in S} \mathbb {P}(s,t).x^{(F)}_t \ &{} \text {if} &{} s \in S_{find}\ \ \end{array} \right. \end{aligned}$$

(2)

$$\begin{aligned} Pr((s, \varPhi _1U\varPhi _2)=?) = x^{(?)}_s= 1 - [x^{(T)}_s + x^{(F)}_s] \end{aligned}$$

(3)

We now discuss how to construct $S_{=0}$, $S_{=?}$ and $S_{=1}$. Pseudocode listing for these subroutines is provided in the Algorithms 2, 3 and 4. Then, the set $S_{find}= S\setminus [S_{=0} \cup S_{=1} \cup S_{=?}]$ is computed.

We first compute $S_{=0}$, the set of states that have the false satisfaction probability $Pr((s,\varPhi _1U \varPhi _2)=F)=1$. We identify the states that have false satisfaction probability less than 1. To do this, we first identify the set R of states for which $\varPhi _2$ is either T or ?. Then we do a backward search on the paths leading to R, to find states where $\varPhi _1$ is not F. We add these states to R. When no more states can be added to R, we remove R from the state space to get the set $S_{=0}$.

Example 2

For the qDTMC $\mathcal {M}_1$ in Fig. 1 and a qPCTL state formula $\varPhi = Pr_{\ge 0.5}[\lnot p \ U\ q]$, we first identify the satisfaction sets for the state formulas $\varPhi _1=\lnot p$ and $\varPhi _2=q$ :

$Sat_T(\varPhi _1)=\{s_0,s_3\}$, $Sat_T(\varPhi _2)=\{s_2,s_6\}$,

$Sat_F(\varPhi _1)=\{s_2,s_4,s_6\}$, $Sat_F(\varPhi _2)=\{s_1,s_4\}$

$Sat_?(\varPhi _1)=\{s_1,s_5\}$ and $Sat_?(\varPhi _2)=\{s_0,s_3,s_5\}$.

We can now compute the set $R=\{s_0,s_1,s_2,s_3,s_5,s_6\}$. Thus the partition set $S_{=0}$ will be $\{s_4\}$.

We follow a similar procedure to identify the set of states for which the probability $Pr((s,\varPhi _1 U \varPhi _2)=?)$ will be 1. We start with the states that belong to either $S_{=0}$ or $Sat_T(\varPhi _2)$ and then identify the paths leading to these states. The probability $Pr((s,\varPhi _1 U \varPhi _2)=?)$ for such paths will always be less than 1. We thus exclude these states from the set $S_{=?}$.

Example 3

In continuation of Example 2, the set R is now computed as $R=\{s_4,s_2,s_6\}\cup \{s_0,s_3\}=\{s_0,s_2,s_3,s_4,s_6\}$. Thus the set $S_{=?}$ is computes to $\{s_1,s_5\}$.

The set $S_{=1}$ consists of states that have the true satisfaction probability $Pr((s,\varPhi _1U\varPhi _2)=T)=1$. As before, we first identify the set of states that have true satisfaction probability less than 1, and then remove them from the state space to compute $S_{=1}$.

Example 4

The set R in Algorithm 4 for $\mathcal {M}_1$ is now computed as $R = \{s_4,s_1,s_5\} \cup \{s_0,s_3\} = \{s_0,s_1,s_3,s_4,s_5\}$. Thus the set $S_{=1}$ will be $\{s_2,s_6\}$. Also, the set $S_{find}$ can now be computed as $S_{find}=\{s_0,s_3\}$.

Example 5

Now for $\mathcal {M}_1$ and the qPCTL formula $\varPhi =Pr_{\ge 0.5}[\lnot p\ U \ q]$, we can compute the satisfaction sets using the true and false satisfaction probabilities: $Sat_T(\varPhi )= \{s_2,s_3,s_6\}$, $Sat_F(\varPhi )=\{s_4\}$ and $Sat_?(\varPhi )=\{s_0,s_1,s_5\}$. Thus, for the initial state $s_0$, $\varPhi$ will be evaluated to ?.

• 3. Bounded Until operator – $[\varPhi _1 U^{\le k} \varPhi _2]$: The satisfaction probabilities for $[\varPhi _1 U^{\le k} \varPhi _2]$ can be directly computed by evaluating k transitions of the qDTMC. Depending on the truth values of $\varPhi _1$ and $\varPhi _2$ in a state, the state space S is partitioned into sets $S_{=0}$, $S_{=1}$, $S_{=?}$ and $S_{find}$ in the 1MC algorithm. This partition is illustrated in Fig. 2.

  $$\begin{aligned} \begin{array}{lll} S_{=0} &{} = &{} Sat_F(\varPhi _2) \cap Sat_F(\varPhi _1), \\ S_{=?} &{}=&{} [\ (Sat_?(\varPhi _1) \setminus Sat_T(\varPhi _2))\ \cup \ (Sat_?(\varPhi _2) \setminus Sat_T(\varPhi _1) )\ ],\\ S_{=1} &{}=&{} Sat_T(\varPhi _2), \\ S_{find} &{}=&{} S \setminus [S_{=0} \cup S_{=1}\cup S_{find}] \ = \ Sat_T(\varPhi _1)\setminus Sat_T(\varPhi _2) \end{array} \end{aligned}$$

A state $s \in S_{=1}$ if the truth value of $\varPhi _2$ is T in s. Now irrespective of the truth value of $\varPhi _1$, the path formula $\varPhi _1 U^{\le k} \varPhi _2$ will be evaluated as T for all paths starting from this state s, because $\varPhi _2$ is T in the initial state of the path. Thus, the true (false) satisfaction probability for states in $S_{=1}$ will be 1 (0).

A state belonging to set $S_{=0}$ will have truth values of both $\varPhi _1$ and $\varPhi _2$ as F. All paths starting from such a state $s \in S_{=0}$ will have both $\varPhi _1$ and $\varPhi _2$ false in the initial state itself and will evaluate $\varPhi _1 U^{\le k} \varPhi _2$ to F. Thus, the true (false) satisfaction probabilities for states in $S_{=0}$ will be 0 (1).

A state s belongs to the set $S_{=?}$ if the truth value of at least one of $\varPhi _1$ or $\varPhi _2$ is ? in s and the other is not T. No path starting from such a state $s \in S_{=?}$ can evaluate $\varPhi _1 U^{\le k} \varPhi _2$ to either T or F–the truth or falsehood of $\varPhi _1 U^{\le k} \varPhi _2$ for a path starting in s is cannot be determined if (i) $\varPhi _1$ is ? in s and $\varPhi _2$ is not T or (ii) $\varPhi _1$ is not T and $\varPhi _2$ is ?. For such states, both true and false satisfaction probabilities are 0.

Fig. 2.

A table illustrating possible combinations of truth values for $\varPhi _1$ and $\varPhi _2$ at a state s and corresponding partition set

Now, the remaining states in the state space will have $\varPhi _1$ as T, but $\varPhi _2$ is either F or ?. Since $\varPhi _2$ is not T in starting state s of the path, we need to find the value of $\varPhi _1$ and $\varPhi _2$ in the subsequent states. Thus, these states form the set $S_{find}$.

Example 6

Given a qDTMC $\mathcal {M}_1$ and qPCTL formula $\varPhi =Pr_{\ge 0.5}[\lnot p\ U^{\le 3} \ q]$, we can compute the partition sets of the state space S as: $S_{=0}=\{s_4\}$, $S_{=?}=\{s_1,s_5\}$, $S_{=1}=\{s_2,s_6\}$ and $S_{find}=\{s_0,s_3\}$.

We now calculate the satisfaction probabilities of the path formula $[\varPhi _1 U^{\le k}\ \varPhi _2]$ for the paths starting at a state s using the 1MC algorithm. We denote the true satisfaction probability for state s as $Pr((s, \varPhi _1 U^{\le k}\ \varPhi _2)=T)$ or $x^{(T),k}_s$. We know that the true satisfaction probability for states in $S_{=1}$ is 1. Also for states in $S_{=0}$ and $S_{=?}$, the true satisfaction probability is 0.

To evaluate the path formula $\varPhi _1 U^{\le k} \varPhi _2$, a path with initial state $s \in S_{find}$ is traversed until either a state in one of $S_{=0}$, $S_{=1}$ or $S_{=?}$, or the bound k is reached. If a state $s \in S_{find}$ when bound k is reached, then the probability of $[\varPhi _1 U^{\le k}\ \varPhi _2]$ being evaluated to T is 0. The 1MC algorithm thus computes the true satisfaction probability as follows.

$$\begin{aligned} x^{(T),k}_s = \left\{ \begin{array}{ccc} 1 &{} \text {if} &{} s \in S_{=1}\\ 0 &{} \text {if} &{} s \in S_{=0}\\ 0 &{} \text {if} &{} s \in S_{=?}\\ 0 &{} \text {if} &{} s \in S_{find} \wedge k=0\\ \sum \limits _{t \in S} \mathbb {P}(s,t).x^{(T),k-1}_t &{} \text {if} &{} s \in S_{find} \wedge k>0 \end{array} \right. \end{aligned}$$

(4)

Similarly, we now calculate the false satisfaction probability and denote it as $Pr((s, \varPhi _1 U^{\le k}\ \varPhi _2)=F)$ or $x^{(F),k}_s$. Recall that the path formula $[\varPhi _1 U^{\le k}\ \varPhi _2]$ evaluates to F if either the formula $\varPhi _2$ is F at all states of k-length path, or if at some state $\varPhi _2$ evaluates to T but at some preceding state, $\varPhi _1$ evaluated to F.

We know that the false satisfaction probability for states in $S_{=0}$ is 1 and is 0 for states in $S_{=1}$ and $S_{=?}$. We also know that the states in set $S_{find}$ will have $\varPhi _1$ as T and $\varPhi _2$ is either F or ?. Now no path starting from a state that has $\varPhi _1$ as T and $\varPhi _2$ as ? ($S_{find} \cap Sat_{?}(\varPhi _2)$) will evaluate $\varPhi _1 U^{\le k} \varPhi _2$ as F. Thus, false satisfaction probability for such states will be 0.

We now traverse paths with initial state $s \in S_{find} \cap Sat_{F}(\varPhi _2)$ until either a state in one of $S_{=0}$, $S_{=1}$, $S_{=?}$ or $S_{find} \cap Sat_{?}(\varPhi _2)$, or the bound k is reached. If a state $s \in S_{find} \cap Sat_{F}(\varPhi _2)$ when bound k is reached, then the probability of $[\varPhi _1 U^{\le k}\ \varPhi _2]$ being evaluated to F is 1. This correlates to $\varPhi _2$ evaluating to F at all states in the path, and thus path formula $[\varPhi _1 U^{\le k}\ \varPhi _2]$ being evaluated to F.

$$\begin{aligned} x^{(F),k}_s = \left\{ \begin{array}{ccc} 0 &{} \text {if} &{} s \in S_{=1}\\ 1 &{} \text {if} &{} s \in S_{=0}\\ 0 &{} \text {if} &{} s \in S_{=?}\\ 0 &{} \text {if} &{} s \in (S_{find} \cap Sat_? (\varPhi _2))\\ 1 &{} \text {if} &{} s \in (S_{find} \cap Sat_F (\varPhi _2)) \wedge k=0\\ \sum \limits _{t \in S} \mathbb {P}(s,t).x^{(F),k}_t &{} \text {if} &{} s \in (S_{find} \cap Sat_F (\varPhi _2)) \wedge k>0 \end{array} \right. \end{aligned}$$

(5)

$$\begin{aligned} x^{(?),k}_s = 1 - [x^{(T),k}_s + x^{(F),k}_s] \end{aligned}$$

(6)

Example 7

For the given qDTMC $\mathcal {M}_1$ and qPCTL formula $\varPhi =Pr_{\ge 0.5}[\lnot p\ U^{\le 3} \ q]$, the true satisfaction probability for state $s_0$, $Pr((s_0,\lnot p\ U^{\le 3} \ q)=T)$ is 0.475. Also, the false satisfaction probability $Pr((s_0,\lnot p\ U^{\le 3} \ q)=F)$ is 0. Thus, the initial state $s_0 \in Sat_?(\varPhi )$ and the formula $\varPhi$ is evaluated to ? at state $s_0$.

From the above arguments, we conclude that:

Lemma 2

For the path formulas $X\varPhi$, $\varPhi _1U^{\le k} \varPhi _2$ and $\varPhi _1U\varPhi _2$, Algorithm 1 is correct for the corresponding probabilistic state formulas:

• 1MC($s,Pr_{\bowtie \theta }[X\varPhi ]$)=T (alt., F or ?) iff $(s,Pr_{\bowtie \theta }[X\varPhi ])$=T (resp., F or ?)

• 1MC($s,Pr_{\bowtie \theta }[\varPhi _1 U \varPhi _2]$)=T (alt., F or ?) iff $(s,Pr_{\bowtie \theta }[\varPhi _1 U \varPhi _2])$=T (resp., F or ?)

• 1MC($s,Pr_{\bowtie \theta }[\varPhi _1U^{\le k} \varPhi _2]$)=T (alt., F or ?) iff $(s,Pr_{\bowtie \theta }[\varPhi _1U^{\le k} \varPhi _2])$=T (resp., F or ?)

From lemmas 1 and 2, we have:

Theorem 1

1MC($s,\varPhi$)=T (alt., F or ?) iff $(s, \varPhi )$ =T (resp., F or ?)

Complexity of qPCTL Model Checking: Unlike for the standard PCTL model checking algorithm [4], the 1MC algorithm for qPCTL model checking computes an additional partition set $S_{=?}$ before solving the system of linear equations for the states in the set $S_{find}$. The computation of set $S_{=?}$ is done in $\varTheta (|S|)$ time. Other than that, the asymptotic time complexity is polynomial with respect to the size of the model $\mathcal {M}$ and linear in terms of the size of the query $\varPhi$. Thus, the time complexity of the 1MC qPCTL model checking algorithm is the same as that of the PCTL algorithm and the 2MC algorithm for qPCTL–$\mathcal {O} (poly(size(M)).n_{max}.|\varPhi |)$, where $n_{max}$ is the maximum step bound for bounded until and 1 if the formula does not contain a bounded until. However, in many cases, a drop in the number of runs results in a significant performance improvement over the 2MC algorithm. This is more pronounced for larger models. We validate this with extensive experimentation in the next section.

4 Implementation and Results

We have implemented the 1MC algorithm as a Java tool. The tool takes as an input the qDTMC model and the qPCTL query. The tool supports both qualitative and quantitative qPCTL queries. A qualitative query only checks if the required probability threshold is met, and results in T, F or ?. A quantitative query on the other hand computes the exact probability of the query being T, F and ?.

We will begin by mentioning that the 1MC approach discussed in this paper yields matching results for the case studies reported in [1] and [2]– (i) a model representing an incomplete program code, and (ii) a network model that has incomplete information about its nodes respectively.

We now compare the performance of the proposed 1MC algorithm with the 2MC algorithm in [2] for model checking different qDTMCs. For the sake of fairness, we also implemented the standard PCTL model checker from scratch. The 2MC algorithm calls this bare-bones model checker as a subroutine.

For a fixed size of state space, we randomly generate 50 qDTMCs with different transition probability matrices and labeling functions. We study the variation in time taken to verify models with different structures for different qPCTL queries, and record the minimum and maximum time taken.

We repeat this for different sizes of state spaces starting from qDTMCs with 5 states, and up to 1500 states. Thus the algorithms were compared in terms of the time taken to verify the models of varying sizes.

Figure 3 plots the minimum and maximum times taken by the 1MC and 2MC algorithms to verify the properties $\varPhi _1= Pr_{\ge 0.8}[p_0\ U\ p_1]$, $\varPhi _2=Pr_{\ge 0.7}[\ p_0\ U\ Pr_{\ge 0.6} [X\ p_1]]$ and $\varPhi _3=Pr_{\ge 0.7}[\ p_0\ U\ Pr_{\ge 0.6}[\ p_1 \ U\ p_2]]$ where $p_0$, $p_1$ and $p_2$ are atomic propositions in the incomplete models.

Fig. 3.

Minimum and maximum time taken by the algorithms to verify properties $\varPhi _1$, $\varPhi _2$ and $\varPhi _3$ for models of varying sizes and topology.

It can be seen from the results that the minimum time curve for 1MC algorithm is higher than that for the 2MC algorithm. This is due to the fact that the 2MC algorithm need not compute both its steps in all cases. For instance, if the probability of a property being true meets the required threshold in the first step itself, the model checker need not calculate the probability of a property being false. However, the 1MC algorithm calculates both true as well as false probability in single step, which increases the computation overhead. In many cases, however, both steps of 2MC algorithm are needed; thus making it very expensive for models with large state space. The proposed 1MC algorithm generates results faster for such models and has a lower maximum time curve than that for 2MC algorithm.

5 Conclusion and Future Work

We believe that model checking for incomplete models will be of immense practical use. While it is possible to design algorithms that use existing techniques designed for binary logic, it is useful to have algorithms designed exclusively for three-valued logics. We discussed an algorithm and its application for model checking PCTL queries against incomplete DTMCs that accommodate a three-valued logic.

Future efforts in this direction would be (i) applying these algorithms for interim analysis of incomplete models in practice and (ii) designing similar algorithms and tools for other models and systems of logic.