Quantitative Analysis of Interval Markov Chains

Abstract

Interval Markov chains (IMCs), as first introduced by Larsen and Jonsson in 1991 are succinct specifications for probabilistic systems that generalise Markov chains (MCs) by allowing state transition probabilities to lie within an interval. In this work, we address the study of IMCs in a quantitative setting by extending the notion of IMCs by associating with each state a reward that is gained when leaving the state. Specifically, we compare three different semantic interpretations proposed in the literature (once-and-for-all, interval Markov decision process and at-every-step) in the context of model-checking rPCTL, an extension of PCTL where each path-formula is equipped with the specification of a bound on the accumulated reward. We prove that for the full logic, the three semantics are not equivalent, but for the fragment of reward-bounded reachability properties, the interval Markov decision process semantics and the at-every-step semantics are equivalent. Finally, we discuss model-checking algorithms for the three semantics by reduction to the model-checking problem for parametric Markov chains.

1 Introduction

The early work of Bengt Jonsson contains several contributions to the verification of distributed systems [20]. This still very active research direction [7] has been dominated by two schools: the North American school stressing automata and temporal logics, and the European school with focus on process algebra and behavioural equivalences. Both directions have their pros and cons with respect to compositionality and refinement: in the process algebraic approach compositional reasoning was guaranteed by congruence properties of the considered equivalences. However, specifications are typically very explicit being single equivalence classes leaving no room for a stepwise refinement process. In contrast, in the temporal logic approach logical implication between specifications provides the basis for stepwise refinement. However, it is notoriously hard to derive logical properties of composite systems from properties of their components, see [2, 30]. Within the process algebraic approach, the introduction of Modal Transition Systems [27] (MTS) may be seen as a step towards support of a true stepwise refinement process. In MTS the transitions of a labelled transition system are classified as either mandatory (must) of optional (may) leading to a modal refinement precongruence generalizing the strict behavioural equivalences.

At the same time, probabilistic extensions of process algebra were introduced, e.g. [15], including the introduction of probabilistic bisimulation [25, 26]. In collaboration with the last author of this paper (during a nice sabbatical at SICS in 1990), Bengt Jonsson quickly followed up with a probabilistic extension of MTS [22], originally termed Probabilistic Specifications, but by now better known as Interval Markov Chains (IMC). It is fair to say that IMC has inspired much subsequent research (including this paper).

On the temporal logical side, the introduction of PCTL in the seminal paper [17, 21] by Bengt Jonsson and Hans Hansson is by now considered a prime logic for specifying properties of probabilistic systems. Since its introduction significant effort has been made towards efficient model checking algorithms for PCTL. However, there are still open problems foremost the question of decidability of satisfiability. One research direction that we will pursue in this paper is that of model checking PCTL with respect to IMC.

Our Contribution. We consider interval Markov reward models (IMRMs), a class of models that extend interval Markov chains by assigning a (positive) reward to each state. For regular IMCs, three distinct semantics have been proposed in the literature: the once-and-for-all semantics [5], the interval Markov decision process (IMDP) semantics [5, 8, 29] and the at-every-step semantics [22]. We provide a natural extension of the three semantics to IMRMs and investigate the differences between the three semantics in the context of model-checking. For this we consider the logic Probabilistic CTL (PCTL) [18] with reward-bounded path-formulae (rPCTL). For a given fragment of the logic, we say that two semantics are equivalent if for some IMRM specification and rPCTL formula, whenever there exists a satisfying model of one semantics, there exists a satisfying model of the other semantics.

Our contribution is twofold. The first part of the paper concerns the comparison of the above mentioned semantics:

• (i) we prove that the three semantics are not equivalent with respect to the full fragment of rPCTL;

• (ii) if one restricts the attention to probabilistic bounded reachability queries (a) we show that the once-and-for-all semantics and the IMDP-semantics are not equivalent, whereas (b) the IMDP-semantics and at-every-step semantics are.

The result in (i) can be seen as a generalisation of a similar result by Bart et al. [5] for IMCs against PCTL properties. In contrast to [5], where three IMCs semantics where shown to be equivalent with respect to reachability queries, we show that such an equivalence does not generalise to IMRMs.

In the second part of the paper we present algorithms for model-checking IMRMs for the three semantics. For the full logic and the once-and-for-all semantics, we present a reduction to the (existential) model-checking problem for parametric Markov reward models [1] with interval-constraints on the parameters. As for the IMDP semantics, we devise a reduction to the model-checking problem of IMRMs using the once-and-for-all semantics.

Notably, thanks to the semantic equivalence result relative to reachability queries mentioned earlier, such a reduction solves also the model checking problem against reachability queries when one interprets IMRMs using the at-every-step semantics. However, model checking generic rPCTL properties with respect to the at-every-step semantics still remains an open problem. Related Work. Since their introduction by Jonsson and Larsen [22], IMCs have been investigated from different perspectives. In particular, [12, 13] tackles the computational complexity of several decision problems, such as deciding whether or not an IMC has an implementation (the consistency problem) and whether the set of implementations of one IMC is entailed by the set of implementation by another IMC (thorough refinement). For model-checking, [6] considers LTL model-checking w.r.t IMCs with the once-and-for-all semantics, while [8, 29] presents algorithms for verifying PCTL properties for both the once-and-for-all semantics as well as the IMDP semantics. The work in [8] also considers general $\omega$-regular properties. From a computational complexity perspective, Chen et al. [9] proved that the two variants of the PCTL model-checking problem w.r.t. the once-and-for-all semantics and the IMDP semantics are both P-complete.

Another body of research is the work on parametric IMCs (PIMCs) [5, 11, 14, 28] where, instead of an interval, one can instead place a parameter. All the problems for IMCs can then be re-cast in two variants for PIMCs, depending on the quantification over the parameters (existential or universal). Closest to our work is [5], in which the equivalence between the three different semantics is investigated for IMCs. In the same paper, verifying a probabilistic reachability property for a given PIMCs is reduced to solving a constraint satisfaction problem.

2 Preliminaries and Notation

We denote by $\mathbb {R}$, $\mathbb {Q}$, and $\mathbb {N}$ respectively the set of real, rational, and natural numbers. Given a binary relation $R \subseteq X \times Y$ and $x \in X$, we define the projection of R on x as $R(x) = \{ y \in Y \mid (x,y) \in R\}$, and we denote by $R^{-1}$ the inverse of R, i.e., $R^{-1} = \{ (y,x) \mid (x,y) \in R \}$.

For a finite nonempty set X, $\mu :X \rightarrow [0,1]$ is a probability distribution on X if $\sum _{x \in X} \mu (x) = 1$. Moreover $\mu$ is extended to sets $Y \subseteq X$ as $\mu (Y) = \sum _{y \in Y} \mu (y)$. We write $\mathcal {D}(X)$ for the set of probability distributions on X. For $\mu \in \mathcal {D}(X)$ we define the support of $\mu$ as $\mathtt {support}(\mu ) = \{x \in X \mid \mu (x) > 0 \}$.

3 Markov Reward Models

In this section we recall the definitions of Markov reward model (MRM), probabilistic reward bisimulation, and Reward-Bounded Probabilistic CTL (rPCTL).

For the rest of the paper, we fix a countable set of atomic propositions A.

Definition 1 (Markov Reward Model)

A Markov reward model is a tuple $\mathcal {M} = (S, s_0, \pi , \rho , \ell )$ consisting of a finite set of states S, an initial state $s_0 \in S$, a transition probability function $\pi :S \rightarrow \mathcal {D}(S)$, a state-reward function $\rho :S \rightarrow \mathbb {N}_{> 0}$ assigning to each state a positive reward¹ and a labelling function $\ell :S \rightarrow 2^{A}$ mapping states to atomic propositions.

Intuitively, if $\mathcal {M}$ is in state s it moves to state $s'$ with probability $\pi (s)(s')$, thereby receiving the reward $\rho (s)$. In this sense $\mathcal {M}$ can be seen as a state-machine that generates paths of states starting from the initial state $s_0$.

We denote by $G_{\mathcal {M}} = (S, \rightarrow )$ the underlying labelled graph of $\mathcal {M}$, where $s, s' \in S$ are connected by a labelled directed edge $s \xrightarrow {p,r} s'$ if and only if $p = \pi (s)(s') > 0$ and $r = \rho (s)$. We will assume without loss of generality that all states of $\mathcal {M}$ are reachable from the initial state $s_0$ in its underlying graph. For $s \in S$ we define the set of successors of s as $\mathtt {succ}(s) = \mathtt {support}(\pi (s))$.

Fig. 1.

IMRM $\mathcal {I}_1$ and implementations , and .

Example 1

Figures 1b–d depicts three MRMs. Consider the MRM $\mathcal {M}_o = (T_o,t_0,\pi _o,\rho _o,\ell ^{\mathcal {M}_o})$ in Fig. 1b. States $T_o = \{t_i \mid 0 \le i \le 4\}$ are visualised by a circle split in two, with the name of a state $t_i$ at the top and the reward $\rho _o(t_i)$ at the bottom. The initial state $t_0$ is identified by a double-stroke border. State labels $\ell ^{\mathcal {M}_o}(t_i)$ are visualised next to the state $t_i$ unless the set is empty, in which case the set is omitted. From the underlying graph $G_{\mathcal {M}_o}$ we have $\mathtt {succ}(t_0) = \{t_1,t_2\}$, $t_0 \xrightarrow {0.3, 1} t_1$ and $t_0 \xrightarrow {0.7, 1} t_2$.

A path is an infinite sequence of states $\sigma = s_0,s_1, \ldots \in S^\omega$; for $j \in \mathbb {N}$, we denote by $\sigma [j]$ the $(j+1)$-th state of $\sigma$, i.e., $\sigma [j] = s_j$ and by $\mathcal {W}(\sigma )(j) = \sum _{i = 0}^{j-1} \rho (s_i)$ the accumulated reward of $\sigma$ after j transitions. For a finite path $\sigma = s_0, \ldots , s_j \in S^*$ we define the length of $\sigma$ as $|\sigma | = j$.

To associate probabilities to measurable events, we adopt the classical cylinder set construction from [4, Chapter 10]. For $w \in S^*$, the cylinder set of w is the set of all paths having prefix w, i.e., $cyl (w) = wS^\omega$. Given an initial probability distribution $\iota \in \mathcal {D}(S)$, we define the probability space $(S^\omega , \Sigma _\mathcal {M}, \mathbb {P}^{\mathcal {M}}_\iota )$, where $\Sigma _\mathcal {M}$ is the smallest $\sigma$-algebra that contains all the cylinder sets, and $\mathbb {P}^{\mathcal {M}}_\iota$ is the unique probability measure such that, for all $w = s_0 \cdots s_n \in S^*$,

$$\begin{aligned} \mathbb {P}^{\mathcal {M}}_\iota ( cyl (w)) = \iota (s_0) \cdot \textstyle \prod _{0 \le i < n} \pi (s_i)(s_{i+1}) \, . \end{aligned}$$

When $\iota$ is the Dirac distribution pointed at s, i.e. $\iota (s) = 1$, we write $\mathbb {P}^{\mathcal {M}}_s$, or just $\mathbb {P}_s$ when $\mathcal {M}$ is clear from the context. Similarly, we may write $\mathbb {P}^{\mathcal {M}}$ as a shorthand for $\mathbb {P}^{\mathcal {M}}_{s_0}$ when $s_0$ is the initial state of $\mathcal {M}$.

Definition 2 (Bisimulation)

Let $\mathcal {M} = (S, s_0, \pi , \rho , \ell )$ be an MRM. An equivalence relation $\mathcal {R} \subseteq S \times S$ is a probabilistic reward bisimulation for $\mathcal {M}$ if whenever $(s,t) \in \mathcal {R}$, then (i) $\rho (s) = \rho (t)$, (ii) $\ell (s) = \ell (t)$, and (iii) $\pi (s)(C) = \pi (t)(C)$ for all $C \in S_{/\mathcal {R}}$.

Two states $s,s' \in S$ are probabilistic bisimilar, written $s \sim s'$, if they are related by some probabilistic bisimulation. By abuse of notation we may write $\mathcal {M} \sim \mathcal {M'}$ to indicate that the initial states of the MRMs $\mathcal {M}$ and $\mathcal {M'}$ are bisimilar w.r.t. their disjoint union.

We now present an extension of probabilistic CTL (PCTL) [18], namely reward-bounded PCTL (rPCTL), where the next and the until operators are equipped with the specification of a finite bound on the accumulated reward. As any CTL-based logic, rPCTL allows for state formulae describing properties about states in an MRM and path formulae describing properties about paths in an MRM. State formulae $\varPhi$ and path formulae $\varPsi$ are formed according to the following abstract syntax:

$$\begin{aligned} \varPhi&\,::=\, \text{ true } \mid a \mid \lnot \varPhi \mid \varPhi \wedge \varPhi \mid \mathcal {P}_{\bowtie \lambda }(\varPsi )\\ \varPsi&\,::=\, \textsf {X}_{\unlhd k} \, \varPhi \mid \varPhi \, \textsf {U}_{\unlhd k} \,\varPhi \end{aligned}$$

where $a \in A$, ${\bowtie } = \{<,\le ,\ge ,>\}$, $\unlhd = \{\le ,=, \ge \}$, $\lambda \in \mathbb {Q} \cap [0,1]$, and $k \in \mathbb {N}$. We denote by $\mathtt {rPCTL}$ the set of all rPCTL state-formulae.

Given an MRM $\mathcal {M}= (S, s_0, \pi , \rho , \ell )$, a state $s \in S$, and a path $\sigma \in S^\omega$, we write $\mathcal {M}, s \,\models \, \varPhi$ (resp. $\mathcal {\mathcal {M}}, \sigma \,\models \, \varPsi$) to indicate that s satisfies the state formula $\varPhi$ (resp. the path $\sigma$ satisfies the path formula $\varPsi$). The satisfiability relation $\models$ is inductively defined as:

As usual, we derive the operators $\text{ false }$, $\vee$, and $\rightarrow$ as $\text{ false } \mathrel {:=}\lnot \text{ true }$, $\varPhi _1 \vee \varPhi _2 \mathrel {:=}\lnot (\lnot \varPhi _1 \wedge \lnot \varPhi _2)$, and $\varPhi _1 \rightarrow \varPhi _2 \mathrel {:=}\lnot \varPhi _1 \vee \varPhi _2$. Moreover, we define the k-bounded reachability operator as $\lozenge _{\unlhd k} \varPhi \mathrel {:=}\text{ true }\, \textsf {U}_{\unlhd k} \,\varPhi$.

The satisfiability relation extends naturally to finite paths: a finite path $\sigma \in S^*$ satisfies a path-formula $\varPsi$ if and only if all the infinite paths in the cylinder-set $cyl (\sigma )$ satisfy $\varPsi$. If the MRM is clear from the context, we sometimes write $s \,\models \, \varPhi$ instead of $\mathcal {M}, s \,\models \, \varPhi$. We may also write $\mathcal {M} \,\models \, \varPhi$ as a shorthand for $\mathcal {M}, s_0 \,\models \, \varPhi$ and $\mathbb {P}^{\mathcal {M}}(\varPsi )$ as a shorthand for $\mathbb {P}_{s_0}^{\mathcal {M}}(\{\sigma \in S^{\omega } \mid \mathcal {M},\sigma \,\models \, \varPsi \})$, where $s_0$ is the initial state of $\mathcal {M}$.

Example 2

Consider the three MRMs $\mathcal {M}_o,\mathcal {M}_d$ and $\mathcal {M}_a$ depicted in Figs. 1b–d and let $\varPhi = \mathcal {P}_{\ge 0.15}(\lozenge _{\le 3} \,b)$. By rPCTL semantics we have $\mathcal {M}_o \,\models \, \varPhi$, witnessed by the path $t_0,t_1,t_4$ and similarly, $\mathcal {M}_d \,\models \, \varPhi$ and $\mathcal {M}_a \,\models \, \varPhi$. If the probability threshold is increased from 0.15 to 0.3, $\mathcal {M}_o$ and $\mathcal {M}_d$ no longer satisfy the formula, i.e. for formula $\varPhi ' = \mathcal {P}_{\ge 0.3}(\lozenge _{\le 3} \,b)$, we have $\mathcal {M}_o \,\not \models \, \varPhi '$, $\mathcal {M}_d \,\not \models \, \varPhi '$ but $\mathcal {M}_a \,\models \, \varPhi '$.

For $s,s' \in S$, we say that s and $s'$ are logically equivalent w.r.t. rPCTL, written $s \cong _{\mathtt {rPCTL}} s'$, if

$$\begin{aligned} \forall \varPhi \in \mathtt {rPCTL}. \, \mathcal {M}, s \,\models \, \varPhi \iff \mathcal {M}, s' \,\models \, \varPhi \,. \end{aligned}$$

The following theorem states that probabilistic bisimilarity equals logical equivalence w.r.t rPCTL.

Theorem 1

Let $\mathcal {M}= (S, s_0, \pi , \rho , \ell )$ be an MRM and $s,s' \in S$. Then, $s \sim s' \iff s \cong _{\mathtt {rPCTL}} s'$.

4 Interval Markov Reward Models

In this section we introduce the notion of interval Markov reward model (IMRM) and present three distinct semantic interpretations of IMRMs, comparing their expressivity with respect to rPCTL.

Before defining IMRMs, it is convenient to introduce some notation. We write $\mathbb {I}$ for the set of all non-empty closed interval subsets of [0, 1], and $\mathcal {D}_{\mathbb {I}}(X) = \{ f \mid f :X \rightarrow \mathbb {I}\}$ denotes the set of interval specifications on a finite set X. An interval specification $f \in \mathcal {D}_{\mathbb {I}}(X)$ describes a family of probability distributions on X that satisfy the specification i.e., $\llbracket f \rrbracket = \{\pi \in \mathcal {D}(X) \mid \forall x \in X. \pi (x) \in f(x)\}$.

Definition 3 (Interval Markov Reward Model)

An interval Markov reward model (IMRM) is a tuple $\mathcal {I}= (S, s_0, \varPi ,R,\ell )$ where

• S is a finite nonempty set of states,

• $s_0 \in S$ is the initial state,

• $\varPi :S \rightarrow \mathcal {D}_{\mathbb {I}}(S)$ is the interval transition function,

• $R :S \rightarrow \mathbb {N}_{> 0}$ is the state-reward function, and

• $\ell :S \rightarrow 2^{A}$ is the state-labeling function.

Given an IMRM $\mathcal {I}= (S, s_0, \varPi , R, \ell )$ and state $s \in S$, $\varPi (s) = I_s$ is the interval-specification for state s, defining for each state $s' \in S$ a probability interval $I_s(s')$, within which s moves to $s'$. By abuse of notation we may refer to MRMs as particular cases of IMRMs having singleton intervals specifications. Hence, an IMRM $\mathcal {I}$ is a succinct specification for a family of MRMs where the transition function satisfies boundary conditions dictated by the interval transition function $\varPi$. Hereafter, we will assume that all IMRMs we will be working with have non-empty interval specifications, i.e., $\llbracket \varPi (s) \rrbracket \ne \emptyset$ for all $s \in S$. In literature this condition is known as (local) consistency [13]. The definition of paths, finite paths and accumulated weight are defined similarly as for MRMs.

Example 3

Consider the IMRM $\mathcal {I}_1 = (S, s_0, \varPi , R, \ell ^{\mathcal {I}})$ depicted in Fig. 1a. For any state $s_i \in \{s_0,s_1,s_2,s_3,s_4\}$, the interval specification $\varPi (s_i)$ is depicted by edges connecting $s_i$ to states in $\mathtt {succ}(s_i)$. These edges are labelled by the interval assigned by $\varPi (s_i)(s_j)$. Singleton intervals [p, p] are simply represented by p.

In the literature [5, 8, 22, 29], there have been proposed three different semantic interpretations of IMRMs, namely, the once-and-for-all semantics, the interval Markov decision process semantics (IMDP), and the at-every-step semantics. We now present the three distinct semantics for IMRMs and some basic results showing the relationship among the different semantics. To ease the presentation, we fix an MRM $\mathcal {M} = (T, t_0, \pi , \rho , \ell ^{\mathcal {M}})$ and an IMRM $\mathcal {I} = (S, s_0, \varPi , R, \ell ^{\mathcal {I}})$ and we will implicitly refer to their components in the remainder of this section.

The once-and-for-all semantics [5], also called the Uncertain Markov Chain semantics [29] is the simplest among the three semantics. It requires to choose for each state of the IMRM a probability distribution satisfying the corresponding interval specification.

Definition 4 (Once-and-for-all semantics)

An arbitrary MRM $\mathcal {M}$ satisfies the IMRM $\mathcal {I}$ w.r.t. the once-and-for-all semantics, written $\mathcal {M} \,\models _o\, \mathcal {I}$, if and only if $T \subseteq S$, $t_0 = s_0$, and for all $t \in T$, $\rho (t) = R(t)$, $\ell ^{\mathcal {M}}(t) = \ell ^{\mathcal {I}}(t)$, and $\pi (t) \in \llbracket \varPi (t) \rrbracket$.

Example 4

Consider again the IMRM $\mathcal {I}_1$ in Fig. 1a. Figure 1b depicts an MRM $\mathcal {M}_o$ that satisfies $\mathcal {I}_1$ with the once-and-for-all semantics.

In contrast to the once-and-for-all semantics, in the interval Markov decision process semantics (IMDP semantics) [5, 8, 29], the choice of the transition probability distribution for a state $s \in S$ is performed each time a state is visited.

Definition 5 (IMDP semantics)

An MRM $\mathcal {M}$ satisfies the IMRM $\mathcal {I}$ w.r.t. the IMDP semantics, written $\mathcal {M} \,\models _d\, \mathcal {I}$, if and only if there exists a mapping $\tau :T \rightarrow S$ such that $\tau (t_0) = s_0$, and for all $t \in T$, $\ell ^{\mathcal {M}}(t) = \ell ^{\mathcal {I}}(\tau (t))$, $\rho (t) = R(\tau (t))$, and there exists $\delta _t \in \llbracket \varPi (\tau (t)) \rrbracket$ such that for all $t' \in T$, $t' \in \mathtt {succ}(t)$ implies that $\pi (t)(t') = \delta _t(\tau (t'))$.

As its name suggests, the IMDP semantics is reminiscent of the way one resolves nondeterminism in a Markov decision process (MDP) by means of a deterministic memory-dependent scheduler (cf. [4, Ch10]). With respect to similar semantic interpretations given for interval Markov chains [5, 8, 29], Definition 5 is more similar in spirit to that given in [5] for the fact that the MRM $\mathcal {M}$ needs to be finite.

Example 5

The MRM in Fig. 1c satisfies the IMRM $\mathcal {I}_1$ in Fig. 1a w.r.t. the IMDP semantics. To see this, consider the mapping $\tau (u_0) = s_0, \tau (u_1) = s_1, \tau (u_{21}) = \tau (u_{22}) = s_2, \tau (u_3) = s_3$ and $\tau (u_4) = s_4$. Note that $u_{21}$ and $u_{22}$ are two different implementations of the IMRM state $s_2$.

Remark 1

Notice that $\mathcal {M} \,\models _o\, \mathcal {I}$ implies $\mathcal {M} \,\models _d\, \mathcal {I}$ and the mapping $\tau :T \rightarrow S$ witnessing this fact is the identity function, i.e., $\tau (t) = t$ for all $t \in T$.

The last semantic interpretation for IMRMs is the so-called at-every-step semantics. Its definition is a simple extension of the original semantics given for interval Markov chains by Jonsson and Larsen [22]. Its main feature consists in generalizing the mapping $\tau :T \rightarrow S$ from the IMDP semantics to a relation $\mathcal {R} \subseteq T \times S$. This allows one to “aggregate” compatible states of the IMRM into a single state of the MRM implementation, as well as “redistributing” the successors of a state of the IMRM into multiple states.

Definition 6 (At-every-step semantics)

An MRM $\mathcal {M}$ satisfies the IMRM $\mathcal {I}$ w.r.t. the at-every-step semantics, written $\mathcal {M} \,\models _a\, \mathcal {I}$ if and only if there exists a relation $\mathcal {R} \subseteq T \times S$ such that $(t_0, s_0) \in \mathcal {R}$ and for all pairs $(t,s) \in \mathcal {R}$ we have that $\ell ^{\mathcal {M}}(t) = \ell ^{\mathcal {I}}(s)$, $\rho (t) = R(s)$, and there exists a correspondence function $\delta _{(t,s)} :T \rightarrow (S \rightarrow [0,1])$ such that

• 1. for all $t' \in \mathtt {succ}(t)$, $\delta _{(t,s)}(t') \in \mathcal {D}(S)$.

• 2. for all $s' \in S$,

  $$\begin{aligned} \left( \sum _{t' \in T} \pi (t)(t') \cdot \delta _{(t,s)}(t')(s')\right) \in \varPi (s)(s'). \end{aligned}$$

• 3. for all $(t',s') \in T \times S$, if $\delta _{(t,s)}(t')(s') > 0$ then $(t',s') \in \mathcal {R}$.

Example 6

The MRM $\mathcal {M}_a$ depicted in Fig. 1d is one possible at-every-step implementation of the IMRM $\mathcal {I}_1$ of Fig. 1a. This is witnessed by the relation

$$\begin{aligned} \mathcal {R} = \{&(v_0,s_0),(v_1,s_1),(v_1,s_2),\\&(v_{31},s_3),(v_{32},s_3),(v_4,s_4)\} \end{aligned}$$

and the following correspondence functions:

$$\begin{aligned}&\delta _{(v_0,s_0)}(v_1)(s_1) = \delta _{(v_0,s_0)}(v_1)(s_2)= \tfrac{1}{2} \,, \\&\delta _{(v_1,s_1)}(v_{31})(s_3) = \delta _{(v_1,s_1)}(v_{32})(s_3) = 1. \end{aligned}$$

Note that the state $v_1$ in $\mathcal {M}_a$ implements both $s_1$ and $s_2$, while the state $s_3$ is “redistributed” into $v_{31}$ and $v_{32}$. The example illustrates that one is allowed to aggregate and split states under the at-every-step semantics.

As shown in Example 6, the at-every-step semantics allows one MRM state to implement multiple IMRM states by aggregation. Next, we show that for any MRM with such aggregated states, there exists an at-every-step implementation with no aggregated states, which is probabilistic bisimilar to the MRM with aggregated states. The result follows immediately from a similar result for IMCs as presented in [5, Proposition 5]. To formalize the result, we borrow the notion of degree of satisfaction from [5].

Definition 7

Let $n \in \mathbb {N}$. The MRM $\mathcal {M}$ satisfies the IMRM $\mathcal {I}$ w.r.t. the at-every-step semantics with degree of satisfaction n, written $\mathcal {M} \,\models _a^n\, \mathcal {I}$, if there exists a relation $\mathcal {R} \subseteq T \times S$ witnessing $\mathcal {M} \,\models _a\, \mathcal {I}$ such that $|\mathcal {R}(t)| \le n$ for all states $t \in T$.

Note that if an MRM $\mathcal {M}$ satisfies IMRM $\mathcal {I}$ with degree 1, all correspondence functions $\delta _{(t,s)}$ are Dirac distributions i.e. $\delta _{(t,s)}(t')(s') > 0 \implies \delta _{(t,s)}(t')(s') = 1$.

The following Lemma states that for any at-every-step implementation $\mathcal {M}$ of the IMRM $\mathcal {I}$, there exists an at-every-step implementation $\mathcal {M'}$ of $\mathcal {I}$ with degree 1 that is probabilistic bisimilar to $\mathcal {M}$.

Lemma 1

Let $\mathcal {M}\,\models _a^n\, \mathcal {I}$ for some $n \in \mathbb {N}$. Then, there exists an MRM $\mathcal {M}'$ such that $\mathcal {M}\sim \mathcal {M}'$ and $\mathcal {M}' \,\models _a^1\, \mathcal {I}$.

Remark 2

Note that $\mathcal {M}\,\models _d\, \mathcal {I}$ implies $\mathcal {M}\,\models ^1_a\, \mathcal {I}$, since the mapping $\tau :T \rightarrow S$ witnessing $\mathcal {M}\,\models _d\, \mathcal {I}$ induces a functional relation $\mathcal {R} = \{ (t, \tau (t)) \mid t \in T\}$ which can be easily verified to be a witness for $\mathcal {M}\,\models ^1_a\, \mathcal {I}$.

The following result identifies the properties that a relation $\mathcal {R}$ witnessing $\mathcal {M}\,\models _a\, \mathcal {I}$ has when the MRM $\mathcal {M}$ satisfies also $\mathcal {M} \,\models _d\, \mathcal {I}$.

Proposition 1

Let $\mathcal {R} \subseteq T \times S$ be a relation witnessing $\mathcal {M} \,\models ^1_a\, \mathcal {I}$. Then, $\mathcal {M} \,\models _d\, \mathcal {I}$ iff for all $(t,s) \in \mathcal {R}$ there exists no $s' \in \mathtt {succ}(s)$ such that $|\mathcal {R}^{-1}(s') \cap \mathtt {succ}(t)| > 1$.

We are now ready to establish some basic relationship between the three semantics in terms of their expressivity. For any semantics $x \in \{o,d,a\}$, we denote by the family of MRMs that satisfy the IMRM $\mathcal {I}$ with respect to the semantic x.

The following result states that the three semantics presented in this section have different expressivity, with the at-every-step semantics being the most expressive semantics, followed by the IMDP semantics which in turn is more expressive than the once-and-for-all semantics.

Proposition 2

For any IMRM $\mathcal {I}$, and for some IMRM $\mathcal {I'}$ these inclusions are strict, i.e., .

Proof

and follow for the arguments sketched respectively in Remarks 1 and 2. For the IMRM $\mathcal {I}_1$ in Fig. 1 in particular it holds that and .    $\square$

5 Comparing Semantics Against rPCTL

In this section we investigate the IMRM semantics presented in Sect. 4 in the context of rPCTL model-checking. The rPCTL satisfiability relation naturally extends to IMRMs by requiring that an rPCTL formula is satisfied by some MRM implementation.

Definition 8

We say that an IMRM $\mathcal {I}$ (existentially) satisfies the formula $\varPhi \in \mathtt {rPCTL}$ with respect to the semantics $x \in \{o,d,a\}$, written $\mathcal {I} \,\models _x\, \varPhi$, iff there exists such that $\mathcal {M} \,\models \, \varPhi$.

The above definition is implicitly given in terms of the initial state $s_0$ of $\mathcal {I}$, but can be generalized to arbitrary states $s \in S$, as $\mathcal {I},s \,\models \, \varPhi$ by replacing $s_0$ with s.

In the following, we compare the three different semantics with respect to different classes of rPCTL formulae. To this end introduce a notion of semantic equivalence.

Definition 9 (Semantic equivalence)

For a fragment of rPCTL, $\mathcal {L} \subseteq \mathtt {rPCTL}$ and two IMRM semantics $x,y \in \{o,d,a\}$, we say that the semantics x and y are equivalent w.r.t. $\mathcal {L}$ if for any IMRM $\mathcal {I}$ and state formula $\varPhi \in \mathcal {L}$, $\mathcal {I}\,\models _x\, \varPhi \iff \mathcal {I}\,\models _y\, \varPhi$.

The next result states that the at-every-step semantics is not equivalent to the IMDP semantics w.r.t. the full logic.

Proposition 3

The at-every-step semantics is not semantically equivalent to the IMDP semantics with respect to $\mathtt {rPCTL}$.

Proof

Consider the IMRM $\mathcal {I}_2$ and MRM $\mathcal {M}_2$ depicted in Fig. 2. One can verify that $\mathcal {M}_2 \,\models _a\, \mathcal {I}_2$. Let $\varPhi$ be the following rPCTL formula

$$\begin{aligned} \varPhi&= \mathcal {P}_{> 0}(\textsf {X}_{\le 1} \varPhi _1) \wedge \mathcal {P}_{> 0}(\textsf {X}_{\le 1} \varPhi _2) \wedge \mathcal {P}_{> 0}(\textsf {X}_{\le 1} \varPhi _3), \end{aligned}$$

where

$$\begin{aligned} \varPhi _1&= \mathcal {P}_{\ge 1}(\textsf {X}_{\le 1} (\lnot \varGamma \wedge \lnot \Lambda )), \,\, \varPhi _2 = \mathcal {P}_{\ge 1}(\textsf {X}_{\le 1} \varGamma )\, \text { and } \varPhi _3 = \mathcal {P}_{\ge 1}(\textsf {X}_{\le 1} \Lambda ). \end{aligned}$$

Clearly $\mathcal {M}_2 \,\models \, \varPhi$ as the three outgoing transitions serve to satisfy each of the sub-formulae $\varPhi _i$ ($i \in \{1,2,3\}$).

Consider an MRM . By IMDP semantics, $\mathcal {M}'$ must have an initial state with exactly two successors, say $t'_1$ and $t'_2$. Therefore there exists $i \in \{1,2,3\}$ such that $\mathcal {M}', t_j \,\not \models \, \varPhi _i$ for any $j = 1,2$ as no single successor can satisfy each $\varPhi _i$ simultaneously. Hence, $\mathcal {I}_2 \,\not \models _d\, \varPhi$.    $\square$

Fig. 2.

IMRM $\mathcal {I}_2$ with at-every-step MRM implementation $\mathcal {M}_2$

The above result is analogous to [5, Section 4.1], where it was proven that for internal Markov chains the at-every-step semantics and the IMDP semantics are not equivalent with respect to PCTL.

Reachability Queries. In the rest of the section we focus our attention on a semantic comparison relative to reachability queries, namely, formulae of the form $\mathcal {P}_{\bowtie \lambda }(\lozenge _{\unlhd k} \varGamma )$, for arbitrary $\varGamma \in AP$, $k \in \mathbb {N}_{> 0}$, $\lambda \in [0,1]$, ${\bowtie } \in \{<,\le ,\ge ,>\}$, and ${\unlhd } \in \{\le , \ge \}$. We denote by $\mathcal {L}_{\mathtt {reach}}$ the set of reachability queries and we write $\mathcal {L}_{\mathtt {reach}}^{\le }$ (resp. $\mathcal {L}_{\mathtt {reach}}^{\ge }$) when we fix ${\unlhd } = {\le }$ (resp. ${\unlhd } = {\ge }$).

Reachability properties are one of the fundamental questions for the quantitative analysis of systems. The atomic proposition $\varGamma$ may represent a set of certain bad states which should be unlikely to be visited, or dually, a set of good states which should rather be visited with high probability. In the context of interval Markov chains, Bart et al. [5] have shown that the three semantic interpretations are equivalent with respect to reachability queries.

In contrast, the ability to express bounds on the reward accumulated until reaching a some goal state makes the IMPD semantics and the at-every-step semantics, more expressive than the once-and-for-all semantics relative to reachability queries.

Fig. 3.

IMRM $\mathcal {I}_3$

Fig. 4.

MRM $\mathcal {M}_3$ such that $\mathcal {M}_3 \,\models \, \mathcal {P}_{> 0.8}(\lozenge _{\le 3} \varGamma )$

Proposition 4

The once-and-for-all semantics is not equivalent to the IMDP semantics w.r.t. $\mathcal {L}_{\mathtt {reach}}$.

Proof

Consider the IMRM $\mathcal {I}_3$ in Fig. 3 and the formula $\mathcal {P}_{> 0.8}(\lozenge _{\le 3} \varGamma )$. Figure 4 shows witnessed by the mapping $\tau (t_0) = \tau (t_0')= s_0$ and $\tau (t_i) = s_i$ for $1 \le i \le 5$. Clearly $\mathcal {M}_3 \,\models \, \mathcal {P}_{> 0.8}(\lozenge _{\le 3} \varGamma )$.

Figure 5 shows the once-and-for-all MRM implementation of $\mathcal {I}_3$, $\mathcal {M}_4$, that maximizes the probability of reaching $\varGamma$ without exceeding the weight budget of 3. One can see that $\mathcal {M}_4 \,\not \models \, \mathcal {P}_{> 0.8}(\lozenge _{\le 3} \varGamma )$.    $\square$

Fig. 5.

MRM $\mathcal {M}_4$ such that $\mathcal {M}_4 \,\not \models \, \mathcal {P}_{> 0.8}(\lozenge _{\le 3} \varGamma )$

It remains to compare the at-every-step semantics and IMDP semantics w.r.t. reachability queries. To this end we first present two technical lemmas.

Lemma 2

Let $\mathcal {I}$ be an IMRM, , $\varGamma \in AP$, and $k \in \mathbb {N}$. Then, there exist such that $\mathbb {P}^{\mathcal {M}_{\le }}(\lozenge _{\le k} \varGamma ) \le \mathbb {P}^{\mathcal {M}}(\lozenge _{\le k} \varGamma ) \le \mathbb {P}^{\mathcal {M}_{\ge }}(\lozenge _{\le k} \varGamma )$.

Proof (sketch)

By Lemma 1 and Theorem 1 we can assume w.l.o.g. that $\mathcal {M} \,\models _a^1\, \mathcal {I}$. To construct $\mathcal {M}_{\le }$ and $\mathcal {M}_{\ge }$ we proceed in two steps. We present the construction of $\mathcal {M}_{\le }$ and then explain how to adapt it for $\mathcal {M}_{\ge }$.

• (Step 1) We build an MRM $\mathcal {M}'$ from $\mathcal {M}$ by unfolding its structure. The unfolding of each path terminates when its accumulated weight exceeds k or when a state satisfying $\varGamma$ is reached. Then, the last state of each unfolded path, say t, is replaced with an arbitrary once-and-for-all model of $\mathcal {I}$ with initial state t.

  Note that $\mathbb {P}^{\mathcal {M}}(\lozenge _{\le k} \varGamma ) = \mathbb {P}^{\mathcal {M}'}(\lozenge _{\le k} \varGamma )$ since the probability value is obtained as the sum over all the cylinders obtained from paths constructed in the unfolding. Moreover, $\mathcal {M}' \,\models _a^1\, \mathcal {I}$ because $\mathcal {M}\,\models _a^1\, \mathcal {I}$ and the unfolding does not introduce any aggregation.

• (Step 2) From $\mathcal {M}'$ we construct $\mathcal {M}_{\le }$. Let $\mathcal {R}$ be the relation witnessing $\mathcal {M}' \,\models _a^1\, \mathcal {I}$. If $\mathcal {R}$ satisfies the conditions of Proposition 1 we choose $\mathcal {M}' = \mathcal {M}_{\le }$. Otherwise, for each state t of $\mathcal {M}$ such that $(t,s) \in \mathcal {R}$ and $|\mathcal {R}^{-1}(s') \cap \mathtt {succ}(t)| > 1$ for some $s' \in \mathtt {succ}(s)$ we proceed as follows. Let $t' \in \mathcal {R}^{-1}(s') \cap \mathtt {succ}(t)$ be the successor of t that minimizes the probability of reaching $\varGamma$ within the reward bound up to $t'$, i.e., $\mathbb {P}^{\mathcal {M}'}_{t'}(\lozenge _{\le k'} \varGamma )$ where $k' = k - \mathcal {W}(\sigma )(|\sigma |)$ and $\sigma$ is the finite path from the initial state of $\mathcal {M}'$ to $t'$. Then we redirect all the probability mass that was from t to $\mathcal {R}^{-1}(s') \cap \mathtt {succ}(t)$ to the single state $t'$, “disconnecting” the set of states $(\mathcal {R}^{-1}(s') \cap \mathtt {succ}(t)) \setminus \{ t' \}$ from t.

  Let $\mathcal {M}_{\le }$ be the MRM obtained from the above procedure. Note that $\mathcal {M}_{\le }$ satisfies the conditions of Proposition 1 and $\mathbb {P}^{\mathcal {M}_{\le }}(\lozenge _{\le k} \varGamma ) \le \mathbb {P}^{\mathcal {M}'}(\lozenge _{\le k} \varGamma )$.

As for the construction of $\mathcal {M}_{\ge }$, (Step 1) is done in the same way while in (Step 2) $t'$ is chosen as the one that maximizes $\mathbb {P}^{\mathcal {M}'}_{t'}(\lozenge _{\le k'} \varGamma )$.    $\square$

Lemma 3

Let $\mathcal {I}$ be an IMRM, , $\varGamma \in AP$, and $k \in \mathbb {N}$. Then, there exist such that $\mathbb {P}^{\mathcal {M}_{\le }}(\lozenge _{\ge k} \varGamma ) \le \mathbb {P}^{\mathcal {M}}(\lozenge _{\ge k} \varGamma ) \le \mathbb {P}^{\mathcal {M}_{\ge }}(\lozenge _{\le k} \varGamma )$.

Proof (sketch)

The proof proceeds in two steps analogously as for Lemma 2.

By Lemma 1 and Theorem 1 we can assume w.l.o.g. that $\mathcal {M}\,\models _a^1\, \mathcal {I}$. We present the construction of $\mathcal {M}_{\le }$ and then explain how to adapt it for $\mathcal {M}_{\ge }$.

• (Step 1) We build an MRM $\mathcal {M}'$ from $\mathcal {M}$ by unfolding its structure. The unfolding of each path terminates as soon as its accumulated weight exceeded k. Then, the last state of each unfolded path, say t, is replaced with a once-and-for-all model $\mathcal {M}''$ of $\mathcal {I}$ with initial state t such that $\mathbb {P}^{\mathcal {M}''}_{t}(\lozenge \varGamma ) \le \mathbb {P}^{\mathcal {M}}_{t}(\lozenge \varGamma )$. The existence of $\mathcal {M}''$ is guaranteed by [5, Lemma 4].

  Note that $\mathbb {P}^{\mathcal {M}'}(\lozenge _{\ge k} \varGamma ) \le \mathbb {P}^{\mathcal {M}}(\lozenge _{\ge k} \varGamma )$ since the probability value is obtained as the sum over all the cylinders obtained from paths constructed in the unfolding. Moreover, $\mathcal {M}' \,\models _a^1\, \mathcal {I}$ because $\mathcal {M}\,\models _a^1\, \mathcal {I}$ and the unfolding does not introduce any aggregation.

• (Step 2) From $\mathcal {M}'$ we construct $\mathcal {M}_{\le }$ following the same procedure used for (Step 2) in the proof of Lemma 2.

As for the construction of $\mathcal {M}_{\ge }$, in (Step 1) we need to choose $\mathcal {M}''$ such that $\mathbb {P}^{\mathcal {M}''}_{t}(\lozenge \varGamma ) \ge \mathbb {P}^{\mathcal {M}}_{t}(\lozenge \varGamma )$ and (Step 2) is modified as done for Lemma 2.    $\square$

Theorem 2

The IMDP semantics and the at-every-step semantics are equivalent w.r.t. $\mathcal {L}_{\mathtt {reach}}$.

Proof

Let $\mathcal {I}$ be an IMRM, $\varPhi = \mathcal {P}_{\bowtie \lambda }(\lozenge _{\unlhd k} \varGamma ) \in \mathcal {L}_{\mathtt {reach}}$ and $\mathcal {M}\in \llbracket \mathcal {I} \rrbracket _a$ such that $\mathcal {M} \,\models \, \varPhi$. We proceed by cases.

If ${\unlhd } = {\le }$, we consider two sub-cases. If ${\bowtie } \in \{<,\le \}$ then by Lemma 2 there exists such that $\mathbb {P}^{\mathcal {M}_{\le }}(\lozenge _{\le k} \varGamma ) \le \mathbb {P}^{\mathcal {M}}(\lozenge _{\le k} \varGamma )$. Therefore $\mathcal {I}\,\models _d\, \varPhi$. If ${\bowtie } \in \{\ge ,>\}$ then by Lemma 2 there exists $\mathcal {M}_{\ge } \in \llbracket \mathcal {I} \rrbracket _d$ such that $\mathbb {P}^{\mathcal {M}_{\ge }}(\lozenge _{\le k} \varGamma ) \ge \mathbb {P}^{\mathcal {M}}(\lozenge _{\le k} \varGamma )$. Hence $\mathcal {I}\,\models _d\, \varPhi$.

If ${\unlhd } = {\ge }$ we use the same arguments as before by using Lemma 3 in place of Lemma 2.    $\square$

6 Model-Checking Algorithms

In this section we turn our attention to model-checking different fragments of rPCTL. By the results of the previous section, each IMRM semantics requires its own treatment for the full logic rPCTL. For the important fragment of reachability queries in $\mathcal {L}_{\mathtt {reach}}$, we need two algorithms, one for the once-and-for-all semantics and one for the IMDP semantics. In the following, we restrict ourselves to formulae with only upper bounds on path-formulae and similar to $\mathcal {L}_{\mathtt {reach}}^{\le }$, we denote by $\mathtt {rPCTL} ^{\le }$ the set of all rPCTL formulae with only upper bounds on the path formulae.

For the once-and-for-all semantics we reduce the model-checking problem w.r.t $\mathtt {rPCTL} ^{\le }$ to the (existential) model-checking problem for parametric Markov reward models (PMRMs) [1] with interval constraints on the parameters. Efficient procedures for model-checking PMRMs against various logics have received a lot of attention in recent years and are now supported by modern tools such as $\textsc {PRISM}$ [24], $\textsc {PARAM}$ [16] and $\textsc {PROPhESy}$ [10]. For the IMDP semantics we exploit the fact that all rewards are strictly positive to devise a reduction to the model-checking problem for the once-and-for-all semantics. For the at-every-step semantics we leave the model-checking problem for fragments containing $\mathcal {L}_{\mathtt {reach}}^{\le }$ open. We proceed by treating each semantics in turn.

6.1 Once-and-for-all Semantics

For the fragment $\mathtt {rPCTL} ^{\le }$ we present a reduction to the (existential) model-checking problem for PMRMs with interval constraints on the parameters. We first recall the definition of PRMMs and then present the reduction. PMRMs extend MRMs by allowing the transition probabilities to take values in a finite nonempty set P of parameters. Thus, for any finite nonempty set X, the function $\mu _P :X \rightarrow [0,1] \cup P$ is a parametric distribution. The set $\mathcal {D}_P(X)$ is then the set of all parametric distributions.

Definition 10 (Parametric MRM)

A parametric Markov Reward Model (PMRM) is defined as a tuple $\mathcal {M}_P = (S, s_0, \rho , \pi _P, \ell ^{\mathcal {M}})$ where $S, s_0, \rho$ and $\ell ^{\mathcal {M}}$ are defined as for MRMs and for each $s \in S$, $\pi _P \in \mathcal {D}_P(S)$ is the parametric probability transition function.

A given PMRM gives rise to a set of MRMs by interpreting the parameters as rational values and making sure that the resulting distribution are probability distributions (i.e. sum up to 1). Formally, a valuation function $\kappa :\mathbb {Q}_{> 0} \cup P \rightarrow [0,1]$ is a function such that for all $r \in \mathbb {Q}_{> 0}$, $\kappa (r) = r$, for all $p \in P$, $\kappa (p) > 0$ and for all states $s \in S$, $\sum _{s' \in S} \kappa (\pi _P(s)(s'))) = 1$. We abuse notation and for any PMRM $\mathcal {M}_P$ write $\kappa (\mathcal {M}_P)$ for the MRM induced by $\kappa$.

Existential Model-Checking. We consider the following decision problem for PMRMs: given a PMRM $\mathcal {M}_P$ and formula $\varPhi \in \mathtt {rPCTL} ^{\le }$, does there exist a valuation function $\kappa$ such that $\kappa (\mathcal {M}_P) \,\models \, \varPhi$?

The problem is extended with interval-constraints on the parameters as follows: for all $(s,s') \in S \times S$ let $I_{s,s'} = [l_{s,s'},u_{s,s'}] \in \mathbb {I}$ be some interval. The parameter valuation function $\kappa$ must then also satisfy the following constraints:

$$ \bigwedge _{(s,s') \in S \times S} \kappa (\pi _P(s)(s')) \in I_{s,s'}. $$

The Reduction. Let $\mathcal {I}= (S, s_0, \varPi , R, \ell ^{\mathcal {I}})$ be an IMRM and $\varPhi \in \mathtt {rPCTL} ^{\le }$ an arbitrary formula. We now construct a PMRM $\mathcal {M}_P$ and a set of interval constraints such that if there exists a valuation function $\kappa$ where $\kappa (\mathcal {M}_P) \,\models \, \varPhi$, while $\kappa$ satisfies the given interval constraints, then $\mathcal {I}\,\models _o\, \varPhi$.

Let $\mathcal {M}_P$ be the PMRM identical to $\mathcal {I}$ except that each interval $\varPi (s)(s')$ is replaced by a parameter $p_{s,s'}$. For each $p_{s,s'}$, the interval constraint that $\kappa$ must satisfy, is given by $\varPi (s)(s')$ i.e. any parameter valuation function $\kappa$ must satisfy the following interval constraints:

$$ \bigwedge _{(s,s') \in S \times S} \kappa (p_{s,s'}) \in \varPi (s)(s'). $$

Assume that there exists a valuation function $\kappa$ such that $\kappa (\mathcal {M}_P) \,\models \, \varPhi$ in addition to satisfying the above interval constraints. Without loss of generality, we assume that all states in $\kappa (\mathcal {M}_P)$ are reachable as all states of any MRM have to be reachable. If that is not the case, one can simply remove all unreachable states as they do not influence satisfiability. By construction, it is clear that as $\kappa$ induces a probability distribution for each state s that satisfies the interval-specifications $\varPi (s)$ given by $\mathcal {I}$, while preserving rewards and labels of each state.

Interpreting $\mathtt {rPCTL} ^{\le }$ on PMRMs. In literature, papers on PCTL model-checking for PMRMs only consider step-bounded or unbounded until-formulae, in contrast to the reward-bounded until formulae in $\mathtt {rPCTL} ^{\le }$. This is not a restriction since any PMRM that contains a state s with a reward greater than 1 can be replaced by a sequence of states with reward 1. Hence, any upper bound on the formula can be interpreted as a step-bound in this (larger) model. In the same way, it is possible to “unroll” the model to reduce (step)-bounded reachability to unbounded reachability [23, Remark 4]. Thus, any technique for model-checking PCTL where the until is step-bounded or unbounded on PMRMs can be used for $\mathtt {rPCTL} ^{\le }$ [3, 10, 16, 23, 24]. In the case of unbounded until, the model-checking problem for PMRMs is in PSPACE [19].

6.2 IMDP Semantics

Our approach for verifying properties with the IMDP semantics is based on the fact that the IMDP semantics is a simple extension of the once-and-for-all semantics, where one is allowed to choose a different probability distribution each time a state is visited. Recall that every reward in the model is strictly positive and we have concrete upper bounds on all path-formulae. Hence, even if one is allowed to choose a different distribution each time a state is visited, for the purpose of verifying $\varPhi$, we can bound the number of times a different probability distribution needs to be chosen for any IMDP implementation that satisfies $\varPhi$. Hence, one can do a bounded unfolding of the IMRM that preserves interval specifications, to encode all possible implementations that may satisfy $\varPhi$. The unfolding itself is an IMRM, where the set of states is the set of all non-empty finite paths, $S^+$, bounded by a given depth k. Interval-preservation is ensured by letting the transitioning between any two such states be defined by the transitioning between their two last states in the original IMRM.

Definition 11

(IMRM k-unfolding). For any IMRM $\mathcal {I}= (S, s_0, \varPi , R, \ell ^{\mathcal {I}})$ and $k \in \mathbb {N}$, let $\mathcal {I}{\downarrow _{k}} = (S_k, s_0, \varPi _k, R_k, \ell ^{\mathcal {I}{\downarrow _{k}}})$ be the interval specification preserving k-unfolding of $\mathcal {I}$, defined as follows²:

• $\begin{aligned} S_k = \{ \sigma \in S^+ \mid \,&\mathcal {W}(\sigma )(|\sigma |) \le k,\\&\forall _{0 \le i < |\sigma |}. \varPi (\sigma [i],\sigma [i+1]) \ne [0,0]\}.\end{aligned}$

• For all $\sigma \in S_k \cup \{\epsilon \}$³ and $s,s_1 \in S$, $\varPi _k(\sigma s, \sigma s s_1) = \varPi (s,s_1)$.

• For any path $\sigma = s_1, \ldots , s_n$ in $S_k$, $R_k(\sigma ) = R(s_n)$ and $\ell ^{\mathcal {I}{\downarrow _{k}}}(\sigma ) = \ell ^{\mathcal {I}}(s_n)$.

As any MRM $\mathcal {M}$ can be seen as an IMRM with singleton intervals, we abuse notation and write $\mathcal {M}{\downarrow _{k}}$ for the k-unfolding of the MRM $\mathcal {M}$.

The following two lemmas prove two key properties of our unfolding definition. The first lemma states that for an IMRM $\mathcal {I}$ with initial state $s_0$, if any successor $s_0s'$ of $s_0$ in the k-unfolding of $\mathcal {I}$ satisfies a given formula $\varPhi$, then this can be verified by changing the initial state to $s'$ and performing a $(k-R(s_0))$-unfolding of $\mathcal {I}$ where $R(s_0)$ is the reward assigned by $\mathcal {I}$ to $s_0$. The second lemma states that whenever an MRM is an IMDP implementation of an IMRM $\mathcal {I}$ then the k-unfolding of $\mathcal {M}$ is an once-and-for-all implementation of the k-unfolding of $\mathcal {I}$. This implies that if from any formula $\varPhi \in \mathtt {rPCTL} ^{\le }$ we can define a $k \in \mathbb {N}$ such that the k-unfolding of $\mathcal {I}$ includes all the paths needed for verifying $\varPhi$, we can reduce the model-checking problem using the IMDP semantics to model-checking using the once-and-for-all semantics on the k-unfolding of $\mathcal {I}$, $\mathcal {I}{\downarrow _{k}}$.

Lemma 4

For any two IMRMs defined as $\mathcal {I}^{s_0} = (S, s_0, \varPi , R, \ell ^{\mathcal {I}})$ and $\mathcal {I}^{s'} = (S, s', \varPi , R, \ell ^{\mathcal {I}})$ with $s' \in \mathtt {succ}(s_0)$, $k \ge R(s_0)$, $\varPhi \in \mathtt {rPCTL} ^{\le }$ and semantics $x \in \{o,d,a\}$, it holds that

$$ \mathcal {I}^{s_0}{\downarrow _{k}},s_0s' \,\models _x\, \varPhi \implies \mathcal {I}^{s'}{\downarrow _{k - R(s_0)}}, s' \,\models _x\, \varPhi . $$

Proof

The lemma follows easily from the definition of unfolding and rPCTL semantics. The condition $k \ge R(s_0)$ ensures that $s_0s'$ is a state in $\mathcal {I}^{s_0}$.

Lemma 5

For any IMRM $\mathcal {I}$, MRM $\mathcal {M}$ and $k \in \mathbb {N}$, if .

Remark 3

Strictly speaking, Lemma 5 only holds up to isomorphism as $\mathcal {M}$ by the IMDP semantics may contain states not in $\mathcal {I}$. In this case, the states of $\mathcal {M}{\downarrow _{k}}$ is not a subset of the states of $\mathcal {I}{\downarrow _{k}}$ as required by the once-and-for-all semantics.

For any formula $\varPhi \in \mathtt {rPCTL} ^{\le }$ we define the reward-depth denoted by $K(\varPhi ) \in \mathbb {N}$, on the structure of $\varPhi$. For a probabilistic reward-bounded reachability objective of the form $\varPhi = \mathcal {P}_{\bowtie \lambda }(\lozenge _{\le k} \varGamma )$, $K(\varPhi ) = k$ implies that only paths with an accumulated reward of at most k is of interest. Hence, a k-unfolding of $\mathcal {I}$ is sufficient for the purpose of verifying $\varPhi$.

Definition 12 (Reward-depth)

For every property $\varPhi \in \mathtt {rPCTL} ^{\le }$, the reward-depth, $K(\varPhi ) \in \mathbb {N}$ is defined inductively on the structure of $\varPhi$:

$$\begin{aligned}&K(\text{ true}) = 0\\&K(a) = 0\\&K(\lnot \varPhi ) = K(\varPhi )\\&K(\varPhi _1 \wedge \varPhi _2) = \max \{K(\varPhi _1),K(\varPhi _2)\}\\&K(\mathcal {P}_{\bowtie \lambda }(\textsf {X}_{\le k} \varPhi )) = k + K(\varPhi )\\&K(\mathcal {P}_{\bowtie \lambda }(\varPhi _1 \textsf {U}_{\le k} \varPhi _2)) = k + \max \{K(\varPhi _1), K(\varPhi _2)\} \end{aligned}$$

Example 7

Consider the IMRM $\mathcal {I}_3$ in Fig. 3 and formula $\varPhi = \mathcal {P}_{>0.8}(\lozenge _{\le 3} \varGamma )$. By definition, $K(\varPhi ) = 3 + \max \{K(\text{ true}), K(\varGamma )\} = 3$. Notice that $\mathcal {I}_3 \,\models _d\, \varPhi$ if and only if $k \ge 3$, with the witnessing implementation being the MRM in Fig. 4. Consider now the IMRM $\mathcal {I}_4$ in Fig. 6 and the property $\varPhi ' = \mathcal {P}_{\ge \lambda _1}(\varPhi _1\, U_{\le 2}\, \varPhi _2)$ where $\varPhi _1 = \mathcal {P}_{\ge \lambda _2}(\lozenge _{\le 2}\, \varGamma )$, $\varPhi _2 = \mathcal {P}_{\ge \lambda _3}(\lozenge _{\le 3}\, \Lambda )$ and $\lambda _1, \lambda _2, \lambda _3 \in [0,1]$. For any semantics $x \in \{o,d,a\}$ it is clear that $\mathcal {I}_4{\downarrow _{k}} \,\not \models _x\, \varPhi '$ if $k < 5$, irrespective of the concrete values for $\lambda _1, \lambda _2$ and $\lambda _3$, as the path $s_0,s_1,s_2,s_3,s_4,s_5$ must be preserved. By definition, $K(\varPhi ') = 5$ i.e. if one performs an unfolding of $\mathcal {I}$ with a reward-depth less than $K(\varPhi ')$, one cannot hope to find any implementation satisfying any concrete instantiation of $\varPhi '$.

Fig. 6.

IMRM $\mathcal {I}_4$

As indicated by Example 7, $K(\varPhi )$ is the reward-depth required for the verification of $\varPhi$. Hence, unfolding to a reward-depth greater than $K(\varPhi )$ should not influence the satisfaction of $\varPhi$. The following lemma proves this monotonicity property.

Lemma 6 (Monotonicity)

For any MRM $\mathcal {M}$, formula $\varPhi \in \mathtt {rPCTL} ^{\le }$, $k \ge K(\varPhi )$ and $\varepsilon > 0$,

$$ \mathcal {M}{\downarrow _{k}} \,\models \, \varPhi \implies \mathcal {M}{\downarrow _{k+\varepsilon }} \,\models \, \varPhi . $$

The next lemma states that if an MRM $\mathcal {M}$ satisfies $\varPhi$, then the $K(\varPhi )$-unfolded model $\mathcal {M}{\downarrow _{K(\varPhi )}}$ also satisfies $\varPhi$ i.e. unfolding to a reward-depth of at least $K(\varPhi )$ is sufficient to verify $\varPhi$.

Lemma 7

For any MRM and formula $\varPhi \in \mathtt {rPCTL} ^{\le }$,

$$ \mathcal {M} \,\models \, \varPhi \implies \mathcal {M}{\downarrow _{K(\varPhi )}} \,\models \, \varPhi . $$

We now present the main theorem of this section, stating that rPCTL model-checking for IMRMs with the IMDP semantics can be reduced to model-checking using the once-and-for-all semantics on an IMRM constructed by unfolding to the reward-depth required by the given formula of interest.

Theorem 3

For IMRM $\mathcal {I}$ and formula $\varPhi \in \mathtt {rPCTL} ^{\le }$,

$$ \mathcal {I}\,\models _d\, \varPhi \implies \mathcal {I}{\downarrow _{K(\varPhi )}} \,\models _o\, \varPhi . $$

Proof

We assume $\mathcal {I}\,\models _d\, \varPhi$, hence . By Lemma 7, $\mathcal {M}\,\models \, \varPhi \implies \mathcal {M}{\downarrow _{K(\varPhi )}} \,\models \, \varPhi$ and by Lemma 5 we get . Hence, $\mathcal {I}{\downarrow _{K(\varPhi )}} \,\models _o\, \varPhi$ as required.    $\square$

Complexity. For any IMRM $\mathcal {I}= (S, s_0, \varPi , R, \ell ^{\mathcal {I}})$ let $R_{\min } = \min _{s \in S} R(s)$ be the smallest reward present in $\mathcal {I}$. The unfolded model, $\mathcal {I}{\downarrow _{K(\varPhi )}}$ is then a model of size $\mathcal {O}\left( |S|^{{\lfloor }{\frac{K(\varPhi )}{R_{\min }}}{\rfloor }}\right)$, as each state of $\mathcal {I}{\downarrow _{K(\varPhi )}}$ is a leaf of the underlying $K(\varPhi )$-bounded unfolding of $\mathcal {I}$ which is a tree with branching factor $\mathcal {O}(|S|)$ and height $\mathcal {O}\left( {\lfloor }{\frac{K(\varPhi )}{R_{\min }}}{\rfloor }\right)$.

Remark 4

By Theorem 2, for any $\varPhi \in \mathcal {L}_{\mathtt {reach}}^{\le }$ the approach presented in Sect. 6.2 is valid also for model checking $\varPhi$ w.r.t. the at-every-step semantics.

7 Conclusion and Future Work

We investigated model-checking questions relative to IMRMs specifications interpreted according to three semantics: once-and-for-all, interval Markov decision process, and at-every-step. This work builds on the results of [5] on interval Markov chains by introducing an additional ingredient: rewards. We showed that by introducing rewards the one-at-for-all semantics is no longer expressive enough to answer (existential) reachability queries with respect to the other two semantics. Nevertheless, the IMDP semantics and the at-every-step semantics are still logically equivalent with respect to the reward-bounded reachability fragment of rPCTL.

We then presented how to algorithmically solve the model-checking problem for IMRMs by proposing different reductions to the model-checking problem for parametric Markov reward models (PMRMs). First, we presented a reduction to the model-checking problem of PMRMs for model checking IMRMs interpreted over the once-and-for-all semantics. Then, for the IMDP semantics, we presented a reduction to the model-checking problem for the once-and-for-all semantics, via a finite unfolding of the model. Crucial for our reduction is that the state rewards are positive. Notably, this reduction can also be used also to answer reward-bounded reachability queries for IMRMs interpreted according to the at-every-step semantics.

As future work, we plan to further investigate the model-checking problem with respect to the at-every-step semantic interpretations of IMRMs.