Abstract
Model checking systems formalized using probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) can be reduced to computing constrained reachability properties. Linear programming methods to compute reachability probabilities for DTMCs and MDPs do not scale to large models. Thus, model checking tools often employ iterative methods to approximate reachability probabilities. These approximations can be far from the actual probabilities, leading to inaccurate model checking results. On the other hand, specialized techniques employed in existing state-of-the-art exact quantitative model checkers, don’t scale as well as their iterative counterparts. In this work, we present a new model checking algorithm that improves the approximate results obtained by scalable iterative techniques to compute exact reachability probabilities. Our techniques are implemented as an extension of the PRISM model checker and are evaluated against other exact quantitative model checking engines.
Similar content being viewed by others
Avoid common mistakes on your manuscript.
1 Introduction
Probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) are often used to describe systems in many application areas such as distributed systems [25, 50], hardware communication protocols [26], reliability engineering in circuits [15, 35, 46, 47], dynamic power management [14, 49], networking [41, 42] and security [20]. Probabilistic transitions in these models are used to capture random faults, the uncertainty of the environment, and explicit randomization used in algorithms. Analyzing properties of these probabilistic models is typically achieved through Probabilistic Computation Tree Logic (PCTL) model checking [51], wherein, a desired property of the model is specified as a PCTL formula, and the validity of such a formula is evaluated against the system in question.
PCTL is a quantitative extension of the temporal logic Computation Tree Logic (CTL) used to describe how a system evolves over time. For example, a PCTL formula \(\psi \) can be used to specify the property that almost surely no execution of a probabilistic program leads to a state with a deadlock. Given \(\bowtie \in \{\le , < , \ge , >\}\), the formula \({\mathcal {P}}_{\bowtie p} [\psi ]\) expresses the property that the measure of computation paths satisfying \(\psi \) is \({\bowtie } p\). For a DTMC or MDP \({\mathcal {M}}\) and a PCTL formula \(\phi \), the PCTL model checking procedure recursively computes the set of states of \({\mathcal {M}}\) that satisfy subformulas of \(\phi \). Each recursive step, in turn, reduces to constrained quantitative reachability, wherein, given a set of good states G and a set of target states T, the goal is to compute the measure of the paths that reach T while remaining in G. If the model is decorated with costs or rewards, one may also be interested in computing the expected cost/reward of reaching T. It is well known that the constrained quantitative reachability problem for DTMCs and MDPs can be solved in polynomial time by a reduction to linear programming [10, 51].
Despite low asymptotic complexity, linear programming, unfortunately, doesn’t scale to large models and is rarely used to solve the constrained quantitative reachability problem in practice. Instead, probabilistic model checkers [22, 23, 32, 38, 39, 44], typically compute approximations to the exact reachability probabilities through an iterative process. The most prevalent iterative technique is value iteration, where exact reachability probabilities may only be approached in the limit. For completion in a finite number of steps, it is common practice for model checking tools to terminate value iteration based on various heuristics, for example, when the difference between the computed reachability probabilities of successive iterations is “small”. This approximation step may lead to unsound results [11, 31, 54], particularly in systems where high magnitude changes in value iteration are preceded by periods of stability that cause iteration to terminate prematurely.
Another iterative technique for computing constrained quantitative reachability is interval iteration [11, 17, 31, 53]. Aimed at addressing the shortcomings of value iteration, interval iteration utilizes two simultaneous value iteration procedures converging to the exact probability values from above and below. While, this allows one to bound the error present in the approximation, the exact solution cannot be obtained from such an interval bound. Further, state-of-the-art model checkers typically implement these iterative procedures using floating-point numbers and finite-precision arithmetic. As a result, both iterative techniques are susceptible to overflows in floating-point calculations. The inherent imprecision in the approximate answers, combined with the errors introduced from finite precision arithmetic can be further compounded by the presence of nested probability operators in PCTL formulas when the sets of good states G and target states T are not correctly computed in the recursive step (see Example 3 in Sect. 3).
1.1 Contributions
In this article, we present a new algorithm and its implementation that sharpens approximate solutions computed by fast iterative techniques, to obtain the exact constrained reachability probabilities. The starting point of our approach is the observation that when the transition probabilities in the model are rational numbers, an exact solution is also a rational number of polynomially many bits. The second ingredient in our technique is an algorithm due to Kwek and Mehlhorn [40], which, given a “close enough” approximation to a rational number, finds the rational number efficiently. The rough outline of our algorithm is as follows. We use an iterative technique (value iteration or interval iteration) to compute an approximate solution and then apply the Kwek–Mehlhorn algorithm to find a close candidate rational solution. Since the approximate solution that we start with is of unknown quality, the candidate rational solution obtained may not be the exact answer. Therefore, we check if the candidate satisfies certain necessary and sufficient conditions that characterize the actual solution. This allows one to confirm the correctness of the candidate rational solution. If it is not correct, the process is repeated, starting with an approximate solution of improved precision. Precise details of the algorithm are given in Sect. 5.
We have implemented this approach as an extension of the PRISM model checker, called RationalSearch. Our tool computes exact constrained reachability probabilities and exact expected rewards when model checking DTMCs against PCTL specifications. Our implementation also computes min reachability probabilities and max expected rewards when model checking MDPs against PCTL specifications. For max reachability probabilities, we currently support only the Explicit engine of PRISM. Evaluation of our implementation against a broad set of examples from the PRISM benchmark suite [2] and case studies [3] shows that our technique can be applied to a wide array of examples. In many cases, our tool is orders of magnitude faster than the exact model checking engines implemented in state-of-the-art tools like PRISM [44] and STORM [22].
1.2 Related work
The work closest in spirit to ours is [30], which presents an approach to obtain exact solutions for reachability properties for MDPs and discounted MDPs. The underlying idea in [30] is to interpret the scheduler obtained for an approximate solution, as a basis for the linear program corresponding to the verification question. By examining the optimality of the solution associated with this basis, the exact solution can be obtained by improving the scheduler using the Simplex algorithm. This is significantly different from our approach. In particular, for the case of DTMCs (where there is no scheduler), the approach of [30] reduces to solving a linear program, which is known to be not scalable. Since the implementation from [30] is not available, we could not experimentally compare it with our approach.
Several existing tools [22, 44] implement algorithms for exact quantitative model checking. Essentially these tools work by creating a model representation using rational numbers and performing a state elimination computation similar to Gauss elimination. Much of the infrastructure of this computation can be derived from parametric model checking techniques [21, 23, 33, 34] that analyze systems in which portions of the model are left unspecified. These computations are intrinsically more complicated than those performed by approximation engines. Our techniques avoid these expensive computations while still producing exact solutions for a large class of examples.
1.3 History and organization
An extended abstract of this article appeared in [13]. The main difference from [13] is that in [13], we had claimed that in order to check whether a candidate solution vector represents the actual exact solution of max/min reachability probabilities or that of max/min expected costs for MDPs, it suffices to only check that the candidate vector is a solution to a linear program. This happens to be incorrect for the case of max reachability probabilities and min expected costs (see Sect. 4), and additional checks are required to claim that the candidate solution vector is indeed correct (Lemmas 1, 3). We have modified our algorithm to reflect this. We have also updated our prototype implementation for computing max reachability probabilities and evaluated the new version on our benchmarks. We do not currently support the computation of min expected costs. We have also computed the asymptotic complexity of the algorithm (see Theorem 2). Further, the version of RationalSearch evaluated in this work extends our original prototype by integrating with interval iteration and including several performance enhancements. Additionally, we describe the full details of our implementation and provide a more comprehensive evaluation of the tool.
The paper is organized as follows. Section 2 discusses preliminary notations, definitions and algorithms concerning PCTL model checking of DTMCs and MDPs. Section 3 describes iterative model checking techniques and their shortcomings. In Sect. 4, we discuss fixpoint characterizations for solutions to PCTL model checking questions of MDPs. In Sect. 5 we present our exact model checking algorithm. Sects. 6 and 7 describe the implementation and evaluation of our techniques and we conclude with Sect. 8.
2 Preliminaries
A common technique in the analysis of systems is to model them as state transitions systems where states describe information about the system at a point in time and transitions describe how the system evolves from one state to another. When this evolution is governed by random phenomena, such state transition systems can then be enriched to capture probabilistic behavior. The resulting model is known as a DTMC, in which every state is mapped to a distribution over the successor states. MDPs generalize DTMCs, in that, the distribution over the successor states is non-deterministically chosen. Our presentation of DTMCs and MDPs follows [52]. We begin by formalizing DTMCs and introducing the logic Probabilistic computation tree logic (PCTL), which is used to specify properties of DTMCs. We then discuss the model checking algorithm for DTMCs. We next formally describe MDPs and then present PCTL semantics and model checking for MDPs. Unless otherwise stated, all the transition probabilities in the paper are assumed to be rational numbers. The set of rational numbers shall be denoted as \({\mathbb {Q}}\) and the set of non-negative rational numbers as \({\mathbb {Q}}^{\ge 0}\).
2.1 Discrete time Markov chains (DTMCs)
2.1.1 Syntax and semantics
A DTMC is a tuple \({\mathcal {M}}= (Z, {\varDelta }, {\mathbf {C}}, L)\) where \(Z\) is a finite set of states, \({\varDelta }: Z\rightarrow {\mathsf {Dist}}(Z)\) is the probabilistic transition function that maps every state to a probability distribution over \(Z\), \({\mathbf {C}}: Z\times Z\rightarrow {\mathbb {Q}}^{\ge 0}\) is a cost (or reward) structure and \(L: Z\rightarrow 2^{{\mathsf {AP}}}\) is a labeling function that maps states to subsets of \({\mathsf {AP}}\), the set of atomic propositions. For each \(z\in Z\), \({\varDelta }(z) : Z\rightarrow {\mathbb {Q}} \cap [0,1]\) defines a discrete probability distribution over \(Z\), that is, \({\varDelta }(z)(z') \ge 0\) for all \(z' \in Z\), and \(\sum _{z' \in Z} {\varDelta }(z)(z') = 1\). We will henceforth denote \({\varDelta }(z)(z')\) by \({\varDelta }(z, z')\).
Intuitively, a DTMC \({\mathcal {M}}\) evolves as follows. If \({\mathcal {M}}\) is in state \(z\), it transitions to state \(z'\) with probability \({\varDelta }(z,z')\). Formally, a finite (resp. infinite) path \(\rho \) of \({\mathcal {M}}\) is a finite (resp. infinite) sequence of states \(z_0 \rightarrow z_1 \rightarrow \cdots \) such that \({\varDelta }(z_i,z_{i+1}) > 0\). We write \(\rho (i)\) to denote the ith state \(z_i\) in \(\rho \). For a DTMC \({\mathcal {M}}\), the set of all infinite paths starting from state \(z\) will be denoted by \({\mathsf {Paths}}_{z}({\mathcal {M}})\). For a finite path \(\rho _{\text {fin}} = z_0 \rightarrow \cdots \rightarrow z_m\) starting at state \(z_0\), we associate a measure \({\mathsf {prob}}_{z_0}(\rho _{\text {fin}})= \prod _{i=0}^{m-1} {\varDelta }(z_i, z_{i+1})\). The cylinder set of \(\rho _\text {fin}\) is \({\mathsf {Cyl}}(\rho _{\text {fin}}) = \{ \rho \in {\mathsf {Paths}}_{z_0}({\mathcal {M}}) |\rho _\text {fin}\text { is a prefix of } \rho \}\) and its associated measure is \( {\mathsf {prob}}_{z_0}({\mathsf {Cyl}}(\rho _\text {fin})) = {\mathsf {prob}}_{z_0}(\rho _\text {fin})\). This measure \({\mathsf {prob}}_{z_0}\) can be extended to a unique probability measure over the smallest \(\sigma \)-algebra on \({\mathsf {Paths}}_{z_0}({\mathcal {M}})\) that contain all cylinder sets; the resulting probability measure will also be denoted by \({\mathsf {prob}}_{z_0}\).
2.1.2 Reachability probability and expected cost
Let \(z\in Z\) and \(F \subseteq Z\). The probability of reaching F from the state \(z\) is defined to be the measure \({\mathsf {prob}}_z(Reach)\) where Reach is the set of all infinite paths \(\rho \) such that \(\rho (0) = z\) and \(\rho (i) \in F\) for some \(i\ge 0.\) For defining expected cost, we first define the function \({\mathsf {cost}}_z(F):{\mathsf {Paths}}_z \rightarrow {\mathbb {Q}}^{\ge 0}\) such that for any \(\rho \in {\mathsf {Paths}}_z({\mathcal {M}})\), \({\mathsf {cost}}_z(F)(\rho ) = \sum _{i=0}^{m-1} {\mathbf {C}}(z_i, z_{i+1})\) if \(z_0 \rightarrow \cdots \rightarrow z_m\) is the shortest prefix of \(\rho \) such that \(z_m \in F\) and \({\mathsf {cost}}_z(F)(\rho ) = \infty \) if no such prefix exists. Let \({\mathbb {E}}_{z}\) be the usual expectation on \({\mathsf {Paths}}_{z}({\mathcal {M}})\) with respect to the measure \({\mathsf {prob}}_{z}\). Then \({\mathbb {E}}_{z}[{\mathsf {cost}}_z(F)]\) is defined to be the expected cost of reaching F. Observe that, following [52], the expected cost \({\mathbb {E}}_{z}[{\mathsf {cost}}_z(F)]\) is finite iff the set F can be reached from \(z\) with probability 1.
Example 1
Consider an embedded control system [43] comprised of an input processor, a main processor, an output processor and a bus. In each cycle of the system, the input processor collects data from a set of n sensors \(S_1, S_2, \ldots , S_n\). The main processor polls the input processor and passes instructions to the output processor controlling a set of m actuators \(A_1, A_2, \ldots A_m\). Communication between processors occurs over the bus. The system is designed to tolerate failures in a limited number of components. If the input processor reports that the number of sensor failures exceeds some threshold MAX_FAILURES, then the main processor shuts the system down. Otherwise, it activates the actuators, which again, are prone to failure. When the probabilities with which each of these components fail are known, one can model the system’s reliability using a DTMC. In Fig. 1, we give a DTMC that models a single cycle of such a system with \(n=2\) sensors and \(m=1\) actuator. For simplicity, we assume that each sensor fails with probability \({\hbox {E}}_s\) and each actuator fails with probability \({\hbox {E}}_a\). States of the model are labeled with \(e^s_1,\ldots , e^s_n \in \{0,1\}\) and \(e^a_1,\ldots , e^a_m \in \{0,1\}\), where \(e^s_i = 1\) denotes the failure of sensor \(S_i\) and \(e^a_i = 1\) denotes the failure of actuator \(A_i\). In Fig. 1, we omit labels if they are not relevant in a particular state.
Markov chain for a simple embedded control system with two sensors and one actuator tolerating a single sensor fault
2.2 Probabilistic computation tree logic (PCTL)
Properties of DTMCs be expressed in the logic PCTL, which extends the temporal logic CTL with the ability to reason quantitatively. We start by describing the syntax and semantics of PCTL.
2.2.1 Syntax
Analogous to CTL, PCTL has state formulas that model properties of states and path formulas that model properties of paths.
Definition 1
Let \(a \in {\mathsf {AP}}\) be an atomic proposition, \(\bowtie \in \{\le , < , \ge , >\}\), \(p \in [0,1]\), \(c \in {\mathbb {Q}}^{\ge 0}\) and \(k \in {\mathbb {N}}\). The syntax of PCTL is
Here \(\phi \) is a state formula and \(\psi \) a path formula.
2.2.2 Semantics
The state formulas are interpreted over states and path formulas over infinite paths.
Definition 2
Let \({\mathcal {M}}= (Z, {\varDelta }, {\mathbf {C}}, L)\) be a DTMC, \(\phi , \phi _1, \phi _2\) be state formulas and \(\psi \) be a path formula. The satisfaction relation \(\models \) for PCTL state formulas and for PCTL path formulas is defined by mutual induction:
where \(p_{z}(\psi ) = {\mathsf {prob}}_z(\{ \rho \in {\mathsf {Paths}}_{z}({\mathcal {M}}) |{\mathcal {M}}, \rho \models \psi \})\), \(e_z(\phi ) = {\mathbb {E}}_z[{\mathsf {cost}}_z(Z_{\phi })]\) with \(Z_{\phi } = \{ z' \in Z|{\mathcal {M}}, z' \models \phi \}.\)
Example 2
Consider the DTMC modeling an embedded control system from Example 1. One can describe many important properties of this model using PCTL as follows (\(\bowtie , \bowtie ' \in \{ \le , \ge , <, > \}\) and \(p \in [0,1]\))
-
1.
The probability of success is \({{\bowtie }p}\):
$$\begin{aligned} {\mathcal {P}}_{\bowtie p} \; [\; {\mathsf {true}} \; {\mathcal {U}}\; ``\text {Sucess}'' \; ] \end{aligned}$$ -
2.
The probability of reaching the set of states where there are no sensor failures is \({{\bowtie }p}\):
$$\begin{aligned} {\mathcal {P}}_{\bowtie p} \; [\; {\mathsf {true}} \; {\mathcal {U}}\; (e_1^s + \cdots + e_n^s = 0 ) \; ] \end{aligned}$$ -
3.
Let G be the set of states from which the probability of reaching a state where sensor \(S_1\) fails is \({\bowtie }\frac{1}{2}\). Let T be the set of states from which the probability of reaching a state in which actuator \(A_1\) fails is 0. The probability of remaining in some state from the set G until reaching a state in T is \({\bowtie '}p\):
$$\begin{aligned} {\mathcal {P}}_{{\bowtie '}p} \;[ \; {\mathcal {P}}_{\bowtie \frac{1}{2}} [{\mathsf {true}} \; {\mathcal {U}}\; (e^s_1{=}1) ] \;{\mathcal {U}}\; {\mathcal {P}}_{\le 0} [{\mathsf {true}} \; {\mathcal {U}}\; (e^a_1{=}1) ] \; ] \end{aligned}$$
2.3 PCTL model checking
The PCTL model checking question asks, given a state \(z_0\) of a DTMC \({\mathcal {M}}\) and a PCTL formula \(\phi \), determine whether \({\mathcal {M}}, z_0 \models \phi .\) Similar to the model checking algorithm for CTL, the PCTL model checking algorithm recursively computes the set of states satisfying a state sub-formula (see [10, 52] for the complete details). We consider the special case when the formula \(\phi \) is of the form \({\mathcal {P}}_{\bowtie p} [\phi _1 \; {\mathcal {U}}\; \phi _2].\)
Let \(\phi , \phi '\) be state formulas. To check whether \({\mathcal {M}}, z_0\models {\mathcal {P}}_{\bowtie p} [\phi \; {\mathcal {U}}\; \phi '],\) one recursively computes the set of states \(Z_\phi \) and \(Z_{\phi '}\) satisfying the state formulas \(\phi \) and \(\phi '\), respectively. These can then be used to derive, for every \(z{\in }Z\), the quantity \(p_z(\phi \; {\mathcal {U}}\; \phi ')\) which represents the probability of reaching the set \( Z_{\phi '}\) while remaining in the set \(Z_{\phi }\), starting from the state \(z\). Let \(\lambda z.\; p_z(\phi \; {\mathcal {U}}\; \phi ')\) denote the state-indexed vector (or the function) that maps \(z\in Z\) to \(p_z(\phi \; {\mathcal {U}}\; \phi ').\) The state-indexed vector \(\lambda z.\, p_z(\phi \; {\mathcal {U}}\; \phi ')\) can be computed as the unique solution to following linear program [10, 52]:
In the equation above, \({\mathsf {Prob}}_{0} [\phi \; {\mathcal {U}}\; \phi '] \) and \({\mathsf {Prob}}_{1} [\phi \; {\mathcal {U}}\; \phi '] \) are the set of states of \({\mathcal {M}}\) that satisfy \(\phi \; {\mathcal {U}}\phi '\) with probability 0 and 1, respectively. These sets can be determined via a pre-computation step that analyzes the underlying graph structure of the DTMC. The value of \(y_z\) in the solution is exactly the value \(p_z(\phi \; {\mathcal {U}}\; \phi ').\) To verify if \({\mathcal {M}},z_0\models {\mathcal {P}}_{\bowtie p} [\phi \; {\mathcal {U}}\; \phi ']\), one computes \(\lambda z.\; p_z(\phi \; {\mathcal {U}}\; \phi ')\) and compares \(p_{z_0}(z\; {\mathcal {U}}\; z') \bowtie p.\) The model checking algorithm for \(\lnot \phi \), \(\phi \wedge \phi '\), and \({\mathcal {P}}_{\bowtie p} [{\mathcal {X}}\phi ]\) are as expected.
To check whether \({\mathcal {E}}_{\bowtie c} [\phi ],\) one recursively computes \(Z_\phi \) satisfying the state formula \(\phi \). The expected costs \(\{ e_z(\phi )|z\in Z \} \) can then be computed as the unique solution to the following linear program [52] (with the convention that \(0\cdot \infty =0\)):
In the equation above, \({\mathsf {Cost}}_\infty [\phi ]\) is the set of states for which the expected cost is \(\infty .\) The set \({\mathsf {Cost}}_\infty \) is exactly the set of states that satisfy \(\phi \) with probability \(<1\), and can be determined via a pre-computation step that analyzes the underlying graph structure of the DTMC.
2.4 Markov decision processes (MDPs) and PCTL
2.4.1 Syntax
An MDP is a tuple \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) where \(Z\) is a finite set of states, \({\mathsf {Act}}\) is a finite set of actions, the partial function \({\varDelta }: Z\times {\mathsf {Act}}\hookrightarrow {\mathsf {Dist}}(Z)\), called probabilistic transition function, maps pairs of states and actions to probability distributions over \(Z\), \({\mathbf {C}}: Z\times {\mathsf {Act}} \rightarrow {\mathbb {Q}}^{\ge 0}\) is a cost (or reward) structure and \(L: Z\rightarrow 2^{{\mathsf {AP}}}\) is a labeling function. The set \({\mathsf {enabled}}(z) = \{\alpha \in {\mathsf {Act}} |{\varDelta }(z, \alpha )\text { is defined}\},\) describing the actions enabled from a state z, is assumed to be non-empty for every \(z \in Z\). An MDP, therefore, differs from a DTMC, in that, at each state \(z\), there is a choice among several possible distributions. The choice of which distribution to trigger is resolved by a scheduler (or an attacker). Informally, an MDP \({\mathcal {M}}\) evolves as follows. It starts from some state \(z_0 \in Z\). After i execution steps, if \({\mathcal {M}}\) is in state \(z\), the scheduler chooses an action \(\alpha \in {\mathsf {enabled}}(z)\), which then defines a unique probability distribution \(\mu \) given by \({\varDelta }(z, \alpha )\). The process then moves to state \(z'\) in step \((i+1)\) with probability \({\varDelta }(z, \alpha )(z')\). We will write \({\varDelta }(z, \alpha , z')\) to denote \({\varDelta }(z, \alpha )(z')\) when \(\alpha \in {\mathsf {enabled}}(z)\).
2.4.2 Reachability probability and expected cost
Formally, a path \(\rho \) of an MDP \({\mathcal {M}}\) is a sequence \(z_0{\xrightarrow {\alpha _1}} z_1 {\xrightarrow {\alpha _2}} \cdots \) such that for each \(i \ge 0\), we have \({\alpha _{i+1} \in {\mathsf {enabled}}(z_i)}\) and \({\varDelta }(z_i, \alpha _{i+1}, z_{i+1})>0\). As discussed above, the choice of which action to trigger in a given state is resolved by a scheduler, which is a function \({\mathfrak {S}}\) from finite paths to actionsFootnote 1. A path \(z_0{\xrightarrow {\alpha _1}} z_1 {\xrightarrow {\alpha _2}} \cdots \) is a \({\mathfrak {S}}\)-path if \({\mathfrak {S}}(z_0z_1\ldots z_i) = \alpha _{i+1}\) for all \(i\ge 0\). We will write \({\mathsf {Paths}}_z({\mathcal {M}})\) for the set of infinite paths starting from \(z\) and \({\mathsf {Paths}}^{\mathfrak {S}}_z({\mathcal {M}})\) for the set of infinite \({\mathfrak {S}}\)-paths starting from \(z\). The set of all schedulers will be denoted by \({\mathcal {S}}\). A scheduler \({\mathfrak {S}}\in {\mathcal {S}}\) for MDP \({\mathcal {M}}\) induces a (potentially infinite) DTMC \({\mathcal {M}}^{\mathfrak {S}}\) where the states of \({\mathcal {M}}^{\mathfrak {S}}\), denoted \(Z^{{\mathfrak {S}}}\), are the set of finite paths of \({\mathcal {M}}\) and the transition function \({\varDelta }^{{\mathfrak {S}}}\) is as follows. For any two finite paths \(\rho , \rho ' \in Z^{{\mathfrak {S}}}\) where \(\rho = z_0 \xrightarrow {\alpha _1} \cdots \xrightarrow {\alpha _m} z_m\) let
This allows one to use probability measure over DTMCs to define a probability measure \({\mathsf {prob}}^{{\mathfrak {S}}}_{z}\) over the set of paths \({\mathsf {Paths}}^{{\mathfrak {S}}}_{z}({\mathcal {M}})\). One can also define the expected cost of reaching a target set of states F with respect to a scheduler \({\mathfrak {S}}\), denoted \({\mathbb {E}}^{\mathfrak {S}}_{z}[{\mathsf {cost}}_z(F)]\), in a fashion similar to the DTMC case. Interested readers should refer to standard texts such as [10, 52] for more details.
2.4.3 Probabilistic computation tree logic (PCTL)
Like DTMCs, properties of MDPs can be expressed in the logic PCTL. The semantics of PCTL formulae stay the same, except for the semantics of \({\mathcal {P}}_{\bowtie p}[\psi ]\) and \({\mathcal {E}}_{\bowtie c}[\phi ]\), which now require a quantification over all schedulers.
Definition 3
Let \({\mathcal {M}}\) be an MDP, \(\phi \) be a state formula, and \(\psi \) be a path formula. The satisfaction relation \(\models \) for PCTL state formulae is defined identically to Definition 2, except for the following cases.
where given an adversary \({\mathfrak {S}}\in {\mathcal {S}}\), \(p^{\mathfrak {S}}_{z}(\psi ) = {\mathsf {prob}}^{\mathfrak {S}}_z(\{ \rho \in {\mathsf {Paths}}_{z}^{\mathfrak {S}}({\mathcal {M}}) |{\mathcal {M}}, \rho \models \psi \})\) and \(e^{\mathfrak {S}}_z(\phi ) = {\mathbb {E}}^{\mathfrak {S}}_z[{\mathsf {cost}}_z(Z_{\phi })]\) with \(Z_{\phi } = \{ z' \in Z|{\mathcal {M}}, z' \models \phi \}.\)
2.5 PCTL model checking for MDPs
Similar to the PCTL model checking algorithm for DTMCs, the PCTL model checking algorithm for MDPs recursively computes the set of states satisfying a state sub-formula (see [10, 52] for the complete details). We illustrate the differences when we model check the probability and expected cost operators.
\({\mathcal {P}}_{\bowtie p} [\phi \; {\mathcal {U}}\; \phi ']\) operator. For checking whether a state \(z_0\) satisfies \({\mathcal {P}}_{\bowtie p} [\phi \; {\mathcal {U}}\; \phi '],\) we recursively compute the sets of states \(Z_\phi \) and \(Z_{\phi '}\) as in the case of DTMCs. Given a state \(z\), let \( p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ') = \max \limits _{{\mathfrak {S}}\in {\mathcal {S}}} \; p^{\mathfrak {S}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) and \(p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ') = \min \limits _{{\mathfrak {S}}\in {\mathcal {S}}} \; p^{\mathfrak {S}}_{z}(\phi \; {\mathcal {U}}\; \phi ').\) Thus, \(p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) (resp. \(p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\)) is the maximum (resp. minimum) probability of satisfying \(\phi \; {\mathcal {U}}\; \phi '.\) We note that both \( p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) and \( p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) exist [9, 10, 14, 16, 52]). Thus, in order to check whether \({\mathcal {M}}, z_0 \models {\mathcal {P}}_{\bowtie p} [\phi \; {\mathcal {U}}\; \phi ']\), it suffices to compute \( p^{\mathsf {max}}_{z_0}(\phi \; {\mathcal {U}}\; \phi ')\) when \(\bowtie \in \{ <,\le \}\) and to compute \( p^{\mathsf {min}}_{z_0}(\phi \; {\mathcal {U}}\; \phi ')\) if \(\bowtie \in \{ >,\ge \}.\) We explain below how these are computed.
In order to compute \( p^{\mathsf {max}}_{z_0}(\phi \; {\mathcal {U}}\; \phi ')\), we compute the function \(\lambda z.\, p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) that maps each \(z\in Z\) to \(p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ').\) For each \(z\in Z\), pick a variable \(y_z.\) Consider the following linear optimization problem:
where \({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi ']\) (\({\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) respectively) is the set of states \(z\) such that \(p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) is 0 (1 respectively). The sets \({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \) and \({\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) can be computed using graph-theoretic algorithms. Now, the vector \( \lambda z.\, p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) is the unique solution set for this linear optimization problem, ie, objective is minimized and constraints satisfied if and only if we replace \(y_z\) by \(p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\).
Computation of \(\lambda z.\;p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ') \), the state-indexed vector that maps \(z\in Z\) to \(p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ') \), is along similar lines; the objective changes to maximization, \( {\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \) and \( {\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) are replaced by \( {\mathsf {Prob}}^{{\mathsf {min}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \) and \( {\mathsf {Prob}}^{{\mathsf {min}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) respectively, and the direction the last inequality is reversed. Here \( {\mathsf {Prob}}^{{\mathsf {min}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \) (\({\mathsf {Prob}}^{{\mathsf {min}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) respectively) is the set of states z for which \(p^{\mathsf {min}}_{z}\) is 0 (1 respectively), and can be computed using graph-theoretic algorithms.
\({\mathcal {E}}_{\bowtie p} [\phi ]\) operator. For checking whether a state \(z_0\) satisfies \({\mathcal {E}}_{\bowtie p} [\phi ],\) we recursively compute the set of states \(Z_\phi \) as in the case of DTMCs. Given a state \(z\), let \( e^{\mathsf {max}}_{z}(\phi ) = \max \limits _{{\mathfrak {S}}\in {\mathcal {S}}} \; e^{\mathfrak {S}}_{z}(\phi ) \) and \( e^{\mathsf {min}}_{z}(\phi ) = \min \limits _{{\mathfrak {S}}\in {\mathcal {S}}} \; e^{\mathfrak {S}}_{z}(\phi ).\) Thus, \(e^{\mathsf {max}}_{z}(\phi )\) (\(e^{\mathsf {min}}_{z}(\phi )\) respectively) is the maximum (minimum respectively) expected cost of reaching the set \(Z_\phi .\) Again, we note that both \( e^{\mathsf {max}}_{z}(\phi )\) and \( e^{\mathsf {min}}_{z}(\phi )\) exist [10, 14, 52]). Thus, it suffices to compute \(e^{\mathsf {max}}_{z_0}(\phi )\) when \(\bowtie \in \{ <,\le \}\) and to compute \( e^{\mathsf {min}}_{z_0}(\phi )\) if \(\bowtie \in \{ >,\ge \}.\)
In order to compute \( e^{\mathsf {max}}_{z_0}(\phi )\), we compute the state-indexed vector \(\lambda z.\, e^{\mathsf {max}}_{z}(\phi ).\) For each \(z\in Z\), pick a variable \(y_z.\) Consider the following linear optimization problem (with the convention that \(0\cdot \infty =0\)):
where \({\mathsf {Cost}}_\infty ^{\mathsf {max}}\) is the set of states \(z\) such that \(e^{\mathsf {max}}_{z}(\phi )=\infty .\) Observe that \(z\in {\mathsf {Cost}}_\infty ^{\mathsf {max}}\) if and only if there is a scheduler \({\mathfrak {S}}\) such that \(p^{\mathfrak {S}}_z(\phi ) <1. \) This allows computation of the set \({\mathsf {Cost}}_\infty ^{\mathsf {max}}\) using graph-theoretic methods. Now, the vector \( \lambda z.\, e^{\mathsf {max}}_{z}(\phi )\) is the unique solution for this linear optimization problem, i.e., the objective is minimized and constraints satisfied if and only if we replace \(y_z\) by \(e^{\mathsf {max}}_{z}(\phi )\). Computation of \( \lambda z.\, e^{\mathsf {min}}_{z}(\phi )\) is along similar lines; the objective changes to maximization, \({\mathsf {Cost}}^{\mathsf {max}}_\infty [\phi ]\) is replaced by \( {\mathsf {Cost}}^{\mathsf {min}}_\infty [\phi ]\), and the direction the last inequality is reversed. Here \( {\mathsf {Cost}}^{\mathsf {min}}_\infty [\phi ]\) is the set of states z such that \(e^{\mathsf {min}}_{z}\) is \(\infty \). Observe that \(z\in {\mathsf {Cost}}^{\mathsf {min}}_\infty [\phi ]\) if and only if \(p^{\mathfrak {S}}_z(\phi ) <1\), for all schedulers \({\mathfrak {S}}.\) The set \({\mathsf {Cost}}^{\mathsf {min}}_\infty [\phi ]\) can also be computed graph-theoretically.
3 Approximate model checking
As discussed before, solving quantitative properties of DTMCs and MDPs by a reduction to linear programming does not scale well enough to make it a viable solution technique in practice. As a result, techniques for approximating solutions to the model checking problem using floating-point arithmetic have been widely adopted. In this section, we describe two such techniques, value iteration and interval iteration, and demonstrate how each approach can produce incorrect solutions.
3.1 Iterative techniques
The linear program described in Eq. (1) for DTMCs can equivalently be expressed in the below, for some appropriate matrix A and vector b.
This allows for an alternate approach to solving the linear program from Eq. (1) known as value iteration. In the case of DTMCs, the unique solution to Eq. (1) can be computed iteratively as the the limit of the following sequence.
For the case of MDPs, the unique solution that minimizes the objective function of the linear program in Eq. (3) and used to compute maximum probabilities of satisfying \([\phi \; {\mathcal {U}}\; \phi ']\) can be obtained as the limit of the iterative sequence \(\{ x_i \}_{i\ge 0}\):
For the solution to the linear program that is used to compute minimum probabilities, the iterative sequence is similar except that \({\mathsf {max}}\) is replaced by \({\mathsf {min}}.\) The iterative sequences for computing expected costs can be similarly defined with one notable variation. For computing min expected costs, the MDPs have to be transformed to get rid of cost 0 cycles. We refer the reader to [9, 28, 52] for details.
In many cases, the sequence does not converge in a finite number of steps, and therefore model checkers terminate the sequence when successive vectors \(v_{k}\) and \(v_{k+1}\) become “close enough”. The choice of stopping criterion is based mainly on heuristics. The PRISM model checker, for example, implements two criteria (i) absolute convergence, and (ii) relative convergence. Under the absolute criterion, value iteration terminates if the norm \(\left\Vert v_{k+1} - v_{k}\right\Vert {<} \epsilon \) for some \(\epsilon > 0\). Under the relative criterion, termination occurs when \(\frac{\left\Vert v_{k+1} - v_k\right\Vert }{\left\Vert v_k\right\Vert } < \epsilon \). In spite of the fact that iterative techniques only approximate solutions, value iteration remains the popular choice for widely used tools that analyze PCTL properties as it vastly outperforms linear programming techniques, despite their theoretically better asymptotic complexity.
As originally observed in [27], value iteration provides no guarantees about the quality of the solution, regardless of the stopping criterion used. To help rectify this problem, Haddad et. al. [31] and Brázdil et. al. [17] concurrently introduced interval iteration for computing min/max reachability probabilities in DTMCs and MDPs. In this approach, one simultaneously computes two sequences of vectors, one converging to the solution from below and one converging to the exact solution from above. In this setting, the stopping criterion becomes straightforward; terminate when the distance between the two vectors is within some \(\epsilon \) threshold. Assuming the absence of floating-point errors, this effectively gives a small \(\epsilon \)-neighborhood that contains the actual solution. In order to achieve convergence, interval iteration requires a pre-processing step that transforms the underlying graph of the model. The interval iteration technique was extended to expected costs in [11].
Both iterative techniques described above can be further enhanced by performing arithmetic operations using Multi-terminal binary decision diagrams (MTBDDs) [29, 36]. MTBDDs generalize BDDs [18] by allowing terminal values to be different from 0 or 1. Similar to the role of BDDs in symbolic model checking [45], MTBDD based model checkers leverage the performance benefit due to the succinct representations of the data structures involved.
3.2 Shortcomings of iterative techniques
When computing constrained reachability probabilities using value iteration, both the absolute and relative convergence criteria can result in solutions that are very far from the actual answers. In [31], the authors give a DTMC and a PCTL property whose solution is \(\frac{1}{2}\), yet PRISM reports \(9.77 \times 10^{-4}\) for the absolute criterion and 0.198 for the relative criterion. This drastic error is the result of a premature termination of value iteration. Several other sources of imprecision can also cause state-of-the-art quantitative model checkers to produce unsound results. For example, consider a PCTL formula of the form \({\mathcal {P}}_{ \ge p } (\psi )\) and a system \({\mathcal {M}}\) such that the probability measure of the formula \(\psi \) is exactly p. When value iteration, with floating-point numbers, is used to compute this measure, the value p may only be approached in the limit, and hence the procedure will return some \(p'\) that approximates p from below. This means that the formula \({\mathcal {P}}_{ \ge p } (\psi )\) will evaluate to \({\mathsf {false}}\), where of course the correct value is \({\mathsf {true}}\). This phenomenon was first pointed out in [54]. We also demonstrate a similar phenomenon with the DTMC from Example 1. For the sake of illustration, let \({\hbox {E}}_s = \frac{1}{2}\). Clearly, from the initial state, the probability of reaching a state where sensor 1 fails is exactly \(\frac{1}{2}\) and hence the formula \({\mathcal {P}}_{< \frac{1}{2}} \; [ \; {\mathsf {true}} \;{\mathcal {U}}\; (e^s_1 {=} 1) \; ]\) evaluates to \({\mathsf {false}}\) for the initial state. However, PRISM returns \({\mathsf {true}}\). Errors such as these can be compounded in PCTL formulas containing nested operators, wherein the recursive step of the model checking algorithm returns an incorrect set of states. This can lead to substantial logical errors in model analysis, as we demonstrate with the example below.
Example 3
Let us instantiate the DTMC from Example 1 with \(n=14\) sensors, \(m=1\) actuator, MAX_FAILURES\({=}1\) and with \({\hbox {E}}_s\) = \({\hbox {E}}_a\) = \(\frac{1}{2}\). Recall the third PCTL property of the embedded control system given in Example 2:
When \(\bowtie \) is \(\le \), the PRISM model checker returns \(``0.7096993582589287''\) as the probability for the initial state with both value iteration and interval iterationFootnote 2. With our tool RationalSearch, one can verify that the correct probability is 212895/229376, or \(``0.9281485421316964''\). Further, when \(\bowtie \) is <, PRISM again returns the value given above for both iterative techniques. This time, the actual solution, as generated by RationalSearch, is 0. The errors above are the result of the fact that PRISM incorrectly computes the set of states satisfying \({\mathcal {P}}_{\bowtie \frac{1}{2}} [{\mathsf {true}} \; {\mathcal {U}}\; (e^s_1{=}1) ]\). This error in the recursive step results in an incorrect formulation of the constraints in the outermost constrained reachability problem.
When using interval iteration, we may be unable to conclude whether the DTMC or the MDP being model checked satisfies the given formula. For example, when checking whether a DTMC \({\mathcal {M}}\) satisfies a formula \({\mathcal {P}}_{ \ge p } (\psi ),\) we cannot provide a definite answer if the interval iteration returns that the probability of satisfying \(\psi \) lies in the interval (a, b) where \(p\in (a,b).\)
4 Fixpoint formulations for constrained reachability and expected costs
As discussed in Sect. 2.3, the probability, associated with each state \(z\) in a DTMC, of satisfying a PCTL path formula \(\phi \; {\mathcal {U}}\; \phi '\) can be characterized as the unique solution to a system of linear equations. Similarly, the expected cost of reaching some state satisfying \(\phi \) in a DTMC \({\mathcal {M}}\) starting from any given state \(z\) in \({\mathcal {M}}\) can also be characterized as the unique solution to a linear program. In both these cases, the solution can be seen as the unique fix point of a linear transformation. Thus, when given a candidate solution for the collection of probabilities (or the collection of expected costs), we can check the correctness of this collection by plugging the candidate solution in the corresponding system of equations. In the case of MDPs, the max probabilities, min probabilities, max expected and min expected costs can also be characterized as a solution to a system of equations. For MDPs, however, the system of equations may have multiple solutions. We will show below that when the system of equations for MDPs is not guaranteed to have a unique solution, we can perform an additional graph-theoretic check to confirm that a given candidate solution for the set of probabilities (or the set of expected costs) is correct. Such a confirmation check, as we will discuss in Sect. 5, is crucial to our algorithm for computing exact answers.
4.1 Fixpoint formulation for constrained reachability in MDPs
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be an MDP and \(\phi , \phi '\) be PCTL state formulas. The state-indexed vector \(P^{\mathsf {max}}(\phi \; {\mathcal {U}}\; \phi ')= \lambda z.\, p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) can be characterized as the least fix point (least under pointwise ordering) of the set of equations:
The state-indexed vector \(P^{\mathsf {min}}(\phi \; {\mathcal {U}}\; \phi ')= \lambda z. \, p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) can be similarly characterized by replacing \({\mathsf {max}}\) by \({\mathsf {min}}.\) For \({\mathsf {min}}\), the fix point, in fact, turns out to be unique [9]. For \({\mathsf {max}}\), the fix point is not unique, although several references claim this to be case (see Theorem 10.100 in [10] for example). The non-uniqueness has also been pointed out by [31]. However, for the \({\mathsf {max}}\) case, we show that a simple graph-theoretic check can be performed to verify if a given fix point to the set of equations is indeed the exact solution \(P^{\mathsf {max}}\). We describe this below. We shall need the notion of a memoryless scheduler, namely a scheduler that assigns the same action to any two finite paths ending in the same state (see [9, 10, 52]). A memoryless scheduler \({\mathfrak {S}}_{\mathsf {V}}\) can be considered as a function from states to actions instead of a function from paths to actions.
Let \({\mathsf {V}}: Z\rightarrow [0,1]\) be a solution of the set of equations in Eq. (7). We start by defining a directed graph that is obtained from \({\mathcal {M}}\) by selecting, for each state, the set of actions that potentially achieve the maximum reachability probabilities.
Definition 4
Let \({\mathsf {V}}: Z\rightarrow [0,1]\) be a fix point of Eq. (7). Let \(Z^?=Z{\setminus } ({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \,\cup \,{\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] )\) For each state \(z\in Z^?\), let
Let \({\mathcal {G}}_{\mathsf {V}}=(Z,E)\) be a directed graph such that \((z_1,z_2) \in E \text{ iff } z_1\in Z^? \text{ and } \exists \alpha \in {\mathsf {argmax}}^{\mathsf {V}}_{z_1} \text{ such } \text{ that } {\varDelta }(z_1,\alpha ,z_2) >0.\)
With the above definition of the graph \({\mathcal {G}}_{\mathsf {V}}\), we can characterize the solution to the max reachability problem for MDPs as follows.
Lemma 1
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be a MDP and \(\phi , \phi '\) be PCTL state formulas. For each state \(z\) of \({\mathcal {M}}\), let \(p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) be the maximum probability of satisfying \(\phi \; {\mathcal {U}}\; \phi '.\) Let \({\mathsf {V}}: Z\rightarrow [0,1]\) be a solution of the set of equations given by Eq. (7). Consider \({\mathcal {G}}_{\mathsf {V}}\) as defined in Definition 4 above. Let \(Z_0\) be the set of states \(z\) such that there is no path from \(z\) to any state \(z'\in {\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) in the graph \({\mathcal {G}}_{\mathsf {V}}.\) Then,
Proof
If \(Z= {\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \,\cup \,{\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) then the lemma is immediate. So we will consider the case that \(Z{\setminus } ({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \,\cup \,{\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] ) \ne \emptyset .\) Note also that we have that for each state \(z\in Z\), \({\mathsf {V}}(z)\ge p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) as the state-indexed vector \(P^{\mathsf {max}}= \lambda z.\, p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) is the least fix point of Eq. (7).
It can be easily shown that in order to establish the Lemma, we can assume that \(\phi \) is \({\mathsf {true}}\), \(\phi '\) is some \(a \in {\mathsf {AP}}\), \({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \) and \({\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] \) consists of exactly one state (say \({\mathsf {rej}}\) and \({\mathsf {acc}}\) respectively), exactly one action \(\alpha _0\) is enabled in \({\mathsf {rej}}\) and \({\mathsf {acc}}\), \({\varDelta }({\mathsf {rej}},\alpha _0) = {\mathsf {rej}}\), and \({\varDelta }({\mathsf {acc}},\alpha _0) = {\mathsf {acc}}\).
(\(\Rightarrow \)) It suffices to show that \({\mathsf {V}}(z)\le p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) for each state \(z\in Z.\) Let \(Z^? = Z{\setminus } ({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \,\cup \,{\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] ).\) Let m be the cardinality of \(Z^?.\) From the fact that \({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] =Z_0\), we can construct inductively an enumeration \(z_1,\ldots , z_m \) of states in \(Z^?\) and an enumeration of actions \(\alpha _1,\ldots ,\alpha _m \) in Act such that for each \(1\le i \le m\),
-
1.
\(\alpha _i \in {\mathsf {argmax}}^{\mathsf {V}}_{z_i},\) and
-
2.
\({\varDelta }(z_i,\alpha _i, z)\ne 0\) for some \(z\in \{ {\mathsf {acc}},z_1,\ldots ,z_{i-1} \}.\)
Consider the memoryless scheduler \({\mathfrak {S}}_{\mathsf {V}}\) for the MDP \({\mathcal {M}}\), that picks \(\alpha _i\) when the last state in the execution is \(z_i\in Z^?\) and picks \(\alpha _0\) otherwise. By definition, \({\mathsf {prob}}^{{\mathfrak {S}}_{\mathsf {V}}}_z({\mathsf {true}}\;\;{\mathcal {U}}\;\; a) \le p^{\mathsf {max}}_z({\mathsf {true}}\;\;{\mathcal {U}}\;\; a)\) for each \(z\in Z.\) Thus, it suffices to show that \({\mathsf {prob}}^{{\mathfrak {S}}_{\mathsf {V}}}_z({\mathsf {true}}\;\;{\mathcal {U}}\;\; a) = {\mathsf {V}}(z)\) for each \(z\in Z.\)
Let us now construct a DTMC, \({\mathcal {M}}_0\), from \({\mathcal {M}}\) which picks for each state \(z\), the action \({\mathfrak {S}}_{\mathsf {V}}(z).\) Formally, the DTMC \({\mathcal {M}}_0=(Z,{\varDelta }_0,{\mathbf {C}},L)\) where \({\varDelta }_0(z, z')= {\varDelta }(z, {\mathfrak {S}}_{\mathsf {V}}(z),z')\) for all \(z,z'\in Z.\) It is easy to see that \({\mathsf {prob}}^{{\mathfrak {S}}_{\mathsf {V}}}_z({\mathsf {true}}\;{\mathcal {U}}a)\) is the probability that \(z\) satisfies the formula \({\mathsf {true}}\;{\mathcal {U}}a\) in \({\mathcal {M}}_0.\) By construction of \({\mathcal {M}}_0\), this probability is 0 (1 respectively) if and only if \(z\) is \({\mathsf {rej}}\) (\({\mathsf {acc}}\) respectively). Thus, \(\{ {\mathsf {prob}}^{{\mathfrak {S}}_{\mathsf {V}}}_z({\mathsf {true}}\;\;{\mathcal {U}}\;\; a) \}_{z\in Z}\) is the unique solution of the set of equations:
As \(\alpha _i\in {\mathsf {argmax}}^{\mathsf {V}}_{z_i}\), we get by construction, \({\mathsf {V}}\) is also a solution to Eq. (8). By uniqueness, we must have that \({\mathsf {prob}}^{{\mathfrak {S}}_{\mathsf {V}}}_z({\mathsf {true}}\;\;{\mathcal {U}}\;\; a) = {\mathsf {V}}(z)\) for each \(z\in Z.\)
(\(\Leftarrow \)) The maximum probability of reaching \({\mathsf {acc}}\) is realized by a memoryless scheduler, namely a scheduler that assigns the same action to any two finite paths ending in the same state (see [9, 10, 52]). Fix one such scheduler \({\mathfrak {S}}\). We have that for all states \(z\in Z, {\mathsf {V}}(z)=p^{\mathsf {max}}_z({\mathsf {true}}\;{\mathcal {U}}\; a)= {\mathsf {prob}}^{\mathfrak {S}}_z({\mathsf {true}}\;{\mathcal {U}}\; a).\) From this, it is easy to show that the following hold:
-
1.
\({\mathfrak {S}}(z) \in {\mathsf {argmax}}_{z,{\mathsf {V}}}\) for all \(z\in Z{\setminus }\{ {\mathsf {acc}},{\mathsf {rej}} \}.\)
-
2.
For each \(z\in Z{\setminus }\{ {\mathsf {acc}},{\mathsf {rej}} \}\), there is a finite path \(\rho =z'_1 {\mathop {\longrightarrow }\limits ^{{\mathfrak {S}}(z'_1)}}\cdots {\mathop {\longrightarrow }\limits ^{{\mathfrak {S}}(z'_{\ell -1})}}z'_\ell \) such that \(z'_1=z\) and \(z'_\ell ={\mathsf {acc}}.\)
From the above two observations, we have that \({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] =Z_0.\) \(\square \)
4.2 Fixpoint formulation for expected costs in MDPs.
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be an MDP and \(\phi \) be a PCTL state formula. The state-indexed vector \(E^{\mathsf {max}}= \lambda z.\, e^{\mathsf {max}}_{z}(\phi )\) can be characterized as a fix point of the following set of equations [28] (with the convention that \(0\cdot \infty =0\)):
While \(E^{\mathsf {max}}\) is described to be the least fix point of Eq. (9) in [28], we, in fact, show that Eq. (9) admits only one solution.
Lemma 2
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be a MDP and \(\phi \) be a PCTL state formula. Let \(Z_\phi \) be the set of states of \({\mathcal {M}}\) that satisfy \(\phi .\) For each state \(z\) of \({\mathcal {M}}\), let \(e^{\mathsf {max}}_{z}(\phi )\) be the maximum expected cost of reaching the set of states \(Z_\phi .\) Then \(E^{\mathsf {max}}= \lambda z.\, e^{\mathsf {max}}_{z}(\phi )\) is the unique solution to Eq. (9).
Proof
We only need to show that Eq. (9) has a unique solution. Let \({\mathsf {V}}^1\) and \({\mathsf {V}}^2\) be two solutions of Eq. (9). Observe that \({\mathsf {V}}^1(z)={\mathsf {V}}^2(z)\) for each \(z\in Z_\phi \,\cup \,{\mathsf {Cost}}^{\mathsf {max}}_\infty [\phi ].\) Let \(U=Z{\setminus } (Z_\phi \,\cup \,{\mathsf {Cost}}^{\mathsf {max}}_\infty [\phi ])\) and \(d= {\mathsf {max}}_{z\in U} |{\mathsf {V}}^1(z)-{\mathsf {V}}^2(z)|.\) It suffices to show that \(d=0.\)
We will establish the result reductio ad absurdum. Assume \(d>0.\) By definition, each state \(z\in U\) does not belong to the set \({\mathsf {Cost}}^{\mathsf {max}}_\infty [\phi ].\) This implies that for all schedulers \({\mathfrak {S}}\) and state \(z\in U\), \(p^{\mathfrak {S}}_z({\mathsf {true}}\;{\mathcal {U}}\;\phi )=1.\) This leads to the following observations:
-
1.
For \(z\in U\) and \(\alpha \in {\mathsf {enabled}}(z)\), probability of transitioning from \(z\) on action \(\alpha \) to each state in \({\mathsf {Cost}}^{\mathsf {max}}_\infty [\phi ]\) is 0.
-
2.
For each \(k=1,2\), \(z\in U\) and \(\alpha \in {\mathsf {enabled}}(z)\), let \(v^{k,\alpha }_{z} = {\mathbf {C}}(z,\alpha )+{\sum \limits _{z' \in U}} {\varDelta }(z,\alpha ,z') \cdot {\mathsf {V}}^k(z'). \) By definition and the previous observation, \( {\mathsf {V}}^k(z) = \displaystyle \max _{\alpha \in {\mathsf {enabled}}(z)}v^{k,\alpha }_{z}.\)
-
3.
There is an enumeration \(z_1,\ldots ,z_n\) of states in U such that for each \(1\le i\le n\) and action \(\alpha \), if \(\alpha \in {\mathsf {enabled}}(z_i)\) then \({\varDelta }(z_i,\alpha ,z)\ne 0\) for some state \(z\in Z_\phi \,\cup \,\{ z_j |1\le j<i \}.\)
Claim
\(|{\mathsf {V}}^1(z_i) - {\mathsf {V}}^2(z_i)| < d \) for each \(1\le i\le n\).
Proof
The proof proceeds by induction on i.
Base case Fix \(\alpha _0\in {\mathsf {enabled}}(z_1).\) By construction of \(z_1,\) \( {\sum \limits _{z' \in U}} {\varDelta }(z_1,\alpha _0,z') <1. \)
We have that for each \(k=1,2,\)
Since \(\alpha _0\) is an arbitrary action in \({\mathsf {enabled}}(z_1),\) we get that
Thus, both \({\mathsf {V}}^1(z_1)- {\mathsf {V}}^{2}(z_1) < d\) and \({\mathsf {V}}^2(z_1) - {\mathsf {V}}^{1}(z_1) < d\) establishing the base case.
Induction step Assume that we have \(|{\mathsf {V}}^1(z_i) - {\mathsf {V}}^2(z_i)| < d\) for each \(1\le i\le \ell .\) Now, consider \(z_{\ell +1}\) and fix \(\alpha _0\in {\mathsf {enabled}}(z_{\ell +1}).\) By construction of \(z_{\ell +1}\),
-
Either \( {\sum \limits _{z' \in U}} {\varDelta }(z_{\ell +1},\alpha _0,z') <1\)
-
Or \({\varDelta }(z_{\ell +1},\alpha _0,z_j) >0\) for some \( 1\le j \le \ell \).
If \( {\sum \limits _{z' \in U}} {\varDelta }(z_{\ell +1},\alpha _0,z') <1\) then we can show by an argument similar to the one used in base case that
Now, consider the case when \({\varDelta }(z_{\ell +1},\alpha _0,z_j) >0\) for some \( 1\le j \le \ell .\) Fix one such \(j_0.\) Thus, we have \({\varDelta }(z_{\ell +1},\alpha _0,z_{j_0}) >0.\) By Induction hypothesis, we also have that \(|{\mathsf {V}}^1(z_{j_0}) - {\mathsf {V}}^2(z_{j_0})| < d.\) For each \(k=1,2\),
Since \(\alpha _0\) is an arbitrary action in \({\mathsf {enabled}}(z_{\ell +1}),\) we get once again that
Thus, we get both \({\mathsf {V}}^1(z_{\ell +1})- {\mathsf {V}}^{2}(z_{\ell +1}) < d\) and \({\mathsf {V}}^2(z_{\ell +1})- {\mathsf {V}}^{1}(z_{\ell +1}) < d\) establishing the induction step.
(End: Proof of claim) \(\square \)
Thus, we have that \(d= {\mathsf {max}}_{z\in U} |{\mathsf {V}}^1(z)-{\mathsf {V}}^2(z)| < d\), which is a contradiction. \(\square \)
The state-indexed vector \(E^{\mathsf {min}}(\phi ) = \lambda z.\, e^{\mathsf {min}}_{z}(\phi )\) can also be characterized as a fix point of the following set of equations [9, 28]:
However, in this case, the fix point may not be unique. \(E^{\mathsf {min}}(\phi )\) is the greatest fix point of Eq. (10) [9]. Nevertheless, we can perform an additional check to see if a given solution of Eq. (10) is indeed the function \(E^{\mathsf {min}}(\phi )\).
Let \({\mathsf {V}}: Z\rightarrow {\mathbb {Q}}^{\ge 0}\) be a solution of the set of equations given by Eq. (10). We start by defining a directed graph that is obtained from \({\mathcal {M}}\) by selecting for each state, the set of actions that potentially achieve the minimum expected costs.
Definition 5
Let \({\mathsf {V}}: Z\rightarrow {\mathbb {Q}}^{\ge 0}\) be a fix point of Eq. (10). For each state \(z\in Z{\setminus } (Z_\phi \,\cup \,{\mathsf {Cost}}^{\mathsf {min}}_\infty [\phi ])\), let
Let \({\mathcal {H}}_{\mathsf {V}}=(Z,E)\) be a directed graph such that \( (z_1,z_2) \in E \text{ iff } z_1\in Z{\setminus } (Z_\phi \,\cup \,{\mathsf {Cost}}^{\mathsf {min}}_\infty [\phi ]) \text{ and } \exists \alpha \in {\mathsf {argmin}}^{\mathsf {V}}_{z_1} \text{ st } {\varDelta }(z_1,\alpha ,z_2) >0.\)
The following can be proved along the same lines as Lemma 1:
Lemma 3
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be a MDP and \(\phi \) be a PCTL state formula. For each state \(z\) of \({\mathcal {M}}\), let \(e^{\mathsf {min}}_{z}(\phi )\) be the minimum expected cost of reaching the set \(Z_\phi .\) Let \({\mathsf {V}}: Z\rightarrow {\mathbb {Q}}^{\ge 0}\) be a solution of the set of equations given by Eq. (10). Consider \({\mathcal {H}}_{\mathsf {V}}\) as defined in Definition 5 above. Let \(Z_\infty \) be the set of states \(z\) such that there is no path from \(z\) to any state \(z'\in Z_\phi \) in the graph \({\mathcal {H}}_{\mathsf {V}}.\) Then
5 Exact model checking
As demonstrated in Sect. 3, approximate solution techniques can lead to unreliable results and the incorrect analysis of systems. To rectify this serious limitation, tools such as PRISM and STORM have implemented exact model checking engines, which make heavy use of techniques from parametric model checking [21, 23, 33, 34]. The idea behind these engines is to interpret the probabilistic model (DTMC or MDP) as a finite automaton in which transitions probabilities are described by letters of an alphabet. When one is interested in costs, states are additionally labeled by a cost structure. Using techniques derived from state elimination [37], one can then calculate a regular expression representing the language of this automaton. The core idea of this translation is to eliminate a state s by increasing the probability of moving from each predecessor \(s_1\) of s to each successor \(s_2\) of s by the probability of moving from \(s_1\) to \(s_2\) when passing through s. In the case of parametric model checking, various techniques can then be used to translate the regular expression into a rational function over the parameters of the model. When using this approach for exact model checking, one can likewise derive a parameter-free function that describes the property in question.
Although they rectify the problems with approximation techniques, the exact quantitative model checking engines implemented in tools like PRISM and STORM don’t scale as well as their iterative counterparts. See Example 4 below and Sect. 7 for a complete analysis. The goal of our technique, to which the remainder of this section is dedicated, is to utilize the advantages of fast approximate model checking techniques to produce exact solutions.
Example 4
Again consider the DTMC modeling an embedded control system with the parameters given in Example 3. To guarantee the correctness of one’s analysis, exact solution techniques must be employed. Unfortunately, the exact model checking engines of PRISM and STORM do not scale well enough to analyze this example, which contains about 4.8 million states and about 44 million transitions. Under our test setup (see Sect. 7), both tools reached a 30-min timeout when trying to analyze the properties from Example 3. On the other hand, RationalSearch found the exact answer to both the formulae in under a minute.
We now describe our approach for exact model checking. The broad idea is to utilize approximate solutions generated by an iterative technique, and then successively refine these solutions to the exact solution. We begin by first describing the first ingredient of our solution—the Kwek Mehlhorn algorithm [40] in Section 5.1. We then describe the overall algorithm in Sect. 5.2.
5.1 The Kwek–Mehlhorn algorithm
Given an ordered set of integers of bounded size, the classical binary search algorithm can be used to find the smallest element in the set that is larger than a given value, in logarithmic time. Kwek and Mehlhorn [40] extend this methodology to efficiently locate the rational number with the smallest size in a given interval. In our paper, we present a novel application of this technique, where approximate answers to quantitative model checking problems can be used to generate exact solutions efficiently.
Let \(I = [\frac{\alpha }{\beta }, \frac{\gamma }{\delta }]\) be an arbitrary interval with rational end-points. It was established [40] that for such an interval, there exists a unique rational \(a_{\min }(I) /b_{\min }(I)\) such that for all rational numbers \(\frac{a}{b} \in I\), \(a_{\min }(I) \le a\) and \(b_{\min }(I) \le b\). We will call \(a_{\min }(I) /b_{\min }(I)\) the minimal fraction of I. Further, this minimal fraction \(a_{\min }(I) /b_{\min }(I)\) can be found using Algorithm 1 from [40]. The input to the findFraction procedure are integers denoting the numerators and denominators of the endpoints of the interval I, and the output is a pair of integers, corresponding to the numerator and denominator of the unique minimal fraction of the input interval.
Let \(Q_M = \{p/q |p,q \in \{1, ..., M\} \} \cap [0,1]\). For \(\mu \in {\mathbb {N}}\), if \(\frac{a}{b} \in Q_M\) is contained in the interval \([\frac{\mu }{2M^2}, \frac{\mu +1}{2M^2}]\) of length \(\frac{1}{2M^2}\) then \(\frac{a}{b}\) is the unique element of \(Q_M\) in \([\frac{\mu }{2M^2}, \frac{\mu +1}{2M^2}]\). It turns out that \(\frac{a}{b}\) must also be the minimal element of \([\frac{\mu }{2M^2}, \frac{\mu +1}{2M^2}]\), meaning it can be found using Algorithm 1 in time \(O(\log M)\).
5.2 Rational search
In this section, we explain our approach for the exact quantitative model checking of PCTL formulas. The critical insight we exploit is that iterative techniques for solving constrained reachability typically converge very fast and produce a precise enough answer. Using this precise approximation, we can then effectively construct a small interval so that the minimal fraction in the interval corresponds to an element of the exact solution vector, and thus the Kwek–Mehlhorn algorithm can be employed to find the exact solution.
Recall that each iterative technique for approximating a set of equations, like those given in Eqs. (1) and (3), yields a different guarantee on the precision of an approximate solution. The difference between the approximation generated by interval iteration and the actual solution is bounded by a given \(\epsilon \) value, provided there are no errors generated by floating-point arithmetic. Value iteration, on the other hand, comes with no such guarantees. When an approximate solution vector contains values of known precision, like in the case of interval iteration, one can translate it into an exact solution vector as follows. For each value q in the vector, construct the interval \([q-\epsilon , q+\epsilon ]\) and run Algorithm 1 to find the smallest rational in this interval. Then, check that the generated rational values \({\mathsf {V}}^{\star }\) are correct by verifying that they satisfy the fix point equations for constrained reachability and expected costs. In addition, if the algorithm also checks that condition on the graph \({\mathcal {G}}_{{\mathsf {V}}^\star }\) (or \({\mathcal {H}}_{{\mathsf {V}}^\star }\)) also hold in accordance with Lemma 1 (Lemma 3 respectively) if we are computing max reachability probabilities (min reachability respectively) properties. Lemmas 1 and 3, along with the uniqueness of the fix points for the rest of the cases, imply that these checks are only satisfied by the desired solution vector. If these checks fail for the candidate solution vector, one obtains a more precise approximation and re-runs the procedure.
When a solution vector contains values of unknown quality, we can find exact solutions using a similar technique. Here the idea is to “guess” a sequence intervals, with decreasing sizes, that may contain the actual value. This process is formalized in Algorithm 2, which takes as input the model \({\mathcal {M}}\), a maximum precision P and a state-indexed vector \({\mathsf {V}}^{\dagger }\) that approximates the exact solution vector \({\mathsf {V}}\).
For a given precision p and state \(z\), bounds\((p,{\mathsf {V}}^\dagger (z))\) returns \(\alpha , \beta , \gamma , \delta \) such that \(\alpha \) is the first p decimal digits of the fractional part of \({\mathsf {V}}^\dagger (z),\) \(\beta =10^p\), \(\gamma = \alpha +1\) and \(\delta =\beta \). Observe that \({\alpha }/{\beta }\) is the rational representation of the first p digits of the fractional part of \({\mathsf {V}}^\dagger (z)\). From this approximation, we identify a sharpened solution vector \({\mathsf {V}}^{\star }\) using the findFraction procedure from Algorithm 1. The procedure fixpoint then tests if \({\mathsf {V}}^{\star }\) is the correct solution by checking if the equation satisfies the appropriate fix point equation in addition to the check, if needed, required by Lemma 1 or 3. If the input vector \({\mathsf {V}}^{\dagger }\) is not precise enough, then shapren returns “\({\mathsf {null}}\)”, indicating that more precision is required to infer an exact solution. The guarantees of Algorithm 2 are formalized as follows. Let \({\mathsf {V}}^{b}\) satisfying \(|{\mathsf {V}}(z) - {\mathsf {V}}^b(z)|\le 10^{-b}\) for all \(z\in Z\) be an approximate solution vector of precision b. Then, Lemma 4 establishes that starting from a close enough approximation, Algorithm 2 finds the actual solution vector.
Lemma 4
Let \({\mathcal {M}}\) be an MDP with the set of states \(Z\). Let \(\xi \) be a PCTL path formula or a PCTL state formula. Given an objective \({\mathsf {obj}}\in \{ {\mathsf {max}},{\mathsf {min}} \},\) let \({\mathsf {V}}\) be the vector \(\lambda z\cdot p^{{\mathsf {obj}}}_z[\xi ]\) if \(\xi \) is a path formula and the vector \(\lambda z\cdot e^{{\mathsf {obj}}}_z[\xi ]\) if \(\xi \) is a state formula. Let \( b, P \in {\mathbb {N}}\) be such that \(P \ge b\) and \({\mathsf {V}}^b\) is an approximate solution vector of precision b. If \({\mathsf {V}}(z) \in Q_{\lfloor \sqrt{ 10^{b} / 2} \rfloor }\) for every \(z\in Z\), then \({\textsc {sharpen}}({\mathcal {M}}, P, {\mathsf {V}}^b, \xi , {\mathsf {obj}}) = {\mathsf {V}}\).
Proof
Fix a state \(z\) and assume \({\mathsf {V}}(z) \in Q_M\) for \(M{=}\lfloor \sqrt{10^b/2}\rfloor \). If \(P{\ge }b\) then
sharpen\(({\mathcal {M}}, P, {\mathsf {V}}^b,\xi , {\mathsf {obj}})\) searches for \({\mathsf {V}}(z)\) in \(I=[\alpha /\beta ,\gamma /\delta ]\) for \(\alpha ,\beta ,\gamma ,\delta = {\textsc {bounds}}(b, {\mathsf {V}}^b(z))\). Now, \({\mathsf {V}}(z)\in I\) since \({\mathsf {V}}^b(z)\) satisfies \(|{\mathsf {V}}(z) - {\mathsf {V}}^b(z)|\le 10^{-b}\). Further, \(|I| = 10^{-b} \le \frac{1}{2M^2}\). Due to Kwek et. al. [40], we have that an interval of size \(\frac{1}{2M^2}\) contains at most 1 element of \(Q_M\). Clearly, findFraction\((\alpha ,\beta ,\gamma ,\delta )\) returns \({\mathsf {V}}(z)\) which is the unique “minimal” element in \(I \cap Q_M\). \(\square \)
Using the techniques for sharpening an approximate solution into an exact value from Algorithm 2, we can now derive a procedure for solving constrained reachability (and hence PCTL) formulas exactly. The procedure is given in Algorithm 3, which takes as arguments an MDP or DTMC \({\mathcal {M}}\), a constrained reachability formula \(\phi \) and a precision \(\epsilon \). The \({\textsc {iteration}}\) procedure can be either of value iteration or interval iteration. Algorithm 3 begins by running the iteration procedure up to a given precision \(\epsilon \). If the procedure is value iteration, \(\epsilon \) is used in the convergence criterion—absolute or relative—described in Section 3. In the case of interval iteration, \(\epsilon \) defines the bound on the maximum error in the approximate solution vector. The approximate solution vector \({\mathsf {V}}^{\dagger }\) generated by the iteration procedure is then used by the shapren procedure, which attempts to strengthen the approximate answer to an exact one. Note the version of the shapren varies according to the iterative method being utilized. If it succeeds, the whole process terminates. Otherwise, \({\mathsf {V}}^{\dagger }\) is further refined by re-invoking iteration with an increased \(\epsilon \) precision, and the sharpening process is repeated.
When successive approximations in value iteration or interval iteration are computed using arbitrary precision arithmetic, the correctness guarantees of Algorithm 3 can be stated as follows.
Theorem 1
Let \({\mathcal {M}}\) be an MDP with the set of states \(Z\). Let \(\xi \) be a PCTL path formula or a PCTL state formula. Given an objective \({\mathsf {obj}}\in \{ {\mathsf {max}},{\mathsf {min}} \},\) let \({\mathsf {V}}\) be the state-indexed vector \(\lambda z\cdot p^{{\mathsf {obj}}}_z[\xi ]\) if \(\xi \) is a path formula and the vector \(\lambda z\cdot e^{{\mathsf {obj}}}_z[\xi ]\) if \(\xi \) is a state formula. Then, \({\textsc {RationalSearch}}({\mathcal {M}}, \xi , {\mathsf {obj}}, \epsilon _0)\) (with \(\epsilon _0 > 0\)) terminates and returns the exact solution vector \({\mathsf {V}}\).
Proof
It is easy to see that there is a \(b>0\) such that, for every state \(z\), \({\mathsf {V}}(z) \in Q_N\) for \(N=\lfloor \sqrt{10^b/2} \rfloor \). Now, since value iteration converges in the limit, we have that the first b digits of \({\mathsf {V}}^\dagger (z)\) match that of \({\mathsf {V}}(z)\) for each state \(z\in Z\), eventually. Also, in every iteration of the loop in Algorithm 3, sharpen is invoked with an incremented value of P and eventually \(P\ge b\). \(\square \)
We now state the complexity of computing the exact solutions using RationalSearch. As before, we assume that the transition probabilities are given as rational numbers.
Theorem 2
Let \({\mathcal {M}}\) be an MDP with the set of states \(Z\). Let \(n = |Z|\), \(m = |\{ (z, \alpha , z') | \alpha \in {\mathsf {enabled}}(z), {\varDelta }(z, \alpha )(z') > 0 \}|\) and let \(\delta \) be the largest denominator in any probability value in the transition function of \({\mathcal {M}}\). Let \(\xi \) be a PCTL path formula. Let \(p_{\mathsf {min}}\) be the \(\min \{ \delta (z,\alpha ,z') |{\varDelta }(z, \alpha )(z') > 0 \}.\) Given an objective \({\mathsf {obj}}\in \{ {\mathsf {max}},{\mathsf {min}} \}\) and let \({\mathsf {V}}\) be the state-indexed vector \(\lambda z\cdot p^{{\mathsf {obj}}}_z[\xi ]\). Let \(\ell =\frac{n(m+n) \log \delta }{p^n_{\mathsf {min}}}.\) Then, \({\textsc {RationalSearch}}({\mathcal {M}}, \xi , {\mathsf {obj}}, 1)\) makes at most \(O(\ell )\) value iteration steps, \(O(n\ell ^2)\) calls to FindFraction, and \(O(\ell ^2)\) calls to FixPoint, assuming arbitrary precision arithmetic.
Proof
Observe that we can assume without loss of generality that there is at least one transition probability that is contained in the open interval (0, 1) (Otherwise, the value iteration finishes in zero steps as all probabilities are 0 or 1).
We will proceed as follows. We assume that the objective \({\mathsf {obj}}\) is \({\mathsf {min}}.\) We first estimate the number of iterations k of value iteration that are required to reach an approximate solution state-indexed vector \({\mathsf {V}}^\dagger \) of precision b such that \({\mathsf {V}}^\dagger \) can be used to obtain the exact solution V using one call to sharpen based on Lemma 4..
From [19], we know that the maximum denominator (and thus maximum numerator) of any value in \(\{ {\mathsf {V}}(z) | z\in Z \}\) is less than \(\delta ^{4m}\). Now, the required precision b satisfies \(\big \lfloor \sqrt{\frac{10^b}{2}}\big \rfloor \ge \delta ^{4m}\), giving us
Let us now estimate an upper bound on the number of steps of value iteration that are required to guarantee that the resulting approximate solution vector \(||{\mathsf {V}}- {\mathsf {V}}^\dagger || < 10^{-b}\). Here, the norm \(||\cdot ||\) is defined to be the pointwise maximum.
Let \({\mathcal {U}}=[0,1]^Z\) be the set of all state-indexed vectors. For a vector \({\bar{x}}\) we denote its \(z^\text {th}\) component by \({\bar{x}}(z).\) Consider the function \(f:{\mathcal {U}} \rightarrow {\mathcal {U}}\) be the function such that
Observe that value-iteration described in Section 3 is such that \({{\bar{x}}}_0\) is the vector all of whose components is 0, and \({\bar{x}}_{i+1} = f({\bar{x}}_i)\). The n-th iterate of f, namely \(f^n\), is a contracting mapping (Please see Appendix A for the proof):
Claim
For all vectors \({{\bar{x}}},{{\bar{y}}}\in {\mathcal {U}},\)
where \(q = (1-p_{\mathsf {min}}^n)\) and \(p_{\mathsf {min}}\) is the smallest non-zero probability in the description of \({\mathcal {M}}\).
Let \({\mathsf {V}}^\dagger = {\bar{x}}_{i\cdot n}\) be the required approximation, obtained after \(i\cdot n\) value iteration steps. Using, Banach’s fixpoint theorem [12], we have
Based on our requirement for \(k = i\cdot n\), we will need only one function call to Sharpen if
Let \(i_0\) be an integer such that
We have that \(i_0\) is an upper bound on i.
Now \(q^{i_0} < \frac{\delta ^{-8m} (1-q)}{2}\) iff
Since \(\log (1- p^n_{\mathsf {min}})\) is negative, we get that \(q^{i_0} < \frac{\delta ^{-8m} (1-q)}{2}\) iff
Observe that \(p_{\mathsf {min}}\ge \frac{1}{\delta }\). Thus, \( \log p_{\mathsf {min}}\ge - \log \delta \) and hence
Thus, \(q^{i_0} < \frac{\delta ^{-8m} (1-q)}{2}\) if
Using the inequality \(\ln (1+x) \le x\) for \(x>-1,\) we have that \(\ln (1-p^n_{\mathsf {min}}) \le -p^n_{\mathsf {min}}\) and hence \(\frac{-\ln 2}{p^n_{\mathsf {min}}} \le \frac{1}{\log (1-p^n_{\mathsf {min}})}\) and hence \(\frac{-1}{p^n_{\mathsf {min}}} \le \frac{1}{\log (1-p^n_{\mathsf {min}})}.\) Since multiplying an inequality by a negative number changes signs, we get that
Thus, \(q^{i_0} < \frac{\delta ^{-8m} (1-q)}{2}\) if
Thus, we are guaranteed to terminate the algorithm using one call to Sharpen after k steps, where
Now, let us analyze the calls to Sharpen. Note that the jth call to Sharpen has precision \(P_j=j.\) The maximum value of \(P_j\) is k. Every call to Sharpen gives rise to \(nP_j\) calls to FindFraction and \(P_j\) calls to FixPoint, giving us \(O(n\ell ^2)\) calls to FindFraction and \(O(\ell ^2)\) calls to FixPoint.
When \({\mathsf {obj}}\) is \({\mathsf {max}}\), then please note that there is a memoryless scheduler \({\mathfrak {S}}: Z\rightarrow {\mathsf {Act}}\) such that for each state \(z\in Z,\) \(p^{\mathsf {max}}_z(\xi )= p^{\mathfrak {S}}_z(\xi ).\) Consider the functions \(f_1,f_2:{\mathcal {U}} \rightarrow {\mathcal {U}}\) defined as follows:
and
Observe that value-iteration described in Sect. 3 is such that \({{\bar{x}}}_0\) is the vector all of whose components is 0, and \({\bar{x}}_{i+1} = f_2({\bar{x}}_i)=f_2^i({\bar{x}}_0)\).
Now, it is easy to see that the required solution vector \({\mathsf {V}}\) is the pointwise limit \(\lim _{i\rightarrow \infty } f^i_1 ({\bar{x}}_0) = \lim _{i\rightarrow \infty } f^i_2 ({\bar{x}}_0).\) Further, we also have that for each i, \(f^i_1 ({\bar{x}}_0) \le f^i_2 ({\bar{x}}_0)\le {\mathsf {V}}\) and hence \( || {\mathsf {V}}- {\bar{x}}_i || \le || {\mathsf {V}}- f^i_1({\bar{x}}_0) ||.\) Observe that we can show \(f^i_1\) is contracting with factor \(1-p^n_{\mathsf {min}}\) exactly like the claim above. The theorem now follows similar to the case when \({\mathsf {obj}}\) is \({\mathsf {min}}.\) \(\square \)
Example 5
Our experiments show that Algorithm 3 can make non-trivial improvements to solution quality. Consider the standard example of tossing N biased coins independently, where each coin yields heads with probability 1/3 and tails with probability 2/3. Analyzing the DTMC model to compute the probability of the event that 11 coins land heads, PRISM’s floating-point model checker returned the decimal “0.000005645029269476758”. Our tool could correctly determine the exact probability to be 1/177,147 by examining with the first 12 digits of this approximate answer. This is remarkable given that the period of this fraction (and hence its most succinct decimal representation) is almost 20,000 digits long. Moreover, the algorithm is able to simultaneously infer the reachability probabilities for all of the roughly 200,000 states of the model with a single fixpoint check. This illustrates another advantage of our technique; the algorithm is agnostic of the number of initial states in the system. The exact model checking engine of PRISM, on the other hand, currently only supports systems with a single initial state.
6 Implementation
We have implemented Algorithm 3 in our tool RationalSearch, which is an extension of the PRISM model checker (version 4.3.1). RationalSearch is available for download at [8]. Before describing our integration with PRISM, we briefly describe the relevant portions of its architecture. PRISM is a Java-based tool comprised of four solution engines, three of which (Mtbdd, Hybrid, Sparse) are based (entirely or partially) on symbolic methods using compact data structures like MTBDDs. The fourth engine (Explicit) manipulates sparse matrices, vectors and bit-sets directly (without any symbolic data structures).
The Sparse engine is similar to the Explicit engine in that it uses explicit data structures for storing vectors and matrices. However, it makes use of symbolic data structures during model construction, allowing it to efficiently remove portions of the state space that are not reachable. This is achieved through a conjunction of the MTBDD representing the model’s state space with a BDD representing the characteristic function for the reachable states of the model. The Mtbdd engine is based entirely on symbolic data structures. During value iteration, the transition matrix and solution vector are both given as MTBDDs. The matrix-vector multiplications used to update the solution vector are carried out over these data structures. As described in [48], one drawback of this approach is that the size of the MTBDD storing the solution vector can grow substantially as more computations are performed. To tackle the MTBDD size explosion, the Hybrid engine combines the advantages present in both the symbolic and explicit engines. In particular, it stores the solution vector as a fixed size array and the transition matrix as an MTBDD (which can usually be done succinctly due to symmetry in the model). Updates to the solution vector are carried out by operations over these mixed-type data structures.
RationalSearch implements Algorithm 3 on top of all four engines for model checking DTMCs against PCTL specifications. For exact model checking of MDPs, our tool RationalSearch implements Algorithm 3 for all four engines when the PCTL specification does not involve computing any max probabilities and minimum expected costs. RationalSearch only supports the Explicit engine for the case of max probabilities and min rewards in MDPs, for which the fixpoint check involves additional graph-theoretic analyses (see Section 4). The architecture of our extension is outlined in Fig. 2. It intercepts PRISM’s routine for solving constrained reachability probabilities and expected costs, sharpening the probabilities every time it is invoked. These engines are built using floating-point numbers, which can store at most 16 digits in the fractional part of the decimal expansion of any floating-point number. Hence, the convergence criteria support a minimum \(\epsilon \) of \(10^{-16}\). Our implementation, thus, bypasses the \(\epsilon \) refinement loop from Algorithm 3 and directly invokes the procedure iteration for the maximum precision supported by doubles. Further, for computing max reachability probabilities, checking whether the candidate solution vector returned by the Explicit engine is a fixpoint, we do not take recourse to Lemma 1. Instead, we take advantage of PRISM’s ability to return a candidate memoryless scheduler that achieves the maximum reachability property. The candidate scheduler \({\mathfrak {S}}\) returned by PRISM is a proper scheduler, whose definition we articulate below.
RationalSearch Architecture: Given a PCTL formula \(\varphi \), PRISM (equipped with CUDD) approximates the solution using value/interval iteration. The sharpen procedure uses this approximation \(V^\dagger \) and employs findFraction, in conjunction with the rational extension to CUDD (CUDD + GMP), to generate a candidate rational vector. If this candidate rational vector satisfies an appropriate fixpoint check, it is guaranteed to be correct. Otherwise, the process is repeated with a better approximation
Definition 6
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be a MDP and \(\phi , \phi '\) be PCTL state formulas. A memoryless scheduler \({\mathfrak {S}}\) for \({\mathcal {M}}\) is said to be proper for \({\mathcal {M}},\phi ,\phi '\) if for each \(z\in Z{\setminus } {{\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] \cup {\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi ']}\), there is a sequence of states \(z_1,\ldots ,z_\ell \) such that
-
\(z_1=z\),
-
\(z_\ell \in {\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi ']\), and
-
\({\varDelta }(z_i,{\mathfrak {S}}(z),z_{i+1})>0\) for each \(1\le i < \ell .\)
In order to check whether a given candidate solution, \({\hat{{\mathsf {V}}}}\), to the set of Eqs. (7) is indeed the actual exact solution \({\mathsf {V}}= \lambda z\cdot p^{\mathsf {min}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\), it suffices to check that the proper scheduler, \({\mathfrak {S}}\), returned by PRISM is such that \({\mathfrak {S}}(z) \in {\mathsf {argmax}}^{{\hat{{\mathsf {V}}}}}_z\) for every \(z\in Z{\setminus } {{\mathsf {Prob}}^{{\mathsf {max}}}_{0}[\phi \; {\mathcal {U}}\; \phi '] }\,\cup \,{{\mathsf {Prob}}^{{\mathsf {max}}}_{1}[\phi \; {\mathcal {U}}\; \phi '] }:\)
Proposition 1
Let \({\mathcal {M}}= (Z, {\mathsf {Act}}, {\varDelta }, {\mathbf {C}}, L)\) be a MDP, \(\phi , \phi '\) be PCTL state formulas and \({\mathfrak {S}}\) a proper memoryless scheduler for \({\mathcal {M}},\phi ,\phi '\). For each state \(z\) of \({\mathcal {M}}\), let \(p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) be the maximum probability of satisfying \(\phi \; {\mathcal {U}}\; \phi '\) in \({\mathcal {M}}.\) Let \({\hat{{\mathsf {V}}}} : Z\rightarrow [0,1]\) be a solution of the set of equations given by Eq. (7). Suppose further that
Then \(\forall z\in Z,\, {\hat{{\mathsf {V}}}}(z)=p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ').\)
Proof
As \({\mathsf {V}}= \lambda z\cdot p^{\mathsf {max}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) is the least fix point of Eq. (7), we have that for each state \(z\in Z,\)
Thus, it suffices to show that \(p^{\mathfrak {S}}_{z}(\phi \; {\mathcal {U}}\; \phi ') = {\hat{{\mathsf {V}}}}(z)\) for each \(z\in Z.\)
Let \({\mathsf {prop}}_\phi , {\mathsf {prop}}_{\phi '}\) be distinct propositions. Given a proper memoryless scheduler \({\mathfrak {S}}\) for \({\mathcal {M}}, \phi ,\phi '\), let \({\mathcal {M}}^{\mathfrak {S}}_{\phi ,\phi '}=(Z, {\mathsf {Act}}, {\varDelta }^{\mathfrak {S}}, {\mathbf {C}}, L^{\mathfrak {S}})\) be the DTMC such that \({\varDelta }^{\mathfrak {S}}(z,z')={\varDelta }(z,{\mathfrak {S}}(z),z')\), \(L^{\mathfrak {S}}(z)= \{ {\mathsf {prop}}_\phi \}\) if \({\mathcal {M}}, z\models \phi \) and \(L^{\mathfrak {S}}(z)= \{ {\mathsf {prop}}_{\phi '} \}\) if \({\mathcal {M}}, z\models \phi '.\) It is easy to see that \(p^{\mathfrak {S}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) is exactly the probability of \(z\) satisfying the formula \({\mathsf {prop}}_{\phi '}\;{\mathcal {U}}\;{\mathsf {prop}}_{\phi '}\) in \({\mathcal {M}}^{\mathfrak {S}}_{\phi ,\phi '}.\) Observe further that from the fact that \({\mathfrak {S}}\) is proper, the set of states of \({\mathcal {M}}^{\mathfrak {S}}_{\phi ,\phi '}\) that satisfy \({\mathsf {prop}}_{\phi '}\;{\mathcal {U}}\;{\mathsf {prop}}_{\phi '}\) with probability 0 (1 respectively) is exactly the set \({\mathsf {Prob}}^{{\mathsf {max}}}_{0}[ \phi \; {\mathcal {U}}\; \phi ']\) ( \({\mathsf {Prob}}^{{\mathsf {max}}}_{1}[ \phi \; {\mathcal {U}}\; \phi ']\) respectively). Since \({\mathcal {M}}^{\mathfrak {S}}\) is a DTMC, \({\mathsf {V}}^{\mathfrak {S}}= \lambda z\cdot p^{\mathfrak {S}}_{z}(\phi \; {\mathcal {U}}\; \phi ')\) is the unique solution to the set of equations:
Finally, observe that \({\hat{{\mathsf {V}}}}\) is a solution to the above Eq. (11). Hence, we must have \(p^{\mathfrak {S}}_{z}(\phi \; {\mathcal {U}}\; \phi ') = {\hat{{\mathsf {V}}}}(z)\) for each \(z\in Z.\) \(\square \)
Among the four engines, Explicit is the only one implemented entirely in Java. To support the Explicit engine, our tool uses the libraries JScience [7] and Apfloat [4] to construct the transition matrix using rational entries, perform matrix-vector multiplications for the fixpoint check in Algorithm 3, and implement the Kwek–Mehlhorn algorithm (Algorithm 1).
PRISM implements the remaining three engines using an extension of the CUDD library [5]. The off-the-shelf version of CUDD only supports floating-point numbers at the terminals. RationalSearch enhances CUDD by allowing terminals to hold either floating-points or arbitrary-precision rational numbers provided by the GNU MP library [6]. Our extension allows the data type at a terminal node to be easily interchanged, and the full suite of MTBDD operations can be performed regardless of the data type.
RationalSearch makes use of this extended CUDD functionality in the following manner. When the model is parsed, it constructs two transition matrices, one with doubles at the terminal nodes and one with rationals. The procedure iteration uses double-precision transition matrix to generate a double-precision solution vector. RationalSearch translates this solution vector into a candidate solution vector stored as a rational MTBDDs using sharpen. The fixpoint check from sharpen can then be performed by an MTBDD matrix-vector multiplication between rational MTBDDs.
Algorithm 3 has also been integrated into the STORM model checker. Their implementationFootnote 3 differs from ours in that it supports running iteration with both floating-point and arbitrary-precision numbers. It begins by running value iteration using floating-point numbers and attempts to infer and exact solution from the approximation. If double-precision is determined to be insufficient for extracting the precise solution, the approximation engine is re-invoked using arbitrary-precision numbers. Another significant difference in the STORM implementation is that STROM uses the Sylvan [24] MTBDD library instead of CUDD. Sylvan provides built-in support for arbitrary precision arithmetic.
7 Evaluation
7.1 Setup
We evaluated our tool against examples involving quantitative reachability and costs from the PRISM benchmark suite and case studies [2, 3] and compared the results with the exact parametric engines implemented in PRISM and STORM. In particular, we used version 4.3.1 of PRISM and version 1.0.0 of STORM. Our tests were carried out on an Intel core i7 dual-core processor @2.2 GHz with 8 Gb RAM running macOS 10.12.4.
7.2 Benchmarks
Our focus has been to evaluate the performance of our technique on different probabilistic models (MDPs and DTMCs) against different objectives (Reachability, Cost, full-fledged PCTL). Our PCTL examples, in particular, have been crafted from scratch. Our benchmarks have been selected from the PRISM benchmark suite and case studies [2, 3] by keeping some key objectives in mind. First, in order to stress-test our technique, we tried to choose benchmarks with large state spaces. In fact, most of our benchmarks have state spaces of the order of \(10^5\)–\(10^6\). Second, we also selected some benchmarks (for example, biased coins, ECS, leader election) for which the probability values corresponding to the properties have high precision, that is, their decimal representation requires many digits. We believe that such benchmarks demonstrate the need for exact model checking, as well as, the effectiveness of our technique in determining the correct rational representations of the probabilities. In this process of benchmark selection, we omitted benchmarks for which the resulting answers are trivial (either 0 or 1 probability) or those for which our technique could not result in a fix point. We recall that due to floating-point errors, PRISM’s approximate answer may never get close enough (in a precise sense stated in Theorem 1, Sect. 5) to the actual exact answer (despite an arbitrary number of iterations) and as a consequence, RationalSearch may declare that it did not find an exact answer. We note that our tool never reports an incorrect answer.
7.3 Performance overhead
We examined the overhead incurred by RationalSearch’s extension of PRISM. The results are given in Table 1 for the approximation engines Explicit, MTBDD and Hybrid of PRISM. Due to the similarity between the Explicit and Sparse engines, we chose to only report metrics for the former. In Table 1, all of the tests were conducted using value iteration as the approximation scheme. The overhead incurred for interval iteration is similar and thus not reported. The quantitative properties tested against in two of the MDP benchmarks (‘Fair Exch.’ and ‘Dice Coin’) involve computation of max probabilities. Recall that RationalSearch supports this combination only for the Explicit engine, and as a result, the corresponding entries in columns 8–11 (MTBDD and Hybrid engines) are marked ‘-’ for these benchmarks.
On several examples with large state spaces, the Explicit engine fails with an out-of-memory exception. This can be attributed to the fact that the implementation stores two copies of the transition matrix in memory. On all the examples where Explicit fails, the symbolic engines (MTBDD and Hybrid) find the solution quickly, typically with an overhead of less than 50%. For the examples on which the Explicit engine did not encounter an out-of-memory exception, overhead times where much higher. One major reason for this difference is that the Explicit engine stores the solution vector as an array. Further, in this case, RationalSearch runs the sharpen procedure for each element of this array, thus resulting in redundant computation when a number appears multiple times. By contrast, the symbolic engines perform symmetry reductions on the data structures and store only distinct values at the terminal nodes of the solution vector. As a result, sharpen needs only be run once for each terminal node.
An encouraging observation from our results was that the overhead times did not vary drastically with the size of the model or the type of property being checked. In particular, both PCTL properties that we examined required solving three instances of constrained reachability properties. In spite of this, the overhead induced by RationalSearch on these examples remained consistent with the other examples.
Comparison with exact engines We also compared RationalSearch with the exact engines implemented in PRISM and STORM. The results are reported in Table 2. The existing exact engines of both PRISM and STORM were invoked with the -exact flag. In addition, STORM also uses the flag –minmax:method pi. RationalSearch was run with the underlying Hybrid engine and value iteration with absolute convergence criterion (with \(\epsilon = 10^{-16}\)) as the underlying approximation scheme. We set javamaxmem=4g and cuddmaxmem=4g wherever applicable. As before, Table 2 does not include benchmarks ‘Fair Exch.’ and ‘Dice Coin’ from Table 1. This is because these benchmarks are MDP models, and the specifications to be tested involve computation of max probabilities, which the Hybrid engine of RationalSearch does not currently support.
RationalSearch drastically outperformed PRISM’s exact engine; in many cases, by several orders of magnitude. For about half of the examples, PRISM’s exact engine reached the 30-min timeout. In every case, RationalSearch was able to find the exact solution in a matter of seconds. The comparison with the STORM tool is more competitive. For the majority of the small and medium-size examples (IPv4, Fair Exchange, Firewire, Dining Philosophers), the running times for both engines were within the same order of magnitude. However, the performance benefit of RationalSearch became apparent with large models (Biased Coins, Dice, ECS). RationalSearch achieved a 200x speed-up on the example of the biased coins and 45x speed-up on the dice example. For the embedded control system example, RationalSearch returned a solution in a matter of seconds while both PRISM and STORM hit the 30 min timeout.
In order to check the scalability of each of the exact engines, we also compared the running times on specific models (Biased Coins and Dice) where the number of states is governed by parameters that can be tuned to change the size of the underlying models. The results are depicted in Fig. 3, where we use an approximate engine of PRISM as a baseline for our comparative analysis. Several interesting observations can be made here. As expected, the approximate engine of PRISM is the fastest. Since, RationalSearch is crucially tied to the approximate engine(s) in PRISM, it is not surprising again, that (RationalSearch) scales very well on large models, with comparable performance to the underlying approximate engine because of the low overhead our technique imposes. While the existing exact model checking engines in PRISM and STORM do perform well when the models are small, the performance quickly degrades when the models become reasonably large (the scale is a logarithmic scale). This clearly demonstrates the power of the insight that the approximate answers from fast iterative model checking techniques can be utilized to obtain exact rational solutions with only a little overhead.
Scaling Comparison. Running times for various model checking engines on the biased coins (left) and dice (right) examples. In both graphs, the values on the x-axis represent the parameters of the given model, and the values on the y-axis represent the running times (in \({\hbox {log}}_{{10}}\) scale). The configuration options for RationalSearch, PRISM Exact and STORM exact identical to those in Table 2. PRISM approx was invoked using the same base options as RationalSearch. No data point is given for PRISM Exact with parameter six on the dice example as a 30-min timeout was reached
Comparison of iterative techniques. The final goal of our evaluation was to determine which approximation technique, amongst value iteration and interval iteration, could be more effectively integrated with Algorithm 3. In particular, we compared the two approaches for speed and the quality of their approximations. The results are given in Table 3. We integrated RationalSearch with the implementation of interval iteration in PRISM from prior work [11], available at [1].
To our surprise, we found that the interval iteration implementation from [1] did not always produce an approximate solution within the specified \(\epsilon \) threshold. In particular, for the dice example under parameter six, the approximations for both \(\epsilon =10^{-6}\) and \(\epsilon =10^{-12}\) were not within the given threshold. This resulted in RationalSearch not being able to infer an exact solution. Several other examples also suffered from this symptom. Although the approximate probabilities for the initial states were precise enough, poor approximations for the other states in the solution vector prevented RationalSearch from finding an exact solution.
The accuracy and precision of solution produced by approximation techniques varied according to the \(\epsilon \) threshold and the iterative technique used. Although we have not reported the numbers in Table 3, there are also examples for which the approximations for value (interval) iteration differ across the solution engines (for the same value of \(\epsilon \)). In spite of the difference in the approximations, RationalSearch is able to infer an exact solution for all of these different approximations.
In terms of speed, we observed only a small variance in the performance of the two techniques on the benchmarks we used. In most cases, value iteration slightly outperformed interval iteration. The difference is primarily a result of the extra cost incurred by interval iteration to perform the additional pre-processing steps it requires. This cost outweighs the savings afforded by the version of sharpen used with interval iteration that requires only a single fixpoint. In addition, our benchmarks did not identify any examples for which the improved precision of interval iteration allowed RationalSearch to infer an exact solution where value iteration could not. The preceding observations, in conjunction, lead us to conclude value iteration is the more effective partner for Algorithm 3.
8 Conclusion
Techniques for exact model checking allow one to avoid logical errors in system analysis that can arise due to approximation techniques. We presented an algorithm and tool, RationalSearch, that computes the exact probabilities described by PCTL formulas for DTMCs and MDPs. Our tool works by sharpening approximate results obtained through value iteration, allowing it to benefit from the performance enhancements gained through approximation techniques. Our experimental evaluation concurs with this hypothesis, and shows that our approach often performs significantly better than existing exact quantitative model checking tools while also scaling to large model sizes. We believe there are also performance enhancements that can be achieved by a tighter integration with the Kwek–Mehlhorn algorithm, wherein computations from previous iterations can be reused.
Notes
One can alternatively define a scheduler as a function from finite paths into probability distributions on actions. Both definitions are equivalent in the context of PCTL model checking.
Using the Hybrid engine, the absolute convergence criterion and \(\epsilon =10^{-16}\).
Information about the implementation of Algorithm 3 in STORM was obtained through private email conversations with the developers.
References
(2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/CAV17/
(2017) PRISM benchmark suite,http://www.prismmodelchecker.org/benchmarks/. Accessed 5 May 2020
(2017) PRISM case studies, http://www.prismmodelchecker.org/casestudies/. Accessed 5 May 2020
(2019) Apfloat. http://www.apfloat.org/
(2019) CUDD. http://vlsi.colorado.edu/~fabio/CUDD/html/
(2019) GNU multiple precision arithmetic library. https://gmplib.org/
(2019) JScience. http://jscience.org/
(2019) RationalSearch. https://publish.illinois.edu/rationalmodelchecker/
de Alfaro L (1997) Formal verification of probabilistic systems. Ph.D. thesis, Stanford University
Baier C, Katoen JP (2008) Principles of model checking (representation and mind series). The MIT Press, Cambridge
Baier C, Klein J, Leuschner L, Parker D, Wunderlich S (2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Computer aided verification
Banach S (1922) Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales. Fundamenta Mathematicae 3(1):133–181
Bauer MS, Mathur U, Chadha R, Sistla AP, Viswanathan M (2017) Exact quantitative probabilistic model checking through rational search. In: Proceedings of the 17th conference on formal methods in computer-aided design, FMCAD Inc, Austin, TX, FMCAD ’17, pp 92–99. https://doi.org/10.23919/FMCAD.2017.8102246. http://dl.acm.org/citation.cfm?id=3168451.3168475
Benini L, Bogliolo A, Paleologo GA, De Micheli G (1999) Policy optimization for dynamic power management. IEEE Trans Comput-Aided Des Integr Circuits Syst 13:813–833
Bhaduri D, Shukla SK, Graham PS, Gokhale MB (2007) Reliability analysis of large circuits using scalable techniques and tools. IEEE Trans Circuits Syst I: Regul Pap 54:2447–2460
Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: 15th Conference foundations of software technology and theoretical computer science, lecture notes in computer science. Springer, Berlin, vol 1026, pp 499–513
Brázdil T, Chatterjee K, Chmelík M, Forejt V, Křetínský J, Kwiatkowska M, Parker D, Ujma M (2014) Verification of markov decision processes using learning algorithms. In: Automated technology for verification and analysis. Springer, Cham, pp 98–114
Bryant RE (1986) Graph-based algorithms for boolean function manipulation. EEE Trans Comput 100(8):677–691
Chatterjee K, Henzinger TA (2008) Value iteration. Springer, Berlin, pp 107–138. https://doi.org/10.1007/978-3-540-69850-0_7
Chaum D (1988) The dining cryptographers problem: Unconditional sender and recipient untraceability. J Cryptol 1(1):65–75
Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: International Colloquium on theoretical aspects of computing. Springer, Berlin, pp 280–294
Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: 29th international conference computer aided verification CAV 2017
Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, Katoen JP, Abraham E (2015) Prophesy: a probabilistic parameter synthesis tool. In: International conference on computer aided verification, CAV
van Dijk T, van de Pol J (2015) Sylvan: Multi-core decision diagrams. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 677–691
Dijkstra EW (1982) Self-stabilization in spite of distributed control. In: Selected writings on computing: a personal perspective. Springer, Berlin
Duflot M, Kwiatkowska M, Norman G, Parker D (2006) A formal analysis of bluetooth device discovery. Int J Softw Tools Technol Transf (STTT) 8(6):621–632
Forejt V, Kwiatkowska M, Norman G, Parker D (2011a) Automated verification techniques for probabilistic systems. In: International school on formal methods for the design of computer, communication and software systems. Springer, Berlin, pp 53–113
Forejt V, Kwiatkowska MZ, Norman G, Parker D (2011b) Automated verification techniques for probabilistic systems. In: Formal methods for eternal networked software systems—11th international school on formal methods for the design of computer, communication and software systems, SFM, pp 53–113
Fujita M, McGeer PC, Yang JY (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst Des 10(2–3):149–169
Giro S (2012) Efficient computation of exact solutions for quantitative model checking. In: Proceedings of 10th workshop on quantitative aspects of programming languages (QAPL’12)
Haddad S, Monmege B (2014) Reachability in MDPS: refining convergence of value iteration. In: International workshop on reachability problems. Springer, Berlin, pp 125–137
Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PARAM: a model checker for parametric Markov models. In: International conference on computer aided verification (CAV’10)
Hahn EM, Han T, Zhang L (2011a) Synthesis for PCTL in parametric Markov decision processes. In: NASA formal methods symposium. Springer, Berlin, pp 146–161
Hahn EM, Hermanns H, Zhang L (2011b) Probabilistic reachability for parametric Markov models. Int J Softw Tools Technol Transf 13(1):3–19
Han J, Chen H, Boykin E, Fortes J (2011) Reliability evaluation of logic circuits using probabilistic gate models. Microelectron Reliab 51:468–476
Hoey J, St-Aubin R, Hu A, Boutilier C (1999) Spudd: Stochastic planning using decision diagrams. In: Proceedings of the fifteenth conference on uncertainty in artificial intelligence
Hopcroft JE (2008) Introduction to automata theory, languages, and computation. Pearson Education India, Delhi
Jeannet B, D’Argenio P, Larsen K (2002) Rapture: a tool for verifying Markov decision processes. In: Proceeding of tools day, affiliated to 13th international conference concurrency theory (CONCUR’02)
Katoen JP, Khattri M, Zapreevt I (2005) A Markov reward model checker. In: Second international conference on the quantitative evaluation of systems (QEST’05), IEEE
Kwek S, Mehlhorn K (2003) Optimal search for rationals. Inf Process Lett 86(1):23–26
Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proceedings of 2nd joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM/PROBMIV’02)
Kwiatkowska M, Norman G, Sproston J (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects Comput 14(3):295–318
Kwiatkowska M, Norman G, Parker D (2004) Controller dependability analysis by probabilistic model checking. In: 11th IFAC symposium on information control problems in manufacturing (INCOM’04)
Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: International conference on computer aided verification. Springer, Berlin, pp 585–591
McMillan KL (1993) Symbolic model checking. Kluwer Academic Publishers, Norwell
Mohyuddin N, Pakbaznia E, Pedram M (2011) Probabilistic error propagation in a logic circuit using the Boolean difference calculus. In: Advanced techniques in logic synthesis, optimizations and applications. Springer, Berlin, pp 359–381
Norman G, Parker D, Kwiatkowska M, Shukla S (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans Comput-Aided Des Integr Circuits Syst 24:1629–1637
Parker D (2002) Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham
Qiu Q, Qu Q, Pedram M (2001) Stochastic modeling of a power-managed system-construction and optimization. IEEE Trans Comput-Aided Des Integr Circuits Syst 20:1200–1217
Rabin M (1983) Randomized Byzantine generals. In: Proceedings of symposium on foundations of computer science, pp 403–409
Rutten J, Kwiatkowska M, Norman G, Parker D (2004a) Mathematical techniques for analyzing concurrent and probabilistic systems. In: Panangaden P, van Breugel F (eds) CRM monograph series, vol 23. American Mathematical Society, Providence
Rutten JJ, Kwiatkowska M, Norman G, Parker D (2004b) Mathematical techniques for analyzing concurrent and probabilistic systems. American Mathematical Society, Providence
St-Aubin R, Hoey J, Boutilier C (2001) APRICODD: approximate policy construction using decision diagrams. In: Advances in neural information processing systems, pp 1089–1095
Wimmer R, Kortus A, Herbstritt M, Becker B (2008) Probabilistic model checking and reliability of results. In: 11th IEEE workshop on design and diagnostics of electronic circuits and systems, 2008. DDECS, IEEE, pp 1–6
Acknowledgements
We thank the anonymous reviewers for their useful comments. In particular, we would like to thank the reviewer who pointed out that it is insufficient to check that a proposed solution was a solution to a system of linear equations when computing max reachability probabilities and min expected costs.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
We gratefully acknowledge the support of the following Grants—Umang Mathur was partially supported by a Google PhD Fellowship; Rohit Chadha was partially supported by NSF CNS-1553548 and NSF CCF-1900924; A. Prasad Sistla was partially supported by NSF CNS-1314485, NSF CCF-1319754, NSF CCF-1564296 and NSF CCF-1901069; and Mahesh Viswanathan was partially supported by NSF CCF-1901069.
Proof of the claim in Theorem 2
Proof of the claim in Theorem 2
It can be shown easily that f is non-expanding, i.e, for any \({{{\bar{x}}}}_1,{{\bar{x}}_2}\in {\mathcal {U}}\),
We will assume without loss of generality that \({\mathsf {Prob}}^{{\mathsf {min}}}_{1}[\xi ]\) consists of exactly one element \(z_0.\) Further, we assume that \({\mathsf {Prob}}^{{\mathsf {min}}}_{0}[\xi ]\) consists of at least 1 element as otherwise the claim is trivially true.
Let \(Z^?= Z{\setminus } ( {\mathsf {Prob}}^{{\mathsf {min}}}_{0}[\xi ] \,\cup \,{\mathsf {Prob}}^{{\mathsf {min}}}_{1}[\xi ]).\) For \({{\bar{x}}} \in {\mathcal {U}}, z\in Z^?\) and \(\alpha \in {\mathsf {enabled}}(z),\) we denote the sum \(\displaystyle \sum _{z'\in Z} {\varDelta }(z,\alpha ,z') \cdot {\bar{x}}(z')\) by \(h_{{{\bar{x}}},z,\alpha }.\) By definition
Fix \({\bar{x}},{\bar{y}}\in {\mathcal {U}}.\) The definition of \(Z^?\) implies that for any scheduler \({\mathfrak {S}},\) the probability of reaching \(z_0\) from a state \(z\in Z^?\) is not zero. From this, there it follows that there is an enumeration \(z_1,z_2,\ldots z_r\) of \(Z^?\) such that for any \(1\le i \le r\) and any action \(\alpha \in {\mathsf {enabled}}(z_i),\) \( {\varDelta }(z_i,\alpha ,z_j) >0 \) for some \(0\le j<i.\)
We will show by induction on \(0 \le i\le r,\)
Observe that this suffices to conclude the claim since this implies for any \(z_i\in Z^?,\)
Now we show, by induction, that for each \(0 \le i\le r,\) \(|f^{i+1}({{\bar{x}}}) (z_i)- f^{i+1}({\bar{y}}) (z_i)| \le (1-p^i_{\mathsf {min}}) || {\bar{x}} -{\bar{y}}||. \)
Base case: The base case is trivial since \(f({\bar{x}}) (z_0) = 1 = f({\bar{y}}) (z_0).\)
Induction hypothesis: Let \(|f^{i+1}({\bar{x}}) (z_i)- f^{i+1}({\bar{y}}) (z_i)| \le (1-p^i_{\mathsf {min}}) || {\bar{x}} -{\bar{y}}|| \) for each \(0\le i \le \ell .\) Fix \(\beta \in {\mathsf {enabled}}(z_{\ell +1}).\) Denote the set \(\{ z_0,z_1,\ldots ,z_\ell \}\) by \(Z_\ell .\) We have that
Now, note that \((1-p^i_{\mathsf {min}})\le (1-p^\ell _{\mathsf {min}}) \) for each \(i\le \ell .\) Thus, we get by induction hypothesis,
As f is non-expanding, we get that
By construction, \(\sum _{z'\in Z_\ell } {\varDelta }(z_{\ell +1},\beta ,z')) \ge p_{\mathsf {min}}\) and hence
Now, we have that
As \(\beta \) is arbitrary, the above inequality also holds for the \(\beta \) that minimizes \(h_{f^{\ell +2}({\bar{y}}),z_{\ell +1},\beta }.\) Hence,
Similarly, we can show that
Thus, we get
as required.
Rights and permissions
About this article
Cite this article
Mathur, U., Bauer, M.S., Chadha, R. et al. Exact quantitative probabilistic model checking through rational search. Form Methods Syst Des 56, 90–126 (2020). https://doi.org/10.1007/s10703-020-00348-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-020-00348-y