Reachability in Parametric Interval Markov Chains using Constraints

TL;DR

This paper introduces a formalism called parametric Interval Markov Chains (pIMCs) that incorporate parameterized probability intervals, analyzes their semantics, and develops constraint-based methods for parameter synthesis, supported by a prototype implementation.

Contribution

It extends Markov Chain models with parametric probability intervals, compares semantics, and provides constraint-based solutions for reachability and consistency problems.

Findings

Semantics for IMCs are shown to agree on reachability probabilities.

Constraint encodings effectively solve parameter synthesis problems.

Prototype implementation demonstrates promising results.

Abstract

Parametric Interval Markov Chains (pIMCs) are a specification formalism that extend Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labeled with parametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate the two usual semantics for IMCs: once-and-for-all and at-every-step. In particular, we prove that both semantics agree on the maximal/minimal reachability probabilities of a given IMC. We then investigate solutions to several parameter synthesis problems in the context of pIMCs -- consistency, qualitative reachability and quantitative reachability -- that rely on constraint encodings. Finally, we propose a prototype implementation of our constraint encodings with promising results.

Tables

Table 1. Table 1: Benchmarks

		pIMC			${𝐂}_{\exists 𝐜}$			${𝐂}_{\exists 𝐫}$			${𝐂}_{\exists \overline{𝐫}}$
Benchmark		#states	#trans.	#par.	#var.	#cstr.	time	#var.	#cstr.	time	#var.	#cstr.	time
nand	K=1; N=2	104	147	4	255	1,526	0.17s	170	1,497	0.19s	296	2,457	69.57s
nand	K=1; N=3	252	364	5	621	3,727	0.24s	406	3,557	0.30s	703	5,828	31.69s
nand	K=1; N=5	930	1,371	7	2,308	13,859	0.57s	1,378	12,305	0.51s	2,404	20,165	T.O.
nand	K=1; N=10	7,392	11,207	12	18,611	111,366	9.46s	9,978	89,705	13.44s	17,454	147,015	T.O.

Equations

$$\sum _{t^{\prime }\mathcal{R}{s}^{\prime }}{p}^{\prime }(u_t^s)(u_{t^{\prime }}^{s^{\prime }})=\sum _{t^{\prime }\mathcal{R}{s}^{\prime }}p(t)(t^{\prime })\times {\delta }_t^s(t^{\prime })(s^{\prime })$$

$$=$$

$$p^{\prime }(u_t^s)(B\cap U)$$

$$=\sum _{\{s^{\prime }\in S\mid s^{\prime }\mathcal{R}{t}^{\prime }\}}p(t)(t^{\prime })\times {\delta }_t^s(t^{\prime })(s^{\prime })=p(t)(t^{\prime })\times \sum _{\{s^{\prime }\in S\mid s^{\prime }\mathcal{R}{t}^{\prime }\}}{\delta }_t^s(t^{\prime })(s^{\prime })$$

$$=p(t)(t^{\prime })\times 1=p(t)(\{t^{\prime }\})=p(t)(B\cap T)$$

$$\sum _{t^{\prime }\in T^{\prime }}{p}^{\prime }(t)(t^{\prime })=$$

$$\stackrel{(1)}{=}$$

$$=$$

$$\sum _{s^{\prime }\in S}{\delta }^{\prime }(\bar{t})(s^{\prime })=$$

$$=$$

$$\stackrel{(1)}{=}$$

$$\stackrel{(2)}{=}$$

$$\sum _{t^{\prime }\in T^{\prime }}{p}^{\prime }(t)(t^{\prime })\times {\delta }^{\prime }(t^{\prime })(s^{\prime })$$

$$=$$

$$\stackrel{(1)}{=}$$

$$\stackrel{(2)}{=}$$

$$\stackrel{(3)}{=}$$

$$=$$

$$\stackrel{(4)}{\in }$$

$${\mathbb{P}}_{\bar{t}}^{{\mathcal{M}}^{\prime }}(◊\alpha )$$

$$\stackrel{(1)}{=}$$

$$\stackrel{(2)}{=}$$

$$\stackrel{(3)}{=}$$

$$\stackrel{(4)}{=}$$

$$\stackrel{(5)}{\le }$$

$$\stackrel{(6)}{=}$$

$$\stackrel{(7)}{=}$$

$$=$$

$${\mathbb{P}}_s^{\mathcal{M}}(◊\alpha )=\frac{{\mathbb{P}}_s^{\mathcal{M}}(\neg s\text{ U }\alpha )}{1-{\mathbb{P}}_s^{\mathcal{M}}(\neg \alpha \text{ U }s)}$$

$$\text{(a) }{\mathbb{P}}_s^{\mathcal{M}}({\Omega }_n\times S^{\prime })$$

$$={\mathbb{P}}_s^{\mathcal{M}}({\Omega }_1\times \{s\})\times {\mathbb{P}}_s^{\mathcal{M}}({\Omega }_{n-1}\times S^{\prime })$$

$$={\mathbb{P}}_s^{\mathcal{M}}(\neg \alpha \text{ U }s)\times {\mathbb{P}}_s^{\mathcal{M}}({\Omega }_{n-1}\times S^{\prime })$$

$$\text{(b) }{\mathbb{P}}_s^{\mathcal{M}}(◊\alpha )$$

$$=\frac{{\mathbb{P}}_s^{\mathcal{M}}({\Omega }_1\times S^{\prime })}{1-{\mathbb{P}}_s^{\mathcal{M}}(\neg \alpha \text{ U }s)}$$

$$=\frac{{\mathbb{P}}_s^{\mathcal{M}}(\neg s\text{ U }\alpha )}{1-{\mathbb{P}}_s^{\mathcal{M}}(\neg \alpha \text{ U }s)}$$

Full text

1 Introduction

Discrete time Markov chains (MCs for short) are a standard probabilistic modeling formalism that has been extensively used in the litterature to reason about software [18] and real-life systems [12]. However, when modeling real-life systems, the exact value of transition probabilities may not be known precisely. Several formalisms abstracting MCs have therefore been developed. Parametric Markov chains [1] (pMCs for short) extend MCs by allowing parameters to appear in transition probabilities. In this formalism, parameters are variables and transition probabilities may be expressed as polynomials over these variables. A given pMC therefore represents a potentially infinite set of MCs, obtained by replacing each parameter by a given value. pMCs are particularly useful to represent systems where dependencies between transition probabilities are required. Indeed, a given parameter may appear in several dinstinct transition probabilities, therefore requiring that the same value is given to all its occurences. Interval Markov chains [13] (IMC for short) extend MCs by allowing precise transition probabilities to be replaced by intervals, but cannot represent dependencies between distinct transitions. IMCs have mainly been studied with two distinct semantics interpretation. Under the once-and-for-all semantics, a given IMC represents a potentially infinite number of MCs where transition probabilities are chosen inside the specified intervals while keeping the same underlying graph structure. The at-every-step semantics, which was the original semantics given to IMCs in [13], does not require MCs to preserve the underlying graph structure of the original IMC but instead allows an “unfolding” of the original graph structure where different probability values may be chosen (inside the specified interval) at each occurence of the given transition.

Model-checking algorithms and tools have been developed in the context of pMCs [7, 11, 14] and IMCs with the once-and-for-all semantics [10, 4]. State of the art tools [7] for pMC verification compute a rational function on the parameters that characterizes the probability of satisfying a given property, and then use external tools such as SMT solving [7] for computing the satisfying parameter values. For these methods to be viable in practice, the number of parameters used is quite limited. On the other hand, the model-checking procedure for IMCs presented in [4] is adapted from machine learning and builds successive refinements of the original IMCs that optimize the probability of satisfying the given property. This algorithm converges, but not necessarilly to a global optimum. It is worth noticing that existing model checking procedures for pMCs and IMCs strongly rely on their underlying graph structure. As a consequence, to the best of our knowledge, no solutions for model-checking IMCs with the at-every-step semantics have been proposed yet.

In this paper, we focus on Parametric interval Markov chains [9] (pIMCs for short), that generalize both IMCs and pMCs by allowing parameters to appear in the endpoints of the intervals specifying transition probabilities, and we provide four main contributions.

First, we formally compare abstraction formalisms for MCs in terms of succinctness: we show in particular that pIMCs are strictly more succinct than both pMCs and pIMCs when equipped with the right semantics. In other words, everything that can be expressed using pMCs or IMCs can also be expressed using pIMCs while the reverse does not hold. Second, we prove that the once-and-for-all and the at-every-step semantics are equivalent w.r.t. rechability properties, both in the IMC and in the pIMC settings. Notably, this result gives theoretical backing to the generalization of existing works on the verification of IMCs to the at-every-step semantics. Third, we study the parametric verification of fundamental properties at the pIMC level: consistency, qualitative reachability, and quantitative reachability. Given the expressivity of the pIMC formalism, the risk of producing a pIMC specification that is incoherent and therefore does not model any concrete MC is high. We therefore propose constraint encodings for deciding whether a given pIMC is consistent and, if so, synthesizing parameter values ensuring consistency. We then extend these encodings to qualitative reachability, i.e., ensuring that given state labels are reachable in all (resp. none) of the MCs modeled by a given pIMC. Finally, we focus on the quantitative reachability problem, i.e., synthesizing parameter values such that the probability of reaching given state labels satisfies fixed bounds in at least one (resp. all) MCs modeled by a given pIMC. While consistency and qualitative reachability for pIMCs have already been studied in [9], the constraint encodings we propose in this paper are significantly smaller (linear instead of exponential). To the best of our knowledge, our results provide the first solution to the quantitative reachability problem for pIMCs. Our last contribution is the implementation of all our verification algorithms in a prototype tool that generates the required constraint encodings and can be plugged to any SMT solver for their resolution. Due to space limitation, the proofs of our results are given in Appendix.

2 Background

In this section we introduce notions and notations that will be used throughout the paper. Given a finite set of variables $X=\{x_{1},\ldots,x_{k}\}$, we write $D_{x}$ for the domain of the variable $x\in X$ and $D_{X}$ for the set of domains associated to the variables in $X$. A valuation $v$ over $X$ is a set $v=\{(x,d)|x\in X,d\in D_{x}\}$ of elementary valuations $(x,d)$ where for each $x\in X$ there exists a unique pair of the form $(x,d)$ in $v$. When clear from the context, we write $v(x)=d$ for the value given to variable $x$ according to valuation $v$. A rational function $f$ over $X$ is a division of two (multivariate) polynomials $g_{1}$ and $g_{2}$ over $X$ with rational coefficients, i.e., $f=g_{1}/g_{2}$. We write ${\mathbb{Q}}$ the set of rational numbers and ${\mathbb{Q}}_{X}$ the set of rational functions over $X$. The evaluation $v(g)$ of a polynomial $g$ under the valuation $v$ replaces each variable $x\in X$ by its value $v(x)$.

An atomic constraint over $X$ is a Boolean expression of the form $f(X)\bowtie g(X)$, with ${\bowtie}\in\{\leq,\geq,<,>,=\}$ and $f$ and $g$ two functions over variables in $X$ and constants. A constraint is linear if the functions $f$ and $g$ are linear. A constraint over $X$ is a Boolean combination of atomic constraints over $X$.

Given a finite set of states $S$, we write $\mathsf{Dist}(S)$ for the set of probability distributions over $S$, i.e., the set of functions $\mu:S\to[0,1]$ such that $\sum_{s\in S}\mu(s)=1$. We write ${\mathbb{I}}$ for the set containing all the interval subsets of $[0,1]$. In the following, we consider a universal set of symbols $A$ that we use for labelling the states of our structures. We call these symbols atomic propositions. We will use Latin alphabet in state context and Greek alphabet in atomic proposition context.

Constraints. Constraints are first order logic predicates used to model and solve combinatorial problems [17]. A problem is described with a list of variables, each in a given domain of possible values, together with a list of constraints over these variables. Such problems are then sent to solvers which decide whether the problem is satisfiable, i.e., if there exists a valuation of the variables satisfying all the constraints, and in this case computes a solution. Checking satisfiability of constraint problems is difficult in general, as the space of all possible valuations has a size exponential in the number of variables.

Formally, a Constraint Satisfaction Problem (CSP) is a tuple $\Omega=(X,D,C)$ where $X$ is a finite set of variables, $D=D_{X}$ is the set of all the domains associated to the variables from $X$, and $C$ is a set of constraints over $X$. We say that a valuation over $X$ satisfies $\Omega$ if and only if it satisfies all the constraints in $C$. We write $v(C)$ for the satisfaction result of the valuation of the constraints $C$ according to $v$ (i.e., true or false). In the following we call CSP* encoding* a scheme for formulating a given problem into a CSP. The size of a CSP corresponds to the number of variables and atomic constraints appearing in the problem. Note that, in constraint programming, having less variables or less constraints during the encoding does not necessarily imply faster solving time of the problems.

Discrete Time Markov Chains. A Discrete Time Markov Chain (DTMC or MC for short) is a tuple $\mathcal{M}$ $=$ $(S,$ $s_{0},$ $p,$ $V)$, where $S$ is a finite set of states containing the initial state $s_{0}$, $V:S\to 2^{A}$ is a labelling function, and $p:S\rightarrow\mathsf{Dist}(S)$ is a probabilistic transition function. We write $\tt{MC}$ for the set containing all the discrete time Markov chains.

A Markov Chain can be seen as a directed graph where the nodes correspond to the states of the MC and the edges are labelled with the probabilities given by the transition function of the MC. In this representation, a missing transition between two states represents a transition probability of zero. As usual, given a MC $\mathcal{M}$, we call a path of $\mathcal{M}$ a sequence of states obtained from executing $\mathcal{M}$, i.e., a sequence $\omega=s_{1},s_{2},\ldots$ s.t. the probability of taking the transition from $s_{i}$ to $s_{i+1}$ is strictly positive, $p(s_{i})(s_{i}+1)>0$, for all $i$. A path $\omega$ is finite iff it belongs to $S^{*}$, i.e., it represents a finite sequence of transitions from $\mathcal{M}$.

Example 1

Figure 3 illustrates the Markov chain $\mathcal{M}_{1}=(S,s_{0},p,V)\in\tt{MC}$ where the set of states $S$ is given by $\{s_{0},s_{1},s_{2},s_{3},s_{4}\}$, the atomic proposition are restricted to $\{\alpha,\beta\}$, the initial state is $s_{0}$, and the labelling function $V$ corresponds to $\{(s_{0},\emptyset),(s_{1},\alpha),(s_{2},\beta),(s_{3},\{\alpha,\beta\}),(s_{4},\alpha)\}$. The sequences of states $(s_{0},s_{1},s_{2})$, $(s_{0},s_{2})$, and $(s_{0},s_{2},s_{2},s_{2})$, are three (finite) paths from the initial state $s_{0}$ to the state $s_{2}$.

Reachability. A Markov chain $\mathcal{M}$ defines a unique probability measure $\mathbb{P}^{\mathcal{M}}$ over the paths from $\mathcal{M}$. According to this measure, the probability of a finite path $\omega=s_{0},s_{1},\ldots,s_{n}$ in $\mathcal{M}$ is the product of the probabilities of the transitions executed along this path, i.e., $\mathbb{P}^{\mathcal{M}}(\omega)=p(s_{0})(s_{1})\cdot p(s_{1})(s_{2})\cdot\ldots\cdot p(s_{n-1})(s_{n})$. This distribution naturally extends to infinite paths (see [2]) and to sequences of states over $S$ that are not paths of $\mathcal{M}$ by giving them a zero probability.

Given a MC $\mathcal{M}$, the overall probability of reaching a given state $s$ from the initial state $s_{0}$ is called the reachability probability and written $\mathbb{P}^{\mathcal{M}}_{s_{0}}(\Diamond s)$ or $\mathbb{P}^{\mathcal{M}}(\Diamond s)$ when clear from the context. This probability is computed as the sum of the probabilities of all finite paths starting in the initial state and reaching this state for the first time. Formally, let $\mathsf{reach}_{s_{0}}(s)=\{\omega\in S^{*}\ |\ \omega=s_{0},\ldots s_{n}\mbox{ with }s_{n}=s\mbox{ and }s_{i}\neq s\ \forall 0\leq i<n\}$ be the set of such paths. We then define $\mathbb{P}^{\mathcal{M}}(\Diamond s)=\sum_{\omega\in\mathsf{reach}_{s_{0}}(s)}\mathbb{P}^{\mathcal{M}}(\omega)$ if $s\neq s_{0}$ and $1$ otherwise. This notation naturally extends to the reachability probability of a state $s$ from a state $t$ that is not $s_{0}$, written $\mathbb{P}^{\mathcal{M}}_{t}(\Diamond s)$ and to the probability of reaching a label $\alpha\subseteq A$ written $\mathbb{P}^{\mathcal{M}}_{s_{0}}(\Diamond\alpha)$. In the following, we say that a state $s$ (resp. a label $\alpha\subseteq A$) is reachable in $\mathcal{M}$ iff the reachability probability of this state (resp. label) from the initial state is strictly positive.

Example 2 (Example 1 continued)

In Figure 3 the probability of the path $(s_{0},$ $s_{2},$ $s_{1},$ $s_{1},$ $s_{3})$ is $0.3\cdot 0.5\cdot 0.5\cdot 0.5=0.0375$ and the probability of reaching the state $s_{1}$ is $\mathbb{P}^{\mathcal{M}_{1}}(\Diamond s_{1})=p(s_{0})(s_{1})+\Sigma_{i=0}^{+\infty}{p(s_{0})(s_{2}){\cdot}p(s_{2})(s_{2})^{i}{\cdot}p(s_{2})(s_{1})}=p(s_{0})(s_{1})+p(s_{0})(s_{2}){\cdot}p(s_{2})(s_{1}){\cdot}(1/(1-p(s_{2})(s_{2})))=1$. Furthermore, the probability of reaching $\beta$ corresponds to the probability of reaching the state $s_{2}$.

3 Markov Chains Abstractions

Modelling an application as a Markov Chain requires knowing the exact probability for each possible transition of the system. However, this can be difficult to compute or to measure in the case of a real-life application (e.g., precision errors, limited knowledge). In this section, we start with a generic definition of Markov chain abstraction models. Then we recall three abstraction models from the literature, respectively pMC, IMC, and pIMC, and finally we present a comparison of these existing models in terms of succinctness.

Definition 1 (Markov chain Abstraction Model)

A Markov chain abstraction model (an abstraction model for short) is a pair $({\tt L},\models)$ where ${\tt L}$ is a nonempty set and $\models$ is a relation between ${\tt{MC}}$ and ${\tt L}$. Let $\mathcal{P}$ be in ${\tt L}$ and $\mathcal{M}$ be in $\tt{MC}$ we say that $\mathcal{M}$ implements $\mathcal{P}$ iff $(\mathcal{M},\mathcal{P})$ belongs to $\models$ (i.e., $\mathcal{M}\models\mathcal{P}$). When the context is clear, we do not mention the satisfaction relation $\models$ and only use ${\tt L}$ to refer to the abstraction model $({\tt L},\models)$.

A Markov chain Abstraction Model is a specification theory for MCs. It consists in a set of abstract objects, called specifications, each of which representing a (potentially infinite) set of MCs – implementations – together with a satisfaction relation defining the link between implementations and specifications. As an example, consider the powerset of $\tt{MC}$ (i.e., the set containing all the possible sets of Markov chains). Clearly, $(2^{\tt{MC}},\in)$ is a Markov chain abstraction model, which we call the canonical abstraction model. This abstraction model has the advantage of representing all the possible sets of Markov chains but it also has the disadvantage that some Markov chain abstractions are only representable by an infinite extension representation. Indeed, recall that there exists subsets of $[0,1]\subseteq\mathbb{R}$ which cannot be represented in a finite space (e.g., the Cantor set [5]). We now present existing MC abstraction models from the literature.

3.1 Existing MC Abstraction Models

Parametric Markov Chain is a MC abstraction model from [1] where a transition can be annotated by a rational function over parameters. We write $\tt{pMC}$ for the set containing all the parametric Markov chains.

Definition 2 (Parametric Markov Chain)

A Parametric Markov Chain (pMC for short) is a tuple $\mathcal{I}=(S,s_{0},P,V,Y)$ where $S$, $s_{0}$, and $V$ are defined as for MCs, $Y$ is a set of variables (parameters), and $P:S\times S\to\mathbb{Q}_{Y}$ associates with each potential transition a parameterized probability.

Let $\mathcal{M}=(S,s_{0},p,V)$ be a MC and $\mathcal{I}=(S,s_{0},P,V,Y)$ be a pMC. The satisfaction relation $\models_{\tt{p}}$ between $\tt{MC}$ and $\tt{pMC}$ is defined by $\mathcal{M}\models_{\tt{p}}\mathcal{I}$ iff there exists a valuation $v$ of $Y$ s.t. $p(s)(s^{\prime})$ equals $v(P(s,s^{\prime}))$ for all $s,s^{\prime}$ in $S$.

Example 3

Figure 3 shows a pMC $\mathcal{I}^{\prime}=(S,s_{0},P,V,Y)$ where $S$, $s_{0}$, and $V$ are similar to the same entities in the MC $\mathcal{M}$ from Figure 3, the set of variable $Y$ contains only one variable $p$, and the parametric transitions in $P$ are given by the edge labelling (e.g., $P(s_{0},s_{1})=0.7$, $P(s_{1},s_{3})=p$, and $P(s_{2},s_{2})=1-p$). Note that the pMC $\mathcal{I}^{\prime}$ is a specification containing the MC $\mathcal{M}$ from Figure 3.

Interval Markov Chains extend MCs by allowing to label transitions with intervals of possible probabilities instead of precise probabilities. We write $\tt{IMC}$ for the set containing all the interval Markov chains.

Definition 3 (Interval Markov Chain [13])

An Interval Markov Chain (IMC for short) is a tuple $\mathcal{I}=(S,s_{0},P,V)$, where $S$, $s_{0}$, and $V$ are defined as for MCs, and $P:S\times S\to{\mathbb{I}}$ associates with each potential transition an interval of probabilities.

Example 4

Figure 3 illustrates IMC $\mathcal{I}=(S,s_{0},P,V)$ where $S$, $s_{0}$, and $V$ are similar to the MC given in Figure 3. By observing the edge labelling we see that $P(s_{0},s_{1})=[0,1]$, $P(s_{1},s_{1})=[0.5,1]$, and $P(s_{3},s_{3})=[1,1]$. On the other hand, the intervals of probability for missing transitions are reduced to $[0,0]$, e.g., $P(s_{0},s_{0})=[0,0]$, $P(s_{0},s_{3})=[0,0]$, $P(s_{1},s_{4})=[0,0]$.

In the literature, IMCs have been mainly used with two distinct semantics: at-every-step and once-and-for-all. Both semantics are associated with distinct satisfaction relations which we now introduce.

The once-and-for-all IMC semantics ([7, 19, 16]) is alike to the semantics for pMC, as introduced above. The associated satisfaction relation $\models^{o}_{\tt{I}}$ is defined as follows: A MC $\mathcal{M}=(T,t_{0},p,V^{M})$ satisfies an IMC $\mathcal{I}=(S,s_{0},P,V^{I})$ iff $(T,t_{0},V^{M})=(S,s_{0},V^{I})$ and for all reachable state $s$ and all state $s^{\prime}\in S$, $p(s)(s^{\prime})\in P(s,s^{\prime})$. In this sense, we say that MC implementations using the once-and-for-all semantics need to have the same structure as the IMC specification.

On the other hand, the at-every-step IMC semantics, first introduced in [13], operates as a simulation relation based on the transition probabilities and state labels, and therefore allows MC implementations to have a different structure than the IMC specification. The associated satisfaction relation $\models^{a}_{\tt{I}}$ is defined as follows: A MC $\mathcal{M}$ $=$ $(T,t_{0},$ $p,$ $V^{M})$ satisfies an IMC $\mathcal{I}=(S,s_{0},P,V^{I})$ iff there exists a relation $\mathcal{R}\subseteq T\times S$ such that $(t_{0},s)\in\mathcal{R}$ and whenever $(t,s)\in\mathcal{R}$, we have

1. the labels of $s$ and $t$ correspond: $V^{M}(t)=V^{I}(s)$,

2. there exists a correspondence function $\delta:T\to(S\to[0,1])$ s.t.

(a) $\forall t^{\prime}\in T$if $p(t)(t^{\prime})>0$ then $\delta(t^{\prime})$ is a distribution on $S$

(b) $\forall s^{\prime}\in S:(\Sigma_{t^{\prime}\in T}p(t)(t^{\prime})\cdot\delta(t^{\prime})(s^{\prime}))\in P(s,s^{\prime})$, and

(c) $\forall(t^{\prime},s^{\prime})\in T\times S$, if $\delta(t^{\prime})(s^{\prime})>0$, then $(t^{\prime},s^{\prime})\in\mathcal{R}$.

By construction, it is clear that $\models^{a}_{\tt{I}}$ is more general than $\models^{o}_{\tt{I}}$, i.e., that whenever $\mathcal{M}\models^{o}_{\tt{I}}\mathcal{I}$, we also have $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$. The reverse is obviously not true in general, even when the underlying graphs of $\mathcal{M}$ and $\mathcal{I}$ are isomorphic (see Appendix 0.A.1 for details).

Example 5 (Example 4 continued)

Consider the MC $\mathcal{M}_{1}$ with state space $S$ from Figure 3 and the MC $\mathcal{M}_{2}$ with state space $T$ from Figure 5. They both satisfy the IMC $\mathcal{I}$ with state space $S$ given in Figure 3. Furthermore, $\mathcal{M}_{1}$ satisfies $\mathcal{I}$ with the same structure. On the other hand, for the MC $\mathcal{M}_{2}$ given in Figure 5, the state $s_{3}$ from $\mathcal{I}$ has been “split” into two states $t_{3}$ and $t_{3^{\prime}}$ in $\mathcal{M}_{2}$ and the state $t_{1}$ from $\mathcal{M}_{2}$ “aggregates” states $s_{1}$ and $s_{4}$ in $\mathcal{I}$. The relation $\mathcal{R}\subseteq T\times S$ containing the pairs $(t_{0},s_{0})$, $(t_{1},s_{1})$, $(t_{1},s_{4})$, $(t_{2},s_{2})$, $(t_{3},s_{3})$, and $(t_{3^{\prime}},s_{3})$ is a satisfaction relation between $\mathcal{M}_{2}$ and $\mathcal{I}$.

Parametric Interval Markov Chains, as introduced in [9], abstract IMCs by allowing (combinations of) parameters to be used as interval endpoints in IMCs. Under a given parameter valuation the pIMC yields an IMC as introduced above. pIMCs therefore allow the representation, in a compact way and with a finite structure, of a potentially infinite number of IMCs. Note that one parameter can appear in several transitions at once, requiring the associated transition probabilities to depend on one another. Let $Y$ be a finite set of parameters and $v$ be a valuation over $Y$. By combining notations used for IMCs and pMCs the set ${\mathbb{I}}(\mathbb{Q}_{Y})$ contains all parametrized intervals over $[0,1]$, and for all $I=[f_{1},f_{2}]\in{\mathbb{I}}(\mathbb{Q}_{Y})$, $v(I)$ denotes the interval $[v(f_{1}),v(f_{2})]$ if $0\leq v(f_{1})\leq v(f_{2})\leq 1$ and the empty set otherwise111Indeed, when $0\leq v(f_{1})\leq v(f_{2})\leq 1$ is not respected, the interval is inconsistent and therefore empty.. We write $\tt{pIMC}$ for the set containing all the parametric interval Markov chains.

Definition 4 (Parametric Interval Markov Chain [9])

A Parametric Interval Markov Chain (pIMC for short) is a tuple $\mathcal{P}=(S,s_{0},P,V,Y)$, where $S$, $s_{0}$, $V$ and $Y$ are defined as for pMCs, and $P:S\times S\to{\mathbb{I}}(\mathbb{Q}_{Y})$ associates with each potential transition a (parametric) interval.

In [9] the authors introduced pIMCs where parametric interval endpoints are limited to linear combination of parameters. In this paper we extend the pIMC model by allowing rational functions over parameters as endpoints of parametric intervals. Given a pIMC $\mathcal{P}=(S,s_{0},P,V,Y)$ and a valuation $v$, we write $v(\mathcal{P})$ for the IMC $(S,s_{0},P_{v},V)$ obtained by replacing the transition function $P$ from $\mathcal{P}$ with the function $P_{v}:S\times S\to{\mathbb{I}}$ defined by $P_{v}(s,s^{\prime})=v(P(s,s^{\prime}))$ for all $s,s^{\prime}\in S$. The IMC $v(\mathcal{P})$ is called an instance of pIMC $\mathcal{P}$. Finally, depending on the semantics chosen for IMCs, two satisfaction relations can be defined between MCs and pIMCs. They are written $\models^{a}_{\tt{pI}}$ and $\models^{o}_{\tt{pI}}$ and defined as follows: $\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$ (resp. $\models^{o}_{\tt{pI}}$) iff there exists an IMC $\mathcal{I}$ instance of $\mathcal{P}$ s.t. $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$ (resp. $\models^{o}_{\tt{I}}$).

Example 6

Consider the pIMC $\mathcal{P}=(S,$0$,P,V,Y)$ given in Figure 5. The set of states $S$ and the labelling function are the same as in the MC and the IMC presented in Figures 3 and 3 respectively. The set of parameters $Y$ has two elements $p$ and $q$. Finally, the parametric intervals from the transition function $P$ are given by the edge labelling (e.g., $P(s_{1},s_{3})=[0.3,q]$, $P(s_{2},s_{4})=[0,0.5]$, and $P(s_{3},s_{3})=[1,1]$). Note that the IMC $\mathcal{I}$ from Figure 3 is an instance of $\mathcal{P}$ (by assigning the value $0.6$ to the parameter $p$ and $0.5$ to $q$). Furthermore, as said in Example 5, the Markov Chains $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ (from Figures 3 and 5 respectively) satisfy $\mathcal{I}$, therefore $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ satisfy $\mathcal{P}$.

In the following, we consider that the size of a pMC, IMC, or pIMC corresponds to its number of states plus its number of transitions not reduced to [math], $[0,0]$ or $\emptyset$. We will also often need to consider the predecessors (${\tt{Pred}}$), and the successors (${\tt{Succ}}$) of some given states. Given a pIMC with a set of states $S$, a state $s$ in $S$, and a subset $S^{\prime}$ of $S$, we write:

• •

${\tt{Pred}}(s)=\{s^{\prime}\in S\mid P(s^{\prime},s)\notin\{\emptyset,[0,0]\}\}$

• •

${\tt{Succ}}(s)=\{s^{\prime}\in S\mid P(s,s^{\prime})\notin\{\emptyset,[0,0]\}\}$

• •

${\tt{Pred}}(S^{\prime})=\bigcup_{s^{\prime}\in S^{\prime}}{\tt{Pred}}(s^{\prime})$

• •

${\tt{Succ}}(S^{\prime})=\bigcup_{s^{\prime}\in S^{\prime}}{\tt{Succ}}(s^{\prime})$

3.2 Abstraction Model Comparisons

IMC, pMC, and pIMC are three Markov chain Abstraction Models. In order to compare their expressiveness and compactness, we introduce the comparison operators $\sqsubseteq$ and $\equiv$. Let $({\tt L}_{1},\models_{1})$ and $({\tt L}_{2},\models_{2}\nobreak)$ be two Markov chain abstraction models containing respectively $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$. We say that $\mathcal{L}_{1}$ is entailed by $\mathcal{L}_{2}$, written $\mathcal{L}_{1}\sqsubseteq\mathcal{L}_{2}$, iff all the MCs satisfying $\mathcal{L}_{1}$ satisfy $\mathcal{L}_{2}$ modulo bisimilarity. (i.e., $\forall\mathcal{M}\models_{1}\mathcal{L}_{1},\exists\mathcal{M}^{\prime}\models_{2}\mathcal{L}_{2}$ s.t. $\mathcal{M}$ is bisimilar to $\mathcal{M}^{\prime}$). We say that $\mathcal{L}_{1}$ is (semantically) equivalent to $\mathcal{L}_{2}$, written $\mathcal{L}_{1}\equiv\mathcal{L}_{2}$, iff $\mathcal{L}_{1}\sqsubseteq\mathcal{L}_{2}$ and $\mathcal{L}_{2}\sqsubseteq\mathcal{L}_{1}$. Definition 5 introduces succinctness based on the sizes of the abstractions.

Definition 5 (Succinctness)

Let $({\tt L}_{1},\models_{1})$ and $({\tt L}_{2},\models_{2})$ be two Markov chain abstraction models. ${\tt L}_{1}$ is at least as succinct as ${\tt L}_{2}$, written ${\tt L}_{1}\leq{\tt L}_{2}$, iff there exists a polynomial $p$ such that for every $\mathcal{L}_{2}\in{\tt L}_{2}$, there exists $\mathcal{L}_{1}\in{\tt L}_{1}$ s.t. $\mathcal{L}_{1}\equiv\mathcal{L}_{2}$ and $|\mathcal{L}_{1}|\leq p(|\mathcal{L}_{2}|)$.222 $|\mathcal{L}_{1}|$ and $|\mathcal{L}_{2}|$ are the sizes of $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, respectively. Thus, ${\tt L}_{1}$ is strictly more succinct than ${\tt L}_{2}$, written ${\tt L}_{1}<{\tt L}_{2}$, iff ${\tt L}_{1}\leq{\tt L}_{2}$ and ${\tt L}_{2}\not\leq{\tt L}_{1}$.

We start with a comparison of the succinctness of the pMC and IMC abstractions. Since pMCs allow the expression of dependencies between the probabilities assigned to distinct transitions while IMCs allow all transitions to be independant, it is clear that there are pMCs without any equivalent IMCs (regardless of the IMC semantics used), therefore $(\tt{IMC},\models^{o}_{\tt{I}})\not\leq\tt{pMC}$ and $(\tt{IMC},\models^{a}_{\tt{I}})\not\leq\tt{pMC}$. On the other hand, IMCs imply that transition probabilities need to satisfy linear inequalities in order to fit given intervals. However, these types of constraints are not allowed in pMCs. It is therefore easy to exhibit IMCs that, regardless of the semantics considered, do not have any equivalent pMC specification. As a consequence, $\tt{pMC}\not\leq(\tt{IMC},\models^{o}_{\tt{I}})$ and $\tt{pMC}\not\leq(\tt{IMC},\models^{a}_{\tt{I}})$.

We now compare pMCs and IMCs to pIMCs. Recall that the $\tt{pIMC}$ model is a Markov chain abstraction model allowing to declare parametric interval transitions, while the $\tt{pMC}$ model allows only parametric transitions (without intervals), and the $\tt{IMC}$ model allows interval transitions without parameters. Clearly, any pMC and any IMC can be translated into a pIMC with the right semantics (once-and-for-all for pMCs and the chosen IMC semantics for IMCs). This means that $({\tt{pIMC}},\models^{o}_{\tt{pI}})$ is more succinct than $\tt{pMC}$ and $\tt{pIMC}$ is more succinct than $\tt{IMC}$ for both semantics. Furthermore, since $\tt{pMC}$ and $\tt{IMC}$ are not comparable due to the above results, we have that the $\tt{pIMC}$ abstraction model is strictly more succinct than the $\tt{pMC}$ abstraction model and than the $\tt{IMC}$ abstraction model with the right semantics. Our comparison results are presented in Proposition 1. Further explanations and examples are given in Appendix 0.A.2.

Proposition 1

The Markov chain abstraction models can be ordered as follows w.r.t. succinctness: $({\tt{pIMC}},\models^{o}_{\tt{pI}})<(\tt{pMC},\models_{\tt{p}})$, $({\tt{pIMC}},\models^{o}_{\tt{pI}})<(\tt{IMC},\models^{o}_{\tt{I}})$ and $({\tt{pIMC}},\models^{a}_{\tt{pI}}\nobreak)<(\tt{IMC},\models^{a}_{\tt{I}})$.

Note that $(\tt{pMC},\models_{\tt{p}})\leq(\tt{IMC},\models^{o}_{\tt{I}})$ could be achieved by adding unary constraints on the parameters of a pMC, which is not allowed here. However, this would not have any impact on our other results.

4 Qualitative Properties

As seen above, pIMCs are a succinct abstraction formalism for MCs. The aim of this section is to investigate qualitative properties for pIMCs, i.e., properties that can be evaluated at the specification (pIMC) level, but that entail properties on its MC implementations. pIMC specifications are very expressive as they allow the abstraction of transition probabilities using both intervals and parameters. Unfortunately, as it is the case for IMCs, this allows the expression of incorrect specifications. In the IMC setting, this is the case either when some intervals are ill-formed or when there is no probability distribution matching the interval constraints of the outgoing transitions of some reachable state. In this case, no MC implementation exists that satisfies the IMC specification. Deciding whether an implementation that satisfies a given specification exists is called the consistency problem. In the pIMC setting, the consistency problem is made more complex because of the parameters which can also induce inconsistencies in some cases. One could also be interested in verifying whether there exists an implementation that reaches some target states/labels, and if so, propose a parameter valuation ensuring this property. Both the consistency and the consistent reachability problems have already been investigated in the IMC and pIMC setting [8, 9]. In this section, we briefly recall these problems and propose new solutions based on CSP encodings. Our encodings are linear in the size of the original pIMCs whereas the algorithms from [8, 9] are exponential.

4.1 Existential Consistency

A pIMC $\mathcal{P}$ is existential consistent iff there exists a MC $\mathcal{M}$ satisfying $\mathcal{P}$ (i.e., there exists a MC $\mathcal{M}$ satisfying an IMC $\mathcal{I}$ instance of $\mathcal{P}$). As seen in Section 2, pIMCs are equipped with two semantics: once-and-for-all ($\models^{o}_{\tt{pI}}$) and at-every-step ($\models^{a}_{\tt{pI}}$). Recall that $\models^{o}_{\tt{pI}}$ imposes that the underlying graph structure of implementations needs to be isomorphic to the graph structure of the corresponding specification. In contrast, $\models^{a}_{\tt{pI}}$ allows implementations to have a different graph structure. It therefore seems that some pIMCs could be inconsistent w.r.t $\models^{o}_{\tt{pI}}$ while being consistent w.r.t $\models^{a}_{\tt{pI}}$. On the other hand, checking the consistency w.r.t $\models^{o}_{\tt{pI}}$ seems easier because of the fixed graph structure.

In [8], the author firstly proved that both semantics are equivalent w.r.t. existential consistency, and proposed a CSP encoding for verifying this property which is exponential in the size of the pIMC. Based on this result of semantics equivalence w.r.t. existential consistency from [8] we propose a new CSP encoding, written ${\bf C_{{\exists}c}}$, for verifying the existential consistency property for pIMCs.

Let $\mathcal{P}$ $=$ (S,$$s_{0},$$P,$$V,$$Y) be a pIMC, we write ${\bf C_{{\exists}c}}$($\mathcal{P}$) for the CSP produced by ${\bf C_{{\exists}c}}$ according to $\mathcal{P}$. Any solution of ${\bf C_{{\exists}c}}$($\mathcal{P}$) will correspond to a MC satisfying $\mathcal{P}$. In ${\bf C_{{\exists}c}}$($\mathcal{P}$), we use one variable $\pi_{p}$ with domain $[0,1]$ per parameter $p$ in $Y$; one variable $\theta_{s}^{s^{\prime}}$ with domain $[0,1]$ per transition $(s,s^{\prime})$ in $\{\{s\}\times{\tt{Succ}}(s)\mid s\in S\}$; and one Boolean variable $\rho_{s}$ per state $s$ in $S$. These Boolean variables will indicate for each state whether it appears in the MC solution of the CSP (i.e., in the MC satisfying the pIMC $\mathcal{P}$). For each state $s\in S$, Constraints are as follows:

1. (1)

$\rho_{s}$, if $s=s_{0}$ 2. (3)

$\neg\rho_{s}\Leftrightarrow\Sigma_{s^{\prime}\in{\tt{Pred}}(s)\setminus\{s\}}\theta_{s^{\prime}}^{s}=0$, if $s\neq s_{0}$ 3. (5)

$\rho_{s}\Rightarrow\theta_{s}^{s^{\prime}}\in P(s,s^{\prime})$, for all $s^{\prime}\in{\tt{Succ}}(s)$

1. (2)

$\rho_{s}\Leftrightarrow\Sigma_{s^{\prime}\in{\tt{Succ}}(s)}\theta_{s}^{s^{\prime}}=1$ 2. (4)

$\neg\rho_{s}\Leftrightarrow\Sigma_{s^{\prime}\in{\tt{Succ}}(s)}\theta_{s}^{s^{\prime}}=0$

Recall that given a pIMC $\mathcal{P}$ the objective of the CSP ${\bf C_{{\exists}c}}(\mathcal{P})$ is to construct a MC $\mathcal{M}$ satisfying $\mathcal{P}$. Constraint (1) states that the initial state $s_{0}$ appears in $\mathcal{M}$. Constraint (3) ensures that for each non-initial state $s$, variable $\rho_{s}$ is set to $\mathsf{false}$ iff $s$ is not reachable from its predecessors. Constraint (2) ensures that if a state $s$ appears in $\mathcal{M}$, then its outgoing transitions form a probability distribution. On the contrary, Constraint (4) propagates non-appearing states (i.e., if a state $s$ does not appear in $\mathcal{M}$ then all its outgoing transitions are set to zero). Finally, Constraint (5) states that, for all appearing states, the outgoing transition probabilities must be selected inside the specified intervals.

Example 7

Consider the pIMC $\mathcal{P}$ given in Figure 5. Figure 7 describes the variables in ${\bf C_{{\exists}c}}(\mathcal{P})$: one variable per transition (e.g., $\theta_{0}^{1}$, $\theta_{0}^{2}$, $\theta_{1}^{1}$), one Boolean variable per state (e.g., $\rho_{0}$, $\rho_{1}$), and one variable per parameter ($\pi_{p}$ and $\pi_{q}$). The following constraints correspond to the Constraints (2), (3), (4), and (5) generated by our encoding ${\bf C_{{\exists}c}}$ for the state $2$ of $\mathcal{P}$:

1. $\neg\rho_{2}\Leftrightarrow\theta_{0}^{2}=0$

2. $\neg\rho_{2}\Leftrightarrow\theta_{2}^{1}+\theta_{2}^{2}+\theta_{2}^{4}=0$

3. $\rho_{2}\Leftrightarrow\theta_{2}^{1}+\theta_{2}^{2}+\theta_{2}^{4}=1$

4. $\rho_{2}\Rightarrow 0\leq\theta_{2}^{1}\leq\pi_{p}$

5. $\rho_{2}\Rightarrow 0.2\leq\theta_{2}^{2}\leq\pi_{p}$

6. $\rho_{2}\Rightarrow 0\leq\theta_{2}^{4}\leq 0.5$

Finally, Figure 7 describes a solution for the CSP ${\bf C_{{\exists}c}}(\mathcal{P})$. Note that given a solution of a pIMC encoded by ${\bf C_{{\exists}c}}$, one can construct a MC satisfying the given pIMC by keeping all the states $s$ s.t. $\rho_{s}$ is equal to $\mathsf{true}$ and considering the transition function given by the probabilities in the $\theta_{s}^{s^{\prime}}$ variables. We now show that our encoding works as expected.

Proposition 2

A pIMC $\mathcal{P}$ is existential consistent iff ${\bf C_{{\exists}c}}(\mathcal{P})$ is satisfiable.

Our existential consistency encoding is linear in the size of the pIMC instead of exponential for the encoding from [9] which enumerates the powerset of the states in the pIMC resulting in deep nesting of conjunctions and disjunctions.

4.2 Qualitative Reachability

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC and $\alpha\subseteq A$ be a state label. We say that $\alpha$ is existential reachable in $\mathcal{P}$ iff there exists an implementation $\mathcal{M}$ of $\mathcal{P}$ where $\alpha$ is reachable (i.e., $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)>0$). In a dual way, we say that $\alpha$ is universal reachable in $\mathcal{P}$ iff $\alpha$ is reachable in any implementation $\mathcal{M}$ of $\mathcal{P}$. As for existential consistency, we use a result from [8] that states that both pIMC semantics are equivalent w.r.t. existential (and universal) reachability. We therefore propose a new CSP encoding, written ${\bf C_{{\exists}r}}$, that extends ${\bf C_{{\exists}c}}$, for verifying these properties. Formally, CSP ${\bf C_{{\exists}r}}(\mathcal{P})=(X\cup X^{\prime},D\cup D^{\prime},C\cup C^{\prime})$ is such that $(X,D,C)={\bf C_{{\exists}c}}(\mathcal{P})$, $X^{\prime}$ contains one integer variable $\omega_{s}$ with domain $[0,|S|]$ per state $s$ in $S$, $D^{\prime}$ contains the domains of these variables, and $C^{\prime}$ is composed of the following constraints for each state $s\in S$:

(6)

$\omega_{s}=1$, if $s=s_{0}$

(7)

$\omega_{s}\neq 1$, if $s\neq s_{0}$

(8)

$\rho_{s}\Leftrightarrow(\omega_{s}\neq 0)$

(9)

$\omega_{s}>1\Rightarrow\bigvee_{s^{\prime}\in{\tt{Pred}}(s)\setminus\{s\}}(\omega_{s}=\omega_{s^{\prime}}+1)\wedge(\theta_{s}^{s^{\prime}}>0)$, if $s\neq s_{0}$

(10)

$\omega_{s}=0\Leftrightarrow\bigwedge_{s^{\prime}\in{\tt{Pred}}(s)\setminus\{s\}}(\omega_{s^{\prime}}=0)\vee(\theta_{s}^{s^{\prime}}=0)$, if $s\neq s_{0}$

Recall first that CSP ${\bf C_{{\exists}c}}(P)$ constructs a Markov chain $\mathcal{M}$ satisfying $\mathcal{P}$. Informally, for each state $s$ in $\mathcal{M}$ the Constraints (6), (7), (9) and (10) in ${\bf C_{{\exists}r}}$ ensure that $\omega_{s}=k$ iff there exists in $\mathcal{M}$ a path from the initial state to $s$ of length $k-1$ with non zero probability; and state $s$ is not reachable in $\mathcal{M}$ from the initial state $s_{0}$ iff $\omega_{s}$ equals to [math]. Finally, Constraint (8) enforces the Boolean reachability indicator variable $\rho_{s}$ to bet set to $\mathsf{true}$ iff there exists a path with non zero probability in $\mathcal{M}$ from the initial state $s_{0}$ to $s$ (i.e., $\omega_{s}\neq 0$).

Let $S_{\alpha}$ be the set of states from $\mathcal{P}$ labeled with $\alpha$. ${\bf C_{{\exists}r}}(\mathcal{P})$ therefore produces a Markov chain satisfying $\mathcal{P}$ where reachable states $s$ are such that $\rho_{s}=\mathsf{true}$. As a consequence, $\alpha$ is existential reachable in $\mathcal{P}$ iff ${\bf C_{{\exists}r}}(\mathcal{P})$ admits a solution such that $\bigvee_{s\in S_{\alpha}}\rho_{s}$; and $\alpha$ is universal reachable in $\mathcal{P}$ iff ${\bf C_{{\exists}r}}(\mathcal{P})$ admits no solution such that $\bigwedge_{s\in S_{\alpha}}\neg\rho_{s}$. This is formalised in the following proposition.

Proposition 3

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC, $\alpha\subseteq A$ be a state label, $S_{\alpha}=\{s\ |\ V(s)=\alpha\}$, and $(X,D,C)$ be the CSP ${\bf C_{{\exists}r}}(\mathcal{P})$.

• •

CSP* $(X,D,C\cup\bigvee_{s\in S_{\alpha}}\rho_{s})$ is satisfiable iff $\alpha$ is existential reachable in $\mathcal{P}$*

• •

CSP* $(X,D,C\cup\bigwedge_{s\in S_{\alpha}}\neg\rho_{s})$ is unsatisfiable iff $\alpha$ is universal reachable in $\mathcal{P}$*

As for the existential consistency problem, we have an exponential gain in terms of size of the encoding compared to [9]: the number of constraints and variables in ${\bf C_{{\exists}r}}$ is linear in terms of the size of the encoded pIMC.

Remark. In ${\bf C_{{\exists}r}}$ Constraints (3) inherited from ${\bf C_{{\exists}c}}$ are entailed by Constraints (8) and (10) added to ${\bf C_{{\exists}r}}$. Thus, in a practical approach one may ignore Constraints (3) from ${\bf C_{{\exists}c}}$ if they do not improve the solver performances.

5 Quantitative Properties

We now move to the verification of quantitative reachability properties in pIMCs. Quantitative reachability has already been investigated in the context of pMCs and IMCs with the once-and-for-all semantics. Due to the complexity of allowing implementation structures to differ from the structure of the specifications, quantitative reachability in IMCs with the at-every-step semantics has, to the best of our knowledge, never been studied. In this section, we propose our main theoretical contribution: a theorem showing that both IMC semantics are equivalent with respect to quantitative reachability, which allows the extension of all results from [19, 4] to the at-every-step semantics. Based on this result, we also extend the CSP encodings introduced in Section 4 in order to solve quantitative reachability properties on pIMCs regardless of their semantics.

5.1 Equivalence of $\models^{o}_{\tt{I}}$ and

$\models^{a}_{\tt{I}}$ w.r.t quantitative reachability

Given an IMC $\mathcal{I}=(S,s_{0},P,V)$ and a state label $\alpha\subseteq A$, a quantitative reachability property on $\mathcal{I}$ is a property of the type $\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$, where $0<p<1$ and ${\sim}\in\{\leq,<,>,\geq\}$. Such a property is verified iff there exists an MC $\mathcal{M}$ satisfying $\mathcal{I}$ (with the chosen semantics) such that $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha){\sim}p$.

As explained above, all existing techniques and tools for verifying quantitative reachability properties on IMCs only focus on the once-and-for-all semantics. Indeed, in this setting, quantitative reachability properties are easier to compute because the underlying graph structure of all implementations is known. However, to the best of our knowledge, there are no works addressing the same problem with the at-every-step semantics or showing that addressing the problem in the once-and-for-all setting is sufficiently general. The following theorem fills this theoretical gap by proving that both semantics are equivalent w.r.t quantitative reachability. In other words, for all MC $\mathcal{M}$ such that $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$ and all state label $\alpha$, there exist MCs $\mathcal{M}_{\leq}$ and $\mathcal{M}_{\geq}$ such that $\mathcal{M}_{\leq}\models^{o}_{\tt{I}}\mathcal{I}$, $\mathcal{M}_{\geq}\models^{o}_{\tt{I}}\mathcal{I}$ and $\mathbb{P}^{\mathcal{M}_{\leq}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M_{\geq}}}(\Diamond\alpha)$. This is formalized in the following theorem.

Theorem 5.1

Let $\mathcal{I}=(S,s_{0},P,V)$ be an IMC, $\alpha\subseteq A$ be a state label, ${\sim}\in\{\leq,<,>,\geq\}$ and $0<p<1$. $\mathcal{I}$ satisfies $\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$ with the once-and-for-all semantics iff $\mathcal{I}$ satisfies $\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$ with the at-every-step semantics.

The proof is constructive (see Appendix 0.C.1): we use the structure of the relation $\mathcal{R}$ from the definition of $\models^{a}_{\tt{I}}$ in order to build the MCs $\mathcal{M}_{\leq}$ and $\mathcal{M}_{\geq}$.

5.2 Constraint Encodings

Note that the result from Theorem 5.1 naturally extends to pIMCs. We therefore exploit this result to construct a CSP encoding for verifying quantitative reachability properties in pIMCs. As in Section 4, we extend the CSP ${\bf C_{{\exists}c}}$, that produces a correct MC implementation for the given pIMC, by imposing that this MC implementation satisfies the given quantitative reachability property. In order to compute the probability of reaching state label $\alpha$ at the MC level, we use standard techniques from [2] that require the partitioning of the state space into three sets $S_{\top}$, $S_{\bot}$, and $S_{?}$ that correspond to states reaching $\alpha$ with probability $1$, states from which $\alpha$ cannot be reached, and the remaining states, respectively. Once this partition is chosen, the reachability probabilities of all states in $S_{?}$ are computed as the unique solution of a linear equation system (see [2], Theorem 10.19, p.766). We now explain how we identify states from $S_{\bot},S_{\top}$ and $S_{?}$ and how we encode the linear equation system, which leads to the resolution of quantitative reachability.

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC and $\alpha\subseteq A$ be a state label. We start by setting $S_{\top}=\{s\ |\ V(s)=\alpha\}$. We then extend ${\bf C_{{\exists}r}}(\mathcal{P})$ in order to identify the set $S_{\bot}$. Let ${\bf C^{\prime}_{{\exists}r}}(\mathcal{P},\alpha)=(X\cup X^{\prime},D\cup D^{\prime},C\cup C^{\prime})$ be such that $(X,D,C)={\bf C_{{\exists}r}}(\mathcal{P})$, $X^{\prime}$ contains one Boolean variable $\lambda_{s}$ and one integer variable $\alpha_{s}$ with domain $[0,|S|]$ per state $s$ in $S$, $D^{\prime}$ contains the domains of these variables, and $C^{\prime}$ is composed of the following constraints for each state $s\in S$:

1. (11)

$\alpha_{s}=1$, if $\alpha=V(s)$

1. (12)

$\alpha_{s}\neq 1$, if $\alpha\neq V(s)$

1. (13)

$\lambda_{s}\Leftrightarrow(\rho_{s}\wedge(\alpha_{s}\neq 0))$

1. (14)

$\alpha_{s}>1\Rightarrow\bigvee_{s^{\prime}\in{\tt{Succ}}(s)\setminus\{s\}}(\alpha_{s}=\alpha_{s^{\prime}}+1)\wedge(\theta_{s}^{s^{\prime}}>0)$, if $\alpha\neq V(s)$ 2. (15)

$\alpha_{s}=0\Leftrightarrow\bigwedge_{s^{\prime}\in{\tt{Succ}}(s)\setminus\{s\}}(\alpha_{s^{\prime}}=0)\vee(\theta_{s}^{s^{\prime}}=0)$, if $\alpha\neq V(s)$

Note that variables $\alpha_{s}$ play a symmetric role to variables $\omega_{s}$ from ${\bf C_{{\exists}r}}$: instead of indicating the existence of a path from $s_{0}$ to $s$, they characterize the existence of a path from $s$ to a state labeled with $\alpha$. In addition, due to Constraint (13), variables $\lambda_{s}$ are set to $\mathsf{true}$ iff there exists a path with non zero probability from the initial state $s_{0}$ to a state labeled with $\alpha$ passing by $s$. Thus, $\alpha$ cannot be reached from states s.t. $\lambda_{s}=\mathsf{false}$. Therefore, $S_{\bot}=\{s\ |\ \lambda_{s}=\mathsf{false}\}$.

Finally, we encode the equation system from [2] in a last CSP encoding that extends ${\bf C^{\prime}_{{\exists}r}}$. Let ${\bf C_{{\exists}\bar{r}}}(\mathcal{P},\alpha)=(X\cup X^{\prime},D\cup D^{\prime},C\cup C^{\prime})$ be such that $(X,D,C)={\bf C^{\prime}_{{\exists}r}}(\mathcal{P},\alpha)$, $X^{\prime}$ contains one variable $\pi_{s}$ per state $s$ in $S$ with domain $[0,1]$, $D^{\prime}$ contains the domains of these variables, and $C^{\prime}$ is composed of the following constraints for each state $s\in S$:

1. (16)

$\neg\lambda_{s}\Rightarrow\pi_{s}=0$

1. (17)

$\lambda_{s}\Rightarrow\pi_{s}=1$, if $\alpha=V(s)$

1. (18)

$\lambda_{s}\Rightarrow\pi_{s}=\Sigma_{s^{\prime}\in{\tt{Succ}}(s)}\pi_{s^{\prime}}\theta_{s^{\prime}}^{s}$, if $\alpha\neq V(s)$

As a consequence, variables $\pi_{s}$ encode the probability with which state $s$ eventually reaches $\alpha$ when $s$ is reachable from the initial state and [math] otherwise.

Let $p\in[0,1]\subseteq\mathbb{R}$ be a probability bound. Adding the constraint $\pi_{s_{0}}\leq p$ (resp. $\pi_{s_{0}}\geq p$) to the previous ${\bf C_{{\exists}\bar{r}}}$ encoding allows to determine if there exists a MC $\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$ such that $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\leq p$ (resp $\geq p$). Formally, let ${\sim}\in\{\leq,<,\geq,>\}$ be a comparison operator, we write $\not\sim$ for its negation (e.g., $\not\leq$ is $>$). This leads to the following theorem.

Theorem 5.2

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC, $\alpha\subseteq A$ be a label, $p\in[0,1]$, ${\sim}\in\{\leq,<,\geq,>\}$ be a comparison operator, and $(X,D,C)$ be ${\bf C_{{\exists}\bar{r}}}(\mathcal{P},\alpha)$:

• •

CSP* $(X,D,C\cup(\pi_{s_{0}}\sim p))$ is satisfiable iff $\exists\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$ s.t. $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\sim p$*

• •

CSP* $(X,D,C\cup(\pi_{s_{0}}\not\sim p))$ is unsatisfiable iff $\forall\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$: $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\sim p$*

6 Prototype Implementation

Our results have been implemented in a prototype tool333All resources, benchmarks, and source code are available online as a Python library at https://github.com/anicet-bart/pimc_pylib which generates the above CSP encodings, and CSP encodings from [9] as well. Given a pIMC in a text format inspired from [19], our tool produces the desired CSP as a SMT instance with the QF_NRA logic (Quantifier Free Non linear Real-number Arithmetic). This instance can then be fed to any solver accepting the SMT-LIB format with QF_NRA logic [3]. For our benchmarks, we chose Z3 [6] (latest version: 4.5.0).

QF_NRA does not deal with integer variables. In practice, logics mixing integers and reals are harder than those over reals only. Thus we obtained better results by encoding integer variables into real ones. In our implementations each integer variable $x$ is declared as a real variable whose real domain bounds are its original integer domain bounds; we also add the constraint $x<1\Rightarrow x=0$. Since we only perform incrementation of $x$ this preserves the same set of solutions.

In order to evaluate our prototype, we extend the nand model from [15]444Available online at http://www.prismmodelchecker.com. The original MC nand model has already been extended as a pMC in [7], where the authors consider a single parameter $p$ for the probability that each of the $N$ $nand$ gates fails during the multiplexing. We extend this model to pIMC by considering intervals for the probability that the initial inputs are stimulated and we have one parameter per $nand$ gate to represent the probability that it fails. pIMCs in text format are automatically generated from the PRISM model.

Table 1 summarizes the size of the considered instances of the model (in terms of states, transitions, and parameters) and of the corresponding CSP problems (in terms of number of variables and constraints). In addition, we also present the resolution time of the given CSPs using the Z3 solver. Our experiments were performed on a $2.4$ GHz Intel Core i5 processor with time out set to $10$ minutes and memory out set to $2$Gb.

7 Conclusion and future work

In this paper, we have compared several Markov Chain abstractions in terms of succinctness and we have shown that Parametric Interval Markov Chain is a strictly more succinct abstraction formalism than other existing formalisms such as Parametric Markov Chains and Interval Markov Chains. In addition, we have proposed constraint encodings for checking several properties over pIMC. In the context of qualitative properties such as existencial consistency or consistent reachability, the size of our encodings is significantly smaller than other existing solutions. In the quantitative setting, we have compared the two usual semantics for IMCs and pIMCs and showed that both semantics are equivalent with respect to quantitative reachability properties. As a side effect, this result ensures that all existing tools and algorithms solving reachability problems in IMCs under the once-and-for-all semantics can safely be extended to the at-every-step semantics with no changes. Based on this result, we have then proposed CSP encodings addressing quantitative reachability in the context of pIMCs regardless of the chosen semantics. Finally, we have developed a prototype tool that automatically generates our CSP encodings and that can be plugged to any constraint solver accepting the SMT-LIB format as input.

We plan to develop our tool for pIMC verification in order to manage other, more complex, properties (e.g., supporting the LTL-language in the spirit of what Tulip [19] does). We also plan on investigating a practical way of computing and representing the set of all solutions to the parameter synthesis problem.

Appendix 0.A Complements to Section 3

0.A.1 $\models^{a}_{\tt{I}}$ is More General

than $\models^{o}_{\tt{I}}$

The at-every-step satisfaction relation is more general than the once-and-for-all satisfaction relation. Let $\mathcal{I}=(S,s_{0},P,V)$ be an IMC and $\mathcal{M}=(T,t_{0},p,V^{\prime})$ be a MC. We show that

1. $\mathcal{M}\models^{o}_{\tt{I}}\mathcal{I}\Rightarrow\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$;

2. in general $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}\not\Rightarrow\mathcal{M}~{}\models^{o}_{\tt{I}}~{}\mathcal{I}$. The following examples also illustrates that even if a Markov chain satisfies an IMC with the same graph representation w.r.t. the $\models^{a}_{\tt{I}}$ relation it may not verify the $\models^{o}_{\tt{I}}$ relation.

If $\mathcal{M}\models^{o}_{\tt{I}}\mathcal{I}$ then by definition of $\models^{o}_{\tt{I}}$ we have that $T=S$, $t_{0}=s_{0}$, and $p(s)(s^{\prime})\in P(s,s^{\prime})$. The relation $\mathcal{R}=\{(s,s)\mid s\in S\}$ is a satisfaction relation between $\mathcal{M}$ and $\mathcal{I}$ (consider for each state in $S$ the correspondence function $\delta:S\to(S\to[0,1])$ s.t. $\delta(s)(s^{\prime})=1$ if $s=s^{\prime}$ and $\delta(s)(s^{\prime})=0$ otherwise). Thus $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$. 2. 2.

Consider IMC $\mathcal{I}$, MCs $\mathcal{M}_{1}$, $\mathcal{M}_{2}$, and $\mathcal{M}_{3}$ from Figure 8.

1. (a)

By definition of $\models^{o}_{\tt{I}}$ we have that $\mathcal{M}_{1}\models^{o}_{\tt{I}}\mathcal{I}$. Thus by the previous remark we have that $\mathcal{M}_{1}\models^{a}_{\tt{I}}\mathcal{I}$ ($t_{0}=s_{0}$, $t_{1}=s_{1}$ and $t_{2}=s_{2}$). 2. (b)

By definition of $\models^{o}_{\tt{I}}$ we have that $\mathcal{M}_{2}\not\models^{o}_{\tt{I}}\mathcal{I}$. However the relation $\mathcal{R}$ containing $(t_{0},s_{0})$, $(t_{1},s_{1})$, $(t_{1},s_{2})$, $(t_{2},s_{1})$ and $(t_{2},s_{2})$ is a satisfaction relation between $\mathcal{I}$ and $\mathcal{M}_{2}$. Consider the functions: $\delta$ from $T$ to $(S\to[0,1])$ s.t. $\delta(t_{1})(s_{1})=4/5$, $\delta(t_{1})(s_{2})=1/5$, $\delta(t_{2})(s_{2})=1$, and $\delta(t)(s)=0$ otherwise; $\delta^{\prime}$ with the same signature than $\delta$ s.t. $\delta^{\prime}(t_{1})(s_{1})=1$, $\delta^{\prime}(t_{2})(s_{2})=1$, and $\delta^{\prime}(t)(s)=0$ otherwise. We have that $\delta$ is a correspondence function for the pair $(t_{0},s_{0})$ and $\delta^{\prime}$ is a correspondence function for all the remaining pairs in $\mathcal{R}$. Thus there exists a MCs $\mathcal{M}$ s.t. $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$ and $\mathcal{M}\not\models^{o}_{\tt{I}}\mathcal{I}$.

0.A.2 Model Comparison

According to the given succinctness definition, Lemma 1 states that $\tt{IMC}$ and $\tt{pMC}$ are not comparable w.r.t. both satisfaction relation $\models^{o}_{\tt{I}}$ and $\models^{a}_{\tt{I}}$ and that both satisfaction relations for IMCs are not comparable.

Lemma 1

$\tt{pMC}$* and $\tt{IMC}$ abstraction models are not comparable:

1. \tt{pMC}\not\leq$$(\tt{IMC},\models^{a}_{\tt{I}});

2. $\tt{pMC}\not\leq(\tt{IMC},\models^{o}_{\tt{I}})$;

3. (\tt{IMC},\models^{a}_{\tt{I}})\not\leq$$\tt{pMC};

4. $(\tt{IMC},\models^{a}_{\tt{I}})\not\leq(\tt{IMC},\models^{o}_{\tt{I}})$;

5. $(\tt{IMC},\models^{o}_{\tt{I}})\not\leq\tt{pMC}$;

6. $(\tt{IMC},\models^{o}_{\tt{I}})\not\leq(\tt{IMC},\models^{a}_{\tt{I}})$;

We give a sketch of proof for each statement. Let $({\tt L}_{1},\models_{1})$ and $({\tt L}_{2},\models_{2})$ be two Markov chain abstraction models. Recall that according to the succinctness definition (cf. Definition 5) ${\tt L}_{1}\not\leq{\tt L}_{2}$ if there exists $\mathcal{L}_{2}\in{\tt L}_{2}$ s.t. $\mathcal{L}_{1}\not\equiv\mathcal{L}_{2}$ for all $\mathcal{L}_{1}\in{\tt L}_{1}$.

Consider IMC $\mathcal{I}$ and pMCs $\mathcal{P}_{1}$, $\mathcal{P}_{2}$, and $\mathcal{P}_{n}$ (with $n\in\mathbb{N}$) from Figure 9. presents an IMC $\mathcal{I}$ verifying case (1) $\mathcal{P}_{1}$, $\mathcal{P}_{2}$, and $\mathcal{P}_{n}$ (with $n\in\mathbb{N}$) are entailed by $\mathcal{I}$ w.r.t. $\models^{a}_{\tt{I}}$ but none of them is equivalent to $\mathcal{I}$. Indeed one needs an infinite countable number of states for creating a pMC equivalent to $\mathcal{I}$ w.r.t. $\models^{a}_{\tt{I}}$. However states space must be finite. 2. 2.

Consider IMC $\mathcal{I^{\prime}}$ similar to $\mathcal{I}$ from Figure 9 excepted that the transition from $s_{1}$ to $s_{0}$ is replaced by the interval $[0.5,1]$. Since the pIMC definition does not allow to bound values for parameters there is no equivalent $\mathcal{I^{\prime}}$ w.r.t. $\models^{a}_{\tt{I}}$. 3. 3.

Note that parameters in pMCs enforce transitions in the concrete MCs to receive the same value. Since parameters may range over continuous intervals there is no hope of modeling such set of Markov chains using a single IMC. Figure 9 illustrates this statement. 4. 4.

Recall that $(\textnormal{IMC},\models^{a}_{\tt{I}})$ is more general than $(\textnormal{IMC},\models^{o}_{\tt{I}})$. One cannot restrict the set of Markov chains satisfying an IMC w.r.t. $\models^{a}_{\tt{I}}$ to be bisimilar to the set of Markov chain satisfying an IMC w.r.t. $\models^{o}_{\tt{I}}$. 5. 5.

Same remark than item (3) 6. 6.

Counter-example similar to which in statement (2) (i.e., in order to simulate the at-every-step satisfaction relation with the once-and-for-all satisfaction relation one needs an infinite uncountable number of states).

Proposition 1.

The Markov chain abstraction models can be ordered as follows w.r.t. succinctness: $({\tt{pIMC}},\models^{o}_{\tt{pI}})<(\tt{pMC},\models_{\tt{p}})$, $({\tt{pIMC}},\models^{o}_{\tt{pI}})<(\tt{IMC},\models^{o}_{\tt{I}})$ and $({\tt{pIMC}},\models^{a}_{\tt{pI}}\nobreak)<(\tt{IMC},\models^{a}_{\tt{I}})$.

Proof

Recall that the $\tt{pIMC}$ model is a Markov chain abstraction model allowing to declare parametric interval transitions, while the $\tt{pMC}$ model allows only parametric transitions (without intervals), and the $\tt{IMC}$ model allows interval transitions without parameters. Clearly, any pMC and any IMC can be translated into a pIMC with the right semantics (once-and-for-all for pMCs and the chosen IMC semantics for IMCs). This means that $({\tt{pIMC}},\models^{o}_{\tt{pI}})$ is more succinct than $\tt{pMC}$ and $\tt{pIMC}$ is more succinct than $\tt{IMC}$ for both semantics. Furthermore since $\tt{pMC}$ and $\tt{IMC}$ are not comparable (cf Lemma 1), we have that the $\tt{pIMC}$ abstraction model is strictly more succinct than the $\tt{pMC}$ abstraction model and than the $\tt{IMC}$ abstraction model with the right semantics.

Appendix 0.B Complements to Section 4

0.B.1 CSP Encoding for Qualitative Reachability

Proof (Proposition 2)

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC.

$[\Rightarrow]$ The CSP ${\bf C_{{\exists}c}}(\mathcal{P})=(X,D,C)$ is satisfiable implies that there exists a valuation $v$ of the variables in $X$ satisfying all the constraints in $C$. Consider the MC $\mathcal{M}=(S,s_{0},p,V)$ such that $p(s,s^{\prime})=v(\theta_{s}^{s^{\prime}})$, for all $\theta_{s}^{s^{\prime}}\in\Theta$ and $p(s,s^{\prime})=0$ otherwise.

Firstly, we show by induction that for any state $s$ in $S$: “if $s$ is reachable in $\mathcal{M}$ then $v(\rho_{s})$ equals to $\mathsf{true}$”. This is correct for the initial state $s_{0}$ thanks to the Constraint (1). Let $s$ be a state in $S$ and assume that the property is correct for all its predecessors. By the Constraints (2), $v(\rho_{s})$ equals to $\mathsf{true}$ if there exists at least one predecessor $s^{\prime\prime}\neq s$ reaching $s$ with a non-zero probability (i.e., $v(\theta_{s^{\prime\prime}}^{s})\neq 0$). This is only possible by the Constraint (3) if $v(\rho_{s^{\prime\prime}})$ equals to $\mathsf{true}$. Thus $v(\rho_{s})$ equals to $\mathsf{true}$ if there exists one reachable state $s^{\prime\prime}$ s.t. $v(\theta_{s^{\prime\prime}}^{s})\neq 0$.

Secondly, we show that $\mathcal{M}$ satisfies the pIMC $\mathcal{P}$. We use Theorem 4 from [9] stating that $\models^{a}_{\tt{pI}}$ and $\models^{o}_{\tt{pI}}$ are equivalent w.r.t. qualitative reachability. We proved above that for all reachable states $s$ in $\mathcal{M}$, we have $v(\rho_{s})$ equals to $\mathsf{true}$. By the Constraints (5) it implies that that for all reachable states $s$ in $\mathcal{M}$: $p(s,s^{\prime})\in P(s,s^{\prime})$ for all $s$ and $s^{\prime}$.555As illustrated in Example 7, $\mathcal{M}$ is not a well formed MC since some unreachable states do not respect the probability distribution property. However, one can correct it by simply setting one of its outgoing transition to $1$ for each unreachable state.

$[\Leftarrow]$ The pIMC $\mathcal{P}$ is consistent implies by the Theorem 4 from [9] stating that $\models^{a}_{\tt{pI}}$ and $\models^{o}_{\tt{pI}}$ are equivalent w.r.t. qualitative reachability, that there exists an implementation of the form $\mathcal{M}=(S,s_{0},p,V)$ where, for all reachable states $s$ in $\mathcal{M}$, it holds that $p(s,s^{\prime})\in P(s,s^{\prime})$ for all $s^{\prime}$ in $S$. Consider $\mathcal{M}^{\prime}=(S,s_{0},p^{\prime},V)$ s.t. for each non reachable state $s$ in $S$: $p^{\prime}(s,s^{\prime})=0$, for all $s^{\prime}\in S$. The valuation $v$ is s.t. $v(\rho_{s})$ equals $\mathsf{true}$ iff $s$ is reachable in $\mathcal{M}$, $v(\theta_{s}^{s^{\prime}})=p^{\prime}(s,s^{\prime})$, and for each parameter $y\in Y$ a valid value can be selected according to $p$ and $P$ when considering reachable states. Finally, by construction, $v$ satisfies the CSP ${\bf C_{{\exists}c}}(\mathcal{P})$.∎

Appendix 0.C Complements to Section 5

0.C.1 Equivalence of $\models^{o}_{\tt{I}}$ and

$\models^{a}_{\tt{I}}$ w.r.t quantitative reachability

We first introduce some notations. Let $\mathcal{I}=(S,s_{0},P,V^{I})$ be an IMC and $\mathcal{M}=(T,t_{0},p,V^{M})$ be an MC s.t. $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$. Let $\mathcal{R}\subseteq T\times S$ be a satisfaction relation between $\mathcal{M}$ and $\mathcal{I}$. For all $t\in T$ we write $\mathcal{R}(t)$ for the set $\{s\in S\mid t~{}\mathcal{R}~{}s\}$, and for all $s\in S$ we write $\mathcal{R}^{-1}(t)$ for the set $\{t\in T\mid s~{}\mathcal{R}~{}t\}$. Furthermore we say that $\mathcal{M}$ satisfies $\mathcal{I}$ with degree $n$ (written \mathcal{M}\mathrel{\mathop{\models^{a}_{\tt{I}}}\limits^{\vbox to-1.50694pt{\kern-2.0pt\hbox{\scriptstyle\text{\hskip 0.56917pt\small{$n$}}}\vss}}}\mathcal{I}) if $\mathcal{M}$ satisfies $\mathcal{I}$ with a satisfaction relation $\mathcal{R}$ s.t. each state $t\in T$ is associated by $\mathcal{R}$ to at most $n$ states from $S$ (i.e., $|\mathcal{R}(t)|\leq n$); $\mathcal{M}$ satisfies $\mathcal{I}$ with the same structure than $\mathcal{I}$ if $\mathcal{M}$ satisfies $\mathcal{I}$ with a satisfaction relation $\mathcal{R}$ s.t. each state $t\in T$ is associated to at most one state from $S$ and each state $s\in S$ is associated to at most one state from $T$ (i.e., $|\mathcal{R}(t)|\leq 1$ for all $t\in T$ and $|\mathcal{R}^{-1}(s)|\leq 1$ for all $s\in S$).

Proposition 4

Let $\mathcal{I}$ be an IMC. If a MC $\mathcal{M}$ satisfies $\mathcal{I}$ with degree $n\in\mathbb{N}$ then there exists a MC $\mathcal{M^{\prime}}$ satisfying $\mathcal{I}$ with degree $1$ such that $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are bisimilar.

The main idea for proving Proposition 4 is that if an MC $\mathcal{M}$ with states space $T$ satisfies an IMC $\mathcal{I}$ with a states space $S$ according to a satisfaction relation $\mathcal{R}$ then, each state $t$ related by $\mathcal{R}$ to many states $s_{1},\ldots,s_{n}$ (with $n>1$) can be split in $n$ states $t^{1},\ldots,t^{n}$. The derived MC will satisfy $\mathcal{I}$ with a satisfaction relation $\mathcal{R}^{\prime}$ where each $t_{i}$ is only associated by $\mathcal{R}^{\prime}$ to the state $s_{i}$ ($i\leq n$). This $\mathcal{M^{\prime}}$ will be bisimilar to $\mathcal{M}$ and it will satisfy $\mathcal{I}$ with degree $1$. Note that by construction the size of the resulting MC is in $O(|\mathcal{M}|\times|\mathcal{I}|)$.

Proof (Proposition 4)

Let $\mathcal{I}=(S,s_{0},P,V^{I})$ be an IMC and $\mathcal{M}=(T,t_{0},p,V)$ be a MC. If $\mathcal{M}$ satisfies $\mathcal{I}$ (with degree $n$) then there exists a satisfaction relation $\mathcal{R}$ verifying the $\models^{a}_{\tt{I}}$ satisfaction relation. For each association $t~{}\mathcal{R}~{}s$, we write $\delta_{t}^{s}$ the correspondence function chosen for this pair of states. $\mathcal{M}$ satisfies $\mathcal{I}$ with degree $n$ means that each state in $\mathcal{M}$ is associated by $\mathcal{R}$ to at most $n$ states in $\mathcal{I}$. To construct a MC $\mathcal{M^{\prime}}$ satisfying $\mathcal{I}$ with degree $1$ we create one state in $\mathcal{M^{\prime}}$ per association $(t,s)$ in $\mathcal{R}$. Formally, let $\mathcal{M^{\prime}}$ be equal to $(U,u_{0},p^{\prime},V^{\prime})$ such that $U=\{u_{t}^{s}\mid t~{}\mathcal{R}~{}s\}$, $u_{0}=u_{t_{0}}^{s_{0}}$, $V^{\prime}=\{(u_{t}^{s},v)\mid v=V(t)\}$, and $p^{\prime}(u_{t}^{s})(u_{t^{\prime}}^{s^{\prime}})=p(t)(t^{\prime})\times\delta_{t}^{s}(t^{\prime})(s^{\prime})$. Following computation shows that the outgoing probabilities given by $p^{\prime}$ form a probability distribution for each state in $\mathcal{M^{\prime}}$ and thus that $\mathcal{M^{\prime}}$ is a MC.

[TABLE]

Finally, by construction of $\mathcal{M^{\prime}}$ based on $\mathcal{M}$ which satisfies $\mathcal{I}$, we get that $\mathcal{R^{\prime}}=\{(u_{t}^{s},s)\mid t\in T,s\in S\}$ is a satisfaction relation between $\mathcal{M^{\prime}}$ and $\mathcal{I}$. Furthermore $|\{s\mid u~{}\mathcal{R^{\prime}}~{}s\}|$ equals at most one. Thus, we get that $\mathcal{M^{\prime}}$ satisfies $\mathcal{I}$ with degree $1$.

Consider the relation $\mathcal{B}^{\prime}=\{(u_{t}^{s},t)\subseteq U\times T\mid t~{}\mathcal{R}~{}s\}$. We note $\mathcal{B}$ the closure of $\mathcal{B}^{\prime}$ by transitivity, reflexivity and symetry (i.e., $\mathcal{B}$ is the minimal equivalence relation based on $\mathcal{B}^{\prime}$). We prove that $\mathcal{B}$ is a bisimulation relation between $\mathcal{M}$ and $\mathcal{M^{\prime}}$. By construction each equivalence class from $\mathcal{B}$ contains exactly one state $t$ from $T$ and all the states $u_{t}^{s}$ such that $t~{}\mathcal{R}~{}s$. Let $(u_{t}^{s},t)$ be in $\mathcal{B}$, $t^{\prime}$ be a state in $T$, and $B$ be the equivalence class from $\mathcal{B}$ containing $t^{\prime}$ (i.e., $B$ is the set $\{t^{\prime}\}\cup\{u_{t^{\prime}}^{s^{\prime}}\in U\mid s^{\prime}\in S\text{ and }t^{\prime}~{}\mathcal{R}~{}s^{\prime}\}$). Firstly note that by construction the labels agree on $u_{t}^{s}$ and $t$: $V^{\prime}(u_{t}^{s})=V(t)$. Secondly the following computation shows that $p^{\prime}(u_{t}^{s})(B\cap U)$ equals to $p(t)(B\cap T)$ and thus that $u_{t}^{s}$ and $t$ are bisimilar:

[TABLE]

∎

Corollary 1

Let $\mathcal{I}$ be an IMC, $\mathcal{M}$ be a MC satisfying $\mathcal{I}$, and $\gamma$ be a PCTL∗ formulae. There exists a MC $\mathcal{M^{\prime}}$ satisfying $\mathcal{I}$ with degree $1$ such that the probability $\mathbb{P}^{\mathcal{M}^{\prime}}(\gamma)$ equals the probability $\mathbb{P}^{\mathcal{M}}(\gamma)$.

Corollary 1 is derived from Proposition 4 joined with the probability preservation of the PCTL* formulae on bisimilar Markov chains (see [2], Theorem 10.67, p.813). Corollary 1 allows to reduce to one the number of states in the pIMC $\mathcal{I}$ satisfied by each state in the MC $\mathcal{M}$ while preserving probabilities.

Lemma 2

Let $\mathcal{I}=(S,s_{0},P,V)$ be an IMC, $\mathcal{M}=(T,t_{0},p,V)$ be a MC satisfying $\mathcal{I}$ with degree $1$, and $\alpha\subseteq A$ be a proposition. If $\mathcal{M}$ does not have the same structure than $\mathcal{I}$ then there exists an MC $\mathcal{M}_{1}$ (resp. $\mathcal{M}_{2}$) satisfying $\mathcal{I}$ with a set of states $S_{1}$ (resp. $S_{2}$) s.t. $S_{1}\subset S$ and $\mathbb{P}^{\mathcal{M}_{1}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$ (resp. $S_{2}\subset S$ and $\mathbb{P}^{\mathcal{M}_{2}}(\Diamond\alpha)\geq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$).

Lemma 2 reduces the number of states in $\mathcal{M}$ while preserving the maximal or minimal reachability probability. This lemma has a constructive proof. Here is the main idea of the proof. We first select one state $s$ from the IMC $\mathcal{I}$ which is satisfied by many states $t_{1},\ldots,t_{n}$ in $\mathcal{M}$. The MC $\mathcal{M}^{\prime}$ keeping the state $t_{k}$ minimizing the probability of reaching $\alpha$ in $\mathcal{M}$ and removing all the other states $t_{i}$ (i.e., remove the states $t_{i}$ s.t. $i\neq k$ and move the transitions arriving to a state $t_{i}$ s.t. $i\neq k$ to arrive to the state $t_{k}$) will have less states than $\mathcal{M}$ and verifies $\mathbb{P}^{\mathcal{M}_{1}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$.

Proof (Lemma 2)

Let $\mathcal{I}=(S,s_{0},P,V^{I})$ be an IMC and $\mathcal{M}=(T,t_{0},p,V)$ be a MC satisfying $\mathcal{I}$ with degree $1$. We write $\mathcal{R}$ the satisfaction relation between $\mathcal{M}$ and $\mathcal{I}$ with degree $1$. The following proves in 3 steps the $\mathbb{P}^{\mathcal{M}_{1}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$ case.

We would like to construct a MC $\mathcal{M}^{\prime}$ satisfying $\mathcal{I}$ with less states than $\mathcal{M}^{\prime}$ such that $\mathbb{P}^{\mathcal{M}^{\prime}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$. Since the degree of $\mathcal{R}$ equals to $1$ each state $t$ in $T$ is associated to at most one state $s$ in $S$. Furthermore, since $\mathcal{M}$ does not have the same structure than $\mathcal{I}$ then there exists at most one state from $S$ which is associated by $\mathcal{R}$ to many states from $T$. Let $\bar{s}$ be a state from $S$ such that $|\mathcal{R}^{-1}(s)|\geq 2$, $\bar{T}=\{t_{1},\ldots,t_{n}\}$ be the set $\mathcal{R}^{-1}(s)$ where the $t_{i}$ are ordered by decreasing probability of reaching $\alpha$ (i.e., $\mathbb{P}^{\mathcal{M}}_{t_{i}}(\Diamond\alpha)\geq\mathbb{P}^{\mathcal{M}}_{t_{i+1}}(\Diamond\alpha)$ for all $1\leq i<n$). In the following we refer $\bar{t}$ as $t_{n}$. We produce $\mathcal{M}^{\prime}$ from $\mathcal{M}$ by replacing all the transitions going to a state $t_{1},\ldots,t_{n-1}$ by a transition going to $t_{n}$, and by removing the corresponding states. Formally $\mathcal{M}^{\prime}=(T^{\prime},t_{0},p^{\prime},V^{\prime})$ s.t. $T^{\prime}=(T\setminus\bar{T})\cup\{\bar{t}\}$, $V^{\prime}$ is the restriction of $V$ on $T^{\prime}$, and for all $t,t^{\prime}\in T^{\prime}$: $p^{\prime}(t)(t^{\prime})=p(t)(t^{\prime})$ if $t^{\prime}\neq\bar{t}$ and $p^{\prime}(t)(t^{\prime})=\sum\limits_{\mathclap{t^{\prime}\in\bar{T}}}p(t)(t^{\prime})$ otherwise.

[TABLE]

Previous computation holds for each state $t$ in $\mathcal{M^{\prime}}$. It shows that the outgoing probabilities given by $p^{\prime}$ form a probability distribution for each state in $\mathcal{M^{\prime}}$ and thus that $\mathcal{M^{\prime}}$ is a MC. Note that step ($1$) comes from the definition of $p^{\prime}$ with respect to $p$ and that step ($2$) comes from the definition of $T^{\prime}$ according to $\bar{T}$ and $\bar{t}$. 2. 2.

We now prove that $\mathcal{M}^{\prime}$ implements $\mathcal{I}$. $\mathcal{M}$ satisfies $\mathcal{I}$ implies that there a exists a satisfaction relation $\mathcal{R}$ between $\mathcal{M}$ and $\mathcal{I}$. Let $\mathcal{R}^{\prime}\subseteq T\times S$ be s.t. $t~{}\mathcal{R}^{\prime}~{}s$ if $t~{}\mathcal{R}~{}s$ and $\bar{t}~{}\mathcal{R}^{\prime}~{}\bar{s}$ if there exists a state $t^{\prime}\in\bar{T}$ s.t. $t^{\prime}~{}\mathcal{R}~{}\bar{s}$. We prove that $\mathcal{R}^{\prime}$ is a satisfaction relation between $\mathcal{M}^{\prime}$ and $\mathcal{I}$. For each pair $(t,s)\in\mathcal{R}$ we note $\delta_{(s,t)}$ the correspondance function given by the satisfaction relation $\mathcal{R}$. Let $(t,s)$ be in $\mathcal{R}^{\prime}$ and $\delta^{\prime}:T^{\prime}\to(S\to[0,1])$ be s.t. $\delta^{\prime}(t^{\prime})(s^{\prime})=\delta_{(t,s)}(t^{\prime})(s^{\prime})$ if $t^{\prime}\neq\bar{t}$ and $\delta^{\prime}(t^{\prime})(s^{\prime})=max_{t^{\prime}\in\bar{T}}(\delta_{(t,s)}(t^{\prime})(s^{\prime}))$ otherwise. $\delta^{\prime}$ is a correspondence function for the pair $(t,s)$ in $\mathcal{R}^{\prime}$ such as required by the $\models^{a}_{\tt{I}}$ satisfaction relation:

1. (a)

Let $t^{\prime}$ be in $T$. If $t^{\prime}\neq\bar{t}$ then $\delta^{\prime}(t^{\prime})$ is equivalent to $\delta_{(t,s)}(t^{\prime})(s^{\prime})$ which is by definition a distribution on $S$. Otherwise $t^{\prime}=\bar{t}$ and the following computation proves that $\delta^{\prime}(\bar{t})$ is a distribution on $S$. For the step (1) remind that $\mathcal{R}$ is a satisfaction relation with degree $1$ and that $\bar{t}~{}\mathcal{R}~{}\bar{s}$. This implies that $\delta_{(t,s)}(\bar{t})(s^{\prime})$ equals to zero for all $s^{\prime}\neq\bar{s}$. For the step (2), $\mathcal{R}$ is a satisfaction relation with degree $1$ implies that $\delta_{(t,s)}(t^{\prime})(s^{\prime})$ equals to [math] or $1$ for all $t^{\prime}\in T$ and $s^{\prime}\in S$. Finally the recursive definition of the satisfaction relation $\mathcal{R}$ implies that there exists at least one state $t^{\prime\prime}\in\bar{T}$ s.t. $\delta_{(t,s)}(t^{\prime\prime})(\bar{s})$ does not equal to zero (i.e., equals to one).

[TABLE] 2. (b)

Let $s^{\prime}$ be in $S$. Step (1) uses the definition of $p^{\prime}$ according to $p$. Step (2) uses the definition of $\delta^{\prime}$ according to $\delta_{(t,s)}$. Step (3) comes from the fact that for all $t,t^{\prime}\in T\times\bar{T}$, we have by the definition of the satisfaction relation $\mathcal{R}$ with degree $1$ and by construction of $\bar{T}$ that if $p(t,t^{\prime})\neq 0$ then $\delta_{(t)(s)}(t^{\prime},\bar{s})=1$ and $\delta_{(t,s)}(t^{\prime})(s^{\prime})=0$ for all $s^{\prime}\neq\bar{s}$. Finally, step (4) comes from the definition of the correspondence function $\delta_{(t,s)}$ for the pair $(t,s)$ in $\mathcal{R}$.

[TABLE] 3. (c)

Let $t^{\prime}$ be in $T^{\prime}$ and $s^{\prime}$ be in $S$. We have by construction of $\mathcal{R}^{\prime}$ from $\mathcal{R}$ that if $\delta^{\prime}(t^{\prime})(s^{\prime})>0$ then $(t^{\prime},s^{\prime})\in\mathcal{R}$. 3. 3.

Ne now prove that the probability of reaching $\alpha$ from $\bar{t}$ is lower in $\mathcal{M^{\prime}}$ than in $\mathcal{M}$. We consider the MC $\mathcal{M}^{\prime\prime}$ from $\mathcal{M}$ where the states containing the label $\alpha$ are replaced by absorbing states. Formally $\mathcal{M}^{\prime\prime}=(T,t_{0},p^{\prime\prime},V)$ such that for all $t,t^{\prime}\in T$: $p^{\prime\prime}(t,t^{\prime})=p(t,t^{\prime})$ if $\alpha\not\subseteq V(t)$ else $p^{\prime\prime}(t,t^{\prime})=1$ if $t=t^{\prime}$ and $p^{\prime\prime}(t,t^{\prime})=0$ otherwise. By definition of the reachability property we get that $\mathbb{P}^{\mathcal{M}^{\prime\prime}}_{t}(\Diamond\alpha)$ equals to $\mathbb{P}^{\mathcal{M}}_{t}(\Diamond\alpha)$ for all state $t$ in $T^{\prime}$. Following computation concludes the proof. Step (1) comes from Lemma 3. Step (2) comes by construction of $\mathcal{M}^{\prime}$ from $\mathcal{M}$. Step (3) comes by construction of $\mathcal{M}^{\prime\prime}$ from $\mathcal{M}$ where states labeled with $\alpha$ are absorbing states. Step (4) comes from the fact that $\mathbb{P}^{\mathcal{M}^{\prime\prime}}_{t_{n}}(\Diamond\alpha)$ is equal to $\mathbb{P}^{\mathcal{M}^{\prime\prime}}_{t_{n}}(\neg(t_{1}\lor\ldots\lor t_{n})\textnormal{ U }\alpha)+\Sigma_{1\leq i\leq n}\mathbb{P}^{\mathcal{M}^{\prime\prime}}_{t_{n}}(\neg(t_{1}\lor\ldots\lor t_{n})\textnormal{ U }t_{i})\times\mathbb{P}^{\mathcal{M}^{\prime\prime}}_{t_{i}}(\Diamond\alpha)$. Step (5) uses the fact that $\mathbb{P}^{\mathcal{M}}_{t_{i}}(\Diamond\alpha)\geq\mathbb{P}^{\mathcal{M}}_{t_{n}}(\Diamond\alpha)$ for all $1\leq i\leq n$ and by construction this is also correct in $\mathcal{M}^{\prime\prime}$. Last steps are straightforward.

[TABLE]

The same method can be used for proving the $\mathbb{P}^{\mathcal{M}_{2}}(\Diamond\alpha)\geq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$ case by defining $\bar{T}=\{t_{1},\ldots,t_{n}\}$ be the set $\mathcal{R}^{-1}(s)$ s.t. the $t_{i}$ are ordered by increasing probability of reaching $\alpha$. Thereby the $\leq$ symbol at step (5) for the computation of $\mathbb{P}^{\mathcal{M}^{\prime}}_{\bar{t}}(\Diamond\alpha)$ is replaced by the $\geq$ symbol.∎

Lemma 3

Let $\mathcal{M}=(S,s_{0},p,V)$ be a MC, $\alpha\subseteq A$ be a proposition, and $s$ be a state from $S$. Then

[TABLE]

Lemma 3 is called in the proof of Lemma 2.

Proof (Lemma 3)

Let $S^{\prime}$ be the subset of $S$ containing all the states labeled with $\alpha$ in $\mathcal{M}$. We write $\Omega_{n}$ with $n\in\mathbb{N}^{*}$ the set containing all the paths $\omega$ starting from $s$ s.t. state $s$ appears exactly $n$ times in $\omega$ and no state in $\omega$ is labeled with $\alpha$. Formally $\Omega_{n}$ contains all the $\omega=s_{1},\ldots,s_{k}\in S^{k}$ s.t. $k\in\mathbb{N}$, $s_{1}$ is equal to $s$, $|\{i\in[1,k]\mid s_{i}=s\}|=n$, and $\alpha\not\subseteq V(s_{i})$ for all $i\in[1,k]$. We get by (a) that $(\mathbb{P}^{\mathcal{M}}_{s}(\Omega_{n}\times S^{\prime}))_{n\geq 1}$ is a geometric series. In (b) we partition the paths reaching $\alpha$ according to the $\Omega_{n}$ sets and we use the geometric series of the probabilities to retrieve the required result.

[TABLE]

[TABLE]

∎

Lemma 4

Let $\mathcal{I}=(S,s_{0},P,V)$ be an IMC, $\mathcal{M}$ be an MC satisfying $\mathcal{I}$, and $\alpha\subseteq A$ be a proposition. There exist MCs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ satisfying $\mathcal{I}$ with the same structure than $\mathcal{I}$ such that $\mathbb{P}^{\mathcal{M}_{1}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}_{2}}(\Diamond\alpha)$.

Lemma 4 is a consequence of Corollary 1 and Lemma 2 and states that the maximal and the minimal probability of reaching a given proposition is realized by Markov chains with the same structure than the IMC.

Proof (Lemma 4)

Let $\mathcal{I}$ be an IMC and $\mathcal{M}$ be a MC satisfying $\mathcal{I}$. Consider the sequence of MCs $(\mathcal{M}_{n})_{n\in\mathbb{N}}$ s.t. $\mathcal{M}_{0}$ is the MC satisfying $\mathcal{I}$ with degree $1$ obtained by Corollary 1 and for all $n\in\mathbb{N}$, $\mathcal{M}_{n+1}$ is the MC satisfying $\mathcal{I}$ with strictly less states than $\mathcal{M}_{n}$ and verifying $\mathbb{P}^{\mathcal{M}_{n+1}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}_{n}}(\Diamond\alpha)$ given by Lemma 2 if $\mathcal{M}_{n}$ does not have the same structure than $\mathcal{I}$ and equal to $\mathcal{M}_{n}$ otherwise. By construction $(\mathcal{M}_{n})_{n\in\mathbb{N}}$ is finite and its last element is a Markov chain $\mathcal{M}^{\prime}$ with the same structure than $\mathcal{I}$ s.t. $\mathbb{P}^{\mathcal{M}^{\prime}}(\Diamond\alpha)\leq\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$.∎

Theorem 5.1

Let $\mathcal{I}=(S,s_{0},P,V)$ be an IMC, $\alpha\subseteq A$ be a state label, ${\sim}\in\{\leq,<,>,\geq\}$ and $0<p<1$. $\mathcal{I}$ satisfies $\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$ with the once-and-for-all semantics iff $\mathcal{I}$ satisfies $\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$ with the at-every-step semantics.

Proof

Let $\mathcal{I}=(S,s_{0},P,V)$ be an IMC, $\alpha\subseteq A$ be a state label, ${\sim}\in\{\leq,<,>,\geq\}$ and $0<p<1$. Recall that according to an IMC satisfaction relation the property $\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$ holds iff there exists an MC $\mathcal{M}$ satisfying $\mathcal{I}$ (with the chosen semantics) such that $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha){\sim}p$. Recall also that $\models^{a}_{\tt{I}}$ is more general than $\models^{o}_{\tt{I}}$: for all MC $\mathcal{M}$ if $\mathcal{M}\models^{o}_{\tt{I}}\mathcal{I}$ then $\mathcal{M}\models^{o}_{\tt{I}}\mathcal{I}$

• $[\Rightarrow]$

Direct from the fact that $\models^{o}_{\tt{I}}$ is more general than $\models^{o}_{\tt{I}}$ (cf. Appendix 0.A.1)

• $[\Leftarrow]$

$\mathbb{P}^{\mathcal{I}}(\Diamond\alpha){\sim}p$ with the at-every-step semantics implies that there exists a MC $\mathcal{M}$ s.t. $\mathcal{M}\models^{a}_{\tt{I}}\mathcal{I}$ and $\mathcal{M}{\sim}p$. Thus by Lemma 4 there exists a MC $\mathcal{M}^{\prime}$ s.t. $\mathcal{M}^{\prime}\models^{a}_{\tt{I}}\mathcal{I}$, $\mathcal{M}^{\prime}{\sim}p$, $\mathcal{M}^{\prime}$ has the same structure than $\mathcal{I}$. However if $\mathcal{M}^{\prime}$ has the same structure than $\mathcal{I}$ then $\mathcal{M}^{\prime}$ satisfies $\mathcal{I}$ with the one-and-for-all semantics.

∎

0.C.2 CSP Encodings for Quantitative Reachability

Proposition 5

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC and $\alpha\subseteq A$ be a state label. There exists a MC $\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$ iff there exists a valuation $v$ solution of the CSP ${\bf C^{\prime}_{{\exists}r}}(\mathcal{P},\alpha)$ s.t. for each state $s\in S$: $v(\lambda_{s})$ is equals to $\mathsf{true}$ iff $\mathbb{P}^{\mathcal{M}}_{s}(\Diamond\alpha)\neq 0$.

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC and $\alpha\subseteq A$ be a state label. For each state $s\in S$, the variable $\alpha_{s}$ plays a symmetric role to the variable $\omega_{s}$ from ${\bf C_{{\exists}r}}$: instead of indicating the existence of a path from $s_{0}$ to $s$, it characterizes the existence of a path from $s$ to a state labeled with $\alpha$. As for the ${\bf C_{{\exists}r}}$ CSP encoding, each solution of the CSP ${\bf C_{{\exists}r}}(P,\alpha)$ corresponds to a MC $\mathcal{M}$ satisfying $\mathcal{P}$ w.r.t. $\models^{o}_{\tt{pI}}$. Furthermore the constraints added in ${\bf C^{\prime}_{{\exists}r}}$ ensures that $\alpha_{s}$ is equal to $k$ iff there exists a path of length $k-1$ with non zero probability from $s$ to a state label with $\alpha$ in $\mathcal{M}$. Thus by Constraint (13), variables $\lambda_{s}$ is equal to $\mathsf{true}$ iff there exists a path with non zero probability from the initial state $s_{0}$ to a state labeled with $\alpha$ passing by $s$.

Proposition 6

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC and $\alpha\subseteq A$ be a proposition. There exists a MC $\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$ iff there exists a valuation $v$ solution of the CSP ${\bf C_{{\exists}\bar{r}}}(\mathcal{P},\alpha)$ s.t. $v(\pi_{s})$ is equal to $\mathbb{P}^{\mathcal{M}}_{s}(\Diamond\alpha)$ if $s$ is reachable from the initial state $s_{0}$ in $\mathcal{M}$ and is equal to [math] otherwise.

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC and $\alpha\subseteq A$ be a state label. ${\bf C_{{\exists}\bar{r}}}$ extends the CSP ${\bf C^{\prime}_{{\exists}r}}$ that produces a MC $\mathcal{M}$ satisfying $\mathcal{P}$ (cf. Proposition 5) by computing the probability of reaching $\alpha$ in $\mathcal{M}$. In order to compute this probability, we use standard techniques from [2] that require the partitioning of the state space into three sets $S_{\top}$, $S_{\bot}$, and $S_{?}$ that correspond to states reaching $\alpha$ with probability $1$, states from which $\alpha$ cannot be reached, and the remaining states, respectively. Once this partition is chosen, the reachability probabilities of all states in $S_{?}$ are computed as the unique solution of an equation system (see [2], Theorem 10.19, p.766). Recall that for each state $s\in S$ variable $\alpha_{s}$ is equal to $\mathsf{true}$ iff $s$ is reachable in $\mathcal{M}$ and $s$ can reach $\alpha$ with a non zero probability. Thus we consider $S_{\bot}=\{s\ |\ \alpha_{s}=\mathsf{false}\}$, $S_{\top}=\{s\ |\ V(s)=\alpha\}$, and $S_{?}=S\setminus(S_{\bot}\cup S_{\top})$. Finally constraints in ${\bf C_{{\exists}\bar{r}}}$ encodes the equation system from [2] according to chosen $S_{\bot}$, $S_{\top}$, and $S_{?}$. Thus $\pi_{s_{0}}$ is equal to the probability in $\mathcal{M}$ to reach $\alpha$.

Theorem 5.2.

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC, $\alpha\subseteq A$ be a label, $p\in[0,1]$, ${\sim}\in\{\leq,<,\geq,>\}$ be a comparison operator, and $(X,D,C)$ be ${\bf C_{{\exists}\bar{r}}}(\mathcal{P},\alpha)$:

• •

CSP $(X,D,C\cup(\pi_{s_{0}}\sim p))$ is satisfiable iff $\exists\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$ s.t. $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\sim p$

• •

CSP $(X,D,C\cup(\pi_{s_{0}}\not\sim p))$ is unsatisfiable iff $\forall\mathcal{M}\models^{a}_{\tt{pI}}\mathcal{P}$: $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\sim p$

Let $\mathcal{P}=(S,s_{0},P,V,Y)$ be a pIMC, $\alpha\subseteq A$ be a state label, $p\in[0,1]$, and ${\sim}\in\{\leq,<,\geq,>\}$ be a comparison operator. Recall that ${\bf C_{{\exists}\bar{r}}}(\mathcal{P},\alpha)$ is a CSP s.t. each solution corresponds to a MC $\mathcal{M}$ satisfying $\mathcal{P}$ where $\pi_{s_{0}}$ is equal to $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)$. Thus adding the constraint $\pi_{s_{0}}\sim p$ allows to find a MC $\mathcal{M}$ satisfying $\mathcal{P}$ s.t. $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\sim p$. This concludes the first item presented in the theorem. For the second item, we use Theorem 5.1 with the Proposition 6 which ensure that if the CSP ${\bf C_{{\exists}\bar{r}}}(\mathcal{P},\alpha)$ plus the constraint $\pi_{s_{0}}\not\sim p$ is not satisfiable then there is no MC satisfying $\mathcal{P}$ w.r.t. $\models^{a}_{\tt{pI}}$ s.t. $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\not\sim p$; thus $\mathbb{P}^{\mathcal{M}}(\Diamond\alpha)\sim p$ for all MC satisfying $\mathcal{P}$ w.r.t. $\models^{a}_{\tt{pI}}$.