Model Checking Constrained Markov Reward Models with Uncertainties

Abstract

We study the problem of analysing Markov reward models (MRMs) in the presence of imprecise or uncertain rewards. Properties of interests for their analysis are (i) probabilistic bisimilarity, and (ii) specifications expressed as probabilistic reward CTL formulae.

We consider two extensions of the notion of MRM, namely (a) constrained Markov reward models, i.e., MRMs with rewards parametric on a set variables subject to some constraints, and (b) stochastic Markov reward models, i.e., MRMs with rewards modelled as real-valued random variables as opposed to precise rewards. Our approach is based on quantifier elimination for linear real arithmetic. Differently from existing solutions for parametric Markov chains, we avoid the manipulation of rational functions in favour of a symbolic representation of the set or parameter valuations satisfying a given property in the form of a quantifier-free first-order formula in the linear theory of the reals.

Our work finds applications in model repair, where parameters need to be tuned so as to satisfy the desired specification, as well as in robustness analysis in the presence of stochastic perturbations.

Work supported by the Advanced ERC Grant nr. 867096 (LASSO) and the Innovation Fund Denmark Center DiCyPS (nr. 864701).

1 Introduction

The wide-spread diffusion of cyber-physical systems (CPSs) poses the challenge of handling their growing complexity, while meeting requirements on correctness, predictability, performance without compromising time- and cost-to-market. Their analysis requires one to address a number of non-functional properties related to the quantitative aspects that are typical of such systems.

Finite-state Markovian models are popular modelling formalisms for the quantitative analysis of systems with probabilistic behaviours. Among these, Markov reward models (MRMs) were proposed as a natural extension of the usual notion of discrete-time Markov chain with (real-valued) state rewards.

Interesting properties of MRMs may be expressed by means of quantitative extensions of CTL, such as Probabilistic Reward CTL (PRCTL), cf. e.g., [1].

Fig. 1.

Model of a Ph.D. student in CS.

As a running example, consider the MRM in Fig. 1 modelling the stress level of a Ph.D. student in computer science. It has seven states, namely $s_1, \dots , s_7$, annotated with the propositions thk (thinking), ths (thesis), wr (writing paper), tc (tool coding), and pe (paper evaluation). The level of stress of the student is modelled by associating with each state a reward that represents the stress that the student accumulates in the state at each time unit. After spending some time thinking, the student starts developing a tool with probability $p_c = 0.2$, or writing a paper with probability $p_w = 0.5$ ($40\%$ of the times for a journal and $60\%$ for a conference), otherwise the student submits the thesis with probability 0.1. Once the tool is mature enough, the student starts writing a paper about it with probability $p_w$ (70% of which for a journal, otherwise for a conference). When a paper has been completed it is submitted for evaluation with probability $p_s = 0.3$. The paper may be rejected or accepted (moving resp. to $s_7$ or $s_5$) according to some acceptance rate. At any moment before the thesis is completed, the student may move back to $s_1$ with probability $p_t = 0.2$ to think on how to proceed with his/her Ph.D.

We can use PRCTL formulae for specifying properties such as “the average level of stress accumulated until the thesis is submitted doesn’t exceed 10”, “the student completes the thesis without passing through a state with stress level higher than 2 with probability greater than or equal to 0.9”, or “the probability of eventually start coding and, subsequently, submitting the thesis with expected accumulated stress within [x, y] is less than or equal to z”.

In the above MRM we fixed specific reward values. This is an unrealistic simplification since the level of stress at each state may vary depending on different factors, possibly external to the student. The same argument applies to CPSs, that typically rely on sensor measurements which are inherently imprecise, but also to other systems, e.g., resource-management protocols that depends on stochastic assumptions on the future workload.

Typically, there are two ways for dealing with uncertain measurements: (i) determine the precision of the instrument and associate an error $\epsilon$ with each measurement, or (ii) perform estimation statistics (e.g., by recursive Bayesian estimation [16]) and use random variables to model each measurement.

In this paper we address the problem of analysing MRMs in presence of imprecise rewards. We present two extensions of the notion of MRM: (i) constrained Markov reward models (CMRMs), i.e., MRMs with rewards and transition probabilities parametric on a set variables subject to some constraints expressed as a first-order formula in the linear theory of the reals; (ii) stochastic Markov reward models (SMRMs), i.e., MRMs with rewards modelled as real-valued random variables as opposed to exact rewards.

Intuitively, a CMRM models a family of MRMs arising by plugging in concrete values for the parameters provided that they satisfy its constraints. Analogously, an SMRM models a probability distribution over a family of MRMs.

We are interested in the analysis of these models with respect to (i) probabilistic bisimilarity, and (ii) specifications expressed as PRCTL formulae.

On the one hand, the analysis of CMRMs is done by inferring constraints over its parameters characterising the valuations satisfying the property then, verify the robustness of the model within the given precision. On the other hand, analysing an SMRM consists in measuring the likelihood that an MRM obtained by plugging in real-valued outcomes of its random variables satisfies a given property.

Our Contribution: In relation with the analysis of CMRMs our contribution is twofold. First, we show that the computation of the set of parameter valuations ensuring that some states are probabilistic bisimilar with each other can be done using quantifier elimination in the linear fragment of the theory of the reals. Secondly, we demonstrate that for CMRMs having parameters only on state rewards, also the PRCTL model checking problem can be solved within the linear fragment of the theory of the reals. This allows one to employ SMT solvers and quantifier elimination procedures specialised on linear constraints [14], avoiding to use more inefficient and less scalable solvers for bilinear inequalities [17] as suggested e.g., in the case of interval Markov chains [15].

As for the analysis of SMRMs, we describe how one can apply the results for CMRMs described above for estimating the probability of satisfying a given property by employing Mote Carlo simulation techniques.

Related Work: The analysis of CMRMs falls into the research area of parameter synthesis for parametric Markov chains (pMCs) [4, 6,7,8,9,10, 12] and Interval Markov chains (IMC) [2, 3, 15]. Most of these works [4, 5, 7, 8, 10] consider pMCs without state rewards and focus mainly on computing closed form solutions for reachability probabilities in pMCs as rational functions. The same approach was recently extended to the computation of closed form solutions for expected rewards and long-run average rewards [6, 9].

In the context of model checking pMCs and IMCs, quantifier elimination for the first-order theory of the reals has been mainly applied as a theoretical tool for proving complexity upper-bounds of the model checking problem for IMCs [2, 3, 15] and pMCs [9]. Notably, the model checker PROPhESY [5] relies on SMT solving via the existential theory of the reals to determine approximate covering of the parameter space.

2 Preliminaries and Notation

We denote by $\mathbb {R}$, $\mathbb {Q}$, and $\mathbb {N}$ respectively the sets of real, rational, and natural numbers. We denote by $\varSigma ^n$, $\varSigma ^*$ and, $\varSigma ^\omega$ respectively the set of words of length $n \in \mathbb {N}$, finite length, and infinite length, built over the finite alphabet $\varSigma$.

The dot product of two vectors $\mathbf {a} = (a_1, \dots , a_n)$ and $\mathbf {b} = (b_1,\dots , b_n)$ in $\mathbb {R}^n$ is defined as $\mathbf {a} \cdot \mathbf {b} = \sum _{i = 1}^n a_i b_i$. For $c \in \mathbb {R}$, we use $\mathbf {c} \in \mathbb {R}^n$ to denote the constant vector $(c,\dots , c)$. For a function $f :I \rightarrow \mathbb {R}$ with finite domain with cardinality $|I| = n$ we may use f to denote also the I-indexed vector $(f(i))_{i \in I} = (f(i_1), \dots , f(i_n))$.

Measure Theory. Let $\varOmega$ be a set. A family $\varSigma \subseteq 2^{\varOmega }$ is called a $\sigma$-algebra if it contains the empty set and is closed under complement and countable unions, in this case $(\varOmega ,\varSigma )$ is called a measurable space and elements of $\varSigma$ measurable sets. When $\varSigma = 2^{\varOmega }$, the measure space $(\varOmega ,\varSigma )$ is discrete.

A measure on $(\varOmega ,\varSigma )$ is a $\sigma$-additive function $\mu : \varSigma \rightarrow \mathbb {R}$, i.e. a map satisfying $\mu (\bigcup _{i \in I}E_i) = \sum _{i \in I} \mu (E_i)$ for any countable family of pairwise disjoint measurable sets $(E_i)_{i \in I}$, in this case $(\varOmega ,\varSigma ,\mu )$ is called a measure space. If additionally $\mu$ satisfies $\mu (\varOmega ) = 1$, it is called a probability measure and $(\varOmega ,\varSigma ,\mu )$ a probability space. We denote by $\mathcal {D}(\varOmega )$ the set of discrete probability distributions on $\varOmega$. For $x \in \varOmega$, the Dirac distribution concentrated at x is the distribution $1_x \in \mathcal {D}(\varOmega )$ defined, for arbitrary $y \in \varOmega$, as $1_x(y) = 1$ if $x = y$, 0 otherwise.

For measurable spaces $(\varOmega ,\varSigma )$ and $(\varGamma ,\varTheta )$, a map $f: \varOmega \rightarrow \varGamma$ is measurable if for all $E \in \varTheta$, $f^{-1}(E) = \{ x \mid f(x) \in E \} \subseteq \varSigma$. Given a measurable map $f: \varOmega \rightarrow \varGamma$ and a measure $\mu$ on $(\varOmega ,\varSigma )$ we define the measure $\mu [f]$ on $(\varGamma ,\varTheta )$, called the push forward of $\mu$ under f, as $\mu [f](E) = \mu (f^{-1}(E))$ for $E \in \varTheta$.

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

3 Markov Reward Models

In this section we recall the definitions of Markov reward models (MRMs), probabilistic bisimulation, and probabilistic reward CTL (PRCTL).

In what follows we fix a finite set of atomic propositions $\mathcal {AP}$.

Definition 1

A Markov chain is a tuple $\mathcal {M}= (S, \tau , \ell )$ consisting of a finite nonempty set of states S, a transition probability function $\tau :S \rightarrow \mathcal {D}(S)$, and a labelling function $\ell : S \rightarrow 2^{\mathcal {AP}}$ mapping states to atomic propositions.

Intuitively, if $\mathcal {M}$ is in state s it moves to state $s'$ with probability $\tau (s)(s')$. In this sense, $\mathcal {M}$ can be thought as a state-machine that generates paths in $S^\omega$. A path is an infinite sequence of states $\pi = s_1s_2s_3 \cdots \in S^{\omega }$; for $i \ge 1$ we denote by $\pi [i]$ the i-th state of $\pi$, i.e., $\pi [i] = s_i$, and $\pi |^i$ the prefix of length i of $\pi$, i.e., $\pi |^i = s_1 \cdots s_{i}$ and $\pi |^0 = \varepsilon$.

We denote by $G_\mathcal {M}= (S,\rightarrow )$ the underlying graph of $\mathcal {M}$, where $s,s' \in S$ are connected by a directed edge, written $s \rightarrow s'$, if and only if $\tau (s)(s') > 0$. We indicate by $\rightarrow ^*$, the transitive and reflexive closure of $\rightarrow$.

In order to associate probabilities to events, we adopt the classical cylinder set construction (cf. [1, Ch10]). 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 , \varSigma _\mathcal {M}, Pr^{\mathcal {M}}_\iota )$, where $\varSigma _\mathcal {M}= \sigma (\{ cyl (w) \mid w \in S^*\})$ is the smallest $\sigma$-algebra that contains all the cylinder sets, and $Pr^{\mathcal {M}}_\iota$ is the unique probability measure such that, for all $w = s_1 \cdots s_n \in S^*$, $Pr^{\mathcal {M}}_\iota ( cyl (w)) = \iota (s_1) \cdot \prod _{0< i < n} \tau (s_i)(s_{i+1})$.

When $\iota = 1_s$ we write $Pr^{\mathcal {M}}_s$, or just $Pr_s$ when $\mathcal {M}$ is clear from the context.

Definition 2

A Markov reward model is a tuple $\mathcal {R} = (S,\tau , \ell ,\rho )$ where $(S,\tau , \ell )$ is a MC, and $\rho : S \rightarrow \mathbb {R}$ is the reward function assigning a reward to each state.

A Markov reward model generates paths in $S^\omega$ according to its underlying Markov chain; in addition, whenever a transition is performed, say from s to $s'$, the system is rewarded by $\rho (s)$. It is worth noting that the reward is given after leaving the current state.

In the following, it may be convenient to represent the reward function $\rho$ and the probability transition distributions $\tau (s)$ (for $s \in S$) as S-indexed vectors.

Example 1

Consider the MRM depicted in Fig. 1. Its reward function $\rho$ and the distribution $\tau (s_1)$ are respectively represented in vector notation as

$$\begin{aligned} \rho = (0,0,1.2, 1.5, -3, 2, 3), \quad \text {and} \quad \tau (s_1) = (p_t, 0.1, 0.6 p_w, 0.4 p_w, 0, p_c, 0). \end{aligned}$$

The next definition extends the classic notion of probabilistic bisimulation for Markov chains by Larsen and Skou [13] to the case of MRMs.

Definition 3

(Bisimulation). Let $\mathcal {R} = (S,\tau , \ell ,\rho )$ be an MRM. An equivalence relation $R \subseteq S \times S$ is a probabilistic bisimulation if whenever $(s,s') \in R$ then, $\ell (s) = \ell (s')$, $\rho (s) = \rho (s')$, and for all R-equivalence class $C \in S/_{R}$, $\tau (s)(C) = \tau (s')(C)$.

Two states $s, s' \in S$ are probabilistic bisimilar, written $s \sim _{\mathcal {R}} s'$, if they are related by some probabilistic bisimulation.

Example 2

Consider the MRM depicted in Fig. 1. As it is presented, none of its states are bisimilar with each other because each pair of states differs on the rewards or the labels. If we consider instead an MRM with underlying chain as in Fig. 1 and rewards $\rho = (0,0,1, 1, 3, 2, 3)$, now we have that $s_5 \sim s_7$ and, consequently, $s_3 \sim s_4$ because $\tau (s_3)(\{s_5,s_7\}) = p_s = \tau (s_4)(\{s_5, s_7\})$.    $\square$

Before presenting probabilistic reward CTL, we need to introduce the concept of expected cumulative reward for reaching a set of states $B \subseteq S$.

Let $\hat{\rho }_{B} :S^\omega \rightarrow \mathbb {R}$ be the random variable representing the reward accumulated along a prefix of the path belonging to $(S \setminus B)^*B$. This is formalised as $\hat{\rho }_{B}(\pi ) = \sum _{i = 1}^{n-1} \rho (\pi [i])$ if $\pi |^n \in (S \setminus B)^*B$ for some $n \in \mathbb {N}$, otherwise 0.

We denote by $E[\hat{\rho }_{B} | s]$ the expected value of $\hat{\rho }_{B}$ with respect to the probability distribution $Pr _s$. Following [1, Ch10], $E[\hat{\rho }_{B} | s]$ can be computed as the (unique) solution $r_s$ of the following system of linear equations

$$\begin{aligned} r_s = {\left\{ \begin{array}{ll} 0 &{} \mathrm {if}\; s \in B \text { or } s \not \rightarrow ^* B \\ \rho (s) + \big ( \sum _{t \in S} \tau (s)(t) \cdot r_t \big ) &{} \mathrm {otherwise.} \end{array}\right. } \end{aligned}$$

(1)

We are now ready to present Probabilistic Reward CTL. PRCTL allows for state formulae describing properties about states in a MRM, and path formulae describing properties about paths in a MRM. State formulae $\varPhi ,\varPsi$ and path formulae $\varphi$ are constructed over the following abstract syntax:

where $a \in \mathcal {AP}$, $r \in \mathbb {Q}$, $n \in \mathbb {N}$, ${\bowtie } \in \{ =, <, >\}$, and $J \subseteq [0,1]$ and $R \subseteq \mathbb {R}$ are intervals with rational bounds.

Given a MRM $\mathcal {R} = (S, \tau , \ell , \rho )$, a state $s \in S$, and a path $\pi \in S^\omega$, we denote by $\mathcal {R}, s\,\models \,\varPhi$ (resp. $\mathcal {R}, \pi \,\models \, \varphi$) the fact that the state s satisfies the state formula $\varPhi$ (resp. the path $\pi$ satisfies the path formula $\varphi$). $\mathop {Sat}(\varPhi )$ denotes the set of all states satisfying the property $\varPhi$, i.e. $\mathop {Sat}(\varPhi ) = \{ s \in S \mid \mathcal {R},s\,\models \,\varPhi \}$. Formally, the satisfiability relation $\models$ is inductively defined as:

As usual, we can derive the logical operators $f\!\!f$, $\vee$, and $\rightarrow$ as follows: $f\!\!f\overset{\mathtt{def}}{=}\lnot t\!t$, $\varPhi \vee \varPsi \overset{\mathtt{def}}{=}\lnot (\lnot \varPhi \wedge \lnot \varPsi )$, and $\varPhi \rightarrow \varPsi \overset{\mathtt{def}}{=}\lnot \varPhi \vee \varPsi$. Similarly, we can derive the temporal operators $\lozenge$ and $\square$ as: $\lozenge \varPhi \overset{\mathtt{def}}{=}t\!t\mathcal {U}\varPhi$ and $\square \varPhi \overset{\mathtt{def}}{=}\lnot \lozenge ( \lnot \varPhi )$.

Example 3

Consider the MRM $\mathcal {R}$ depicted in Fig. 1. We can verify that “the average level of stress accumulated by the student until the thesis is submitted doesn’t exceed 23” by proving that $\mathcal {R}, s_1\,\models \,\mathbb {E}_{\le 23}( ths )$ holds true. Analogously, we can check that the property “the student completes the thesis without passing through a state with stress level higher than 2 with probability greater than or equal to 0.5” does not hold true by proving $\mathcal {R}, s_1\,\models \,\lnot \mathbb {P}_{\ge 0.5}((\rho \le 2) \mathbin {\mathcal {U}} ths )$.    $\square$

4 Constrained Markov Reward Models

Constrained Markov reward models (CMRMs) model families of MRMs where both transition probabilities and state rewards are parametric on a set of real-valued variables subject to constraints expressed as a first-order formula in the linear theory of the reals.

Let $\mathbf {x} = (x_1,\ldots ,x_k)$ be a vector of real-valued parameters. We denote by $\mathcal {E}$ the set of affine maps $f: \mathbb {R}^k \rightarrow \mathbb {R}$ of the form $f(\mathbf {x}) = \mathbf {a} \cdot \mathbf {x} + b$ with $\mathbf {a} = (a_1,\ldots ,a_k) \in \mathbb {Q}^k$ and $b \in \mathbb {Q}$, i.e. $f(x_1,\ldots ,x_k) = \big (\sum _{i=1}^k a_i x_i \big ) + b$.

Definition 4

A constrained Markov reward model is a tuple $\mathcal {F} = (S,\tau , \ell , \rho , F)$ where S and $\ell$ are defined as for MCs, $\tau :S \rightarrow (S \rightarrow \mathcal {E})$ is a parametric transition function, $\rho : S \rightarrow \mathcal {E}$ is a parametric reward function, and $F(\mathbf {x})$ is a linear first-order formula s.t., for all $s \in S$, $F(\mathbf {x})$ implies $\tau (s) \ge \mathbf {0} \wedge \mathbf {1} \cdot \tau (s) = 1$.

Intuitively, a CMRM $\mathcal {F} = (S,\tau , \ell , \rho , F)$ defines a family of MRMs arising by plugging in concrete values for the parameters. A parameter valuation $\mathbf {v} \in \mathbb {R}^k$ is admissible (or feasible) if $F(\mathbf {v})$ holds true. By abuse of notation, we may write F to indicate the set of admissible valuations. Given $\mathbf {v} \in F$ we denote by $\mathcal {F}(\mathbf {v})$ the MRM associated with $\mathbf {v}$. In this respect, it will be convenient to think of $\mathcal {F}$ as a function $\mathcal {F}: F \rightarrow \mathrm {MRM}$. The semantics of $\mathcal {F}$, written $[\mathcal {F}]$, is defined as the image of $\mathcal {F}$, i.e. $[\mathcal {F}] = \{\mathcal {F}(\mathbf {v}) \mid \mathbf {v} \in F \}$.

Example 4

As already mentioned in the introduction, the stress level of a Ph.D. student may be influenced by several factors. For instance, we can define the following CMRM $\mathcal {F} = (S, \tau , \ell , \bar{\rho }, F)$ having as underlying Markov chain that of Fig. 1, parametric vector of rewards $\rho = (0, 0, h + c, h + j, r, 0, a)$, and constraints $F = (-5 \le h \le 0) \wedge (1 \le c \le j \le 5) \wedge (-3 \le a + r \le 3) \wedge a \le r$. Here, the parameter h models the help of the supervisor, whereas c and j represent the stress that accumulates while writing a conference paper c, or a journal paper j. The stress caused by having a paper accepted or rejected in modelled by the parameters a and r respectively.

It is easy to note that the MRM in Fig. 1 is an instance of $\mathcal {F}$.    $\square$

Remark 1

Our notion of CMRM trivially extends that of IMC w.r.t. the so-called uncertain Markov chain interpretation [15]. The condition that transitions probabilities lie within some intervals is trivially expressed as a conjunction of liner inequalities. We shall also recall, that our definition is similar to that of augmented pMCs given by Hutschenreiter et al. [9]. Nevertheless, we do not require all admissible valuations to induce the same underlying graph; instead, we require linear constraints as opposed to polynomial constraints.    $\square$

Given a CMRM $\mathcal {F}$ we are interested in finding suitable symbolic representations of the set of parameter valuations that ensure the corresponding MRMs to enjoy some property. Properties of interests for this paper are bisimulation and PRCTL formulae. Specifically, given states $s,s' \in S$, and a PRCTL state formula $\varPhi$, we are interested in the set of parameter valuations for which s becomes bisimilar to $s'$ or such that $\varPhi$ holds at s. These are formalised as follows.

$$\begin{aligned} \llbracket s \sim _{\mathcal {F}} s' \rrbracket&\overset{\mathtt{def}}{=}\left\{ \mathbf {v} \in F \mid s \sim _ {\mathcal {F}(\mathbf {v})} s' \right\} ,&\llbracket \mathcal {F},s\,\models \,\varPhi \rrbracket&\overset{\mathtt{def}}{=}\left\{ \mathbf {v} \in F \mid \mathcal {F}(\mathbf {v}),s\,\models \,\varPhi \right\} \,. \end{aligned}$$

Example 5

Consider the CMRM $\mathcal {F}$ defined in Example 4 and the PCTL formula $\varPhi = \mathbb {E}_{[0,10]}( ths )$. The set of feasible parameter valuations satisfying $\varPhi$, i.e., $\llbracket \mathcal {F},s\,\models \,\varPhi \rrbracket$, can be symbolically represented by the following formula

$$\begin{aligned} \phi = 0\le 57 a+575 c+750 h+175 j+168 r\le \frac{1750}{3}\wedge F \,. \end{aligned}$$

(2)

The above formula can be used for instance to determine how much effort the supervisor needs to provide to ensure that the formula $\varPhi$ is satisfied. In this case, this can be done by maximising h under the constraints $\phi$.    $\square$

5 Analysing Bisimilarity on Constrained MRMs

In this section we address the problem of finding symbolic representations of the set of parameter valuations ensuring that two given states of a CMRM are probabilistic bisimilar.

Before diving in this problem, it will be convenient to present an alternative characterisation for probabilistic bisimilarity on MRMs. The characterisation is a variant of that of Jonsson and Larsen [11] based on the notion of coupling.

Given $\mu , \nu \in \mathcal {D}(X)$, we denote by $\varGamma (\mu , \nu )$ the set of couplings for $(\mu , \nu )$, i.e., probability distributions $\gamma \in \mathcal {D}(X \times X)$ such that, for all $x,y \in X$

$$\begin{aligned} \textstyle \sum _{x' \in X} \gamma (x',y) = \nu (y) \quad \text {and} \quad \textstyle \sum _{y' \in X} \gamma (x,y') = \mu (x) \, . \end{aligned}$$

(3)

The probability measures $\mu$ and $\nu$ are respectively called left and right marginals of $\gamma$. A coupling can be seen as a redistribution of the “probability mass” from the right marginal to the left and vice versa.

Lemma 1

$s \sim s'$, if and only if there exists a relation $R \subseteq S \times S$, such that $s \mathrel {R} s'$ and, whenever $m \mathrel {R} n$ the following conditions hold

• (i) $\ell (m) = \ell (n)$, $\rho (m) = \rho (n)$, and

• (ii) there exists $\gamma \in \varGamma (\tau (m), \tau (n))$ such that $\{(u,v) \in S\times S \mid \gamma (u,v) > 0 \} \subseteq R$.

The above lemma allows us to encode $\llbracket s \sim _{\mathcal {F}} s' \rrbracket$ as the following first-order formula in the linear theory of the reals.

(4)

where the sub-formulae $\beta$, $\gamma$, and $\sigma$ are defined as follows:

$$\begin{aligned}&\beta (m,n) \overset{\mathtt{def}}{=}\bigwedge _{m,n \in S} (b_{mn} = 0 \vee b_{mn} = 1) \end{aligned}$$

(5)

$$\begin{aligned}&\gamma (m,n) \overset{\mathtt{def}}{=}(b_{mn} = 1) \rightarrow \exists \mathbf {c} \ge \mathbf {0}. \, \left( \begin{aligned}&\textstyle \bigwedge _{u \in S} \sum _{v \in S} c_{u v} = \tau (m)(u) \wedge {} \\&\textstyle \bigwedge _{v \in S} \sum _{u \in S} c_{u v} = \tau (n)(v) \wedge {} \\&\textstyle \bigwedge _{u,v \in S} c_{uv} \le b_{uv} \end{aligned} \right) \end{aligned}$$

(6)

$$\begin{aligned}&\sigma (m,n) \overset{\mathtt{def}}{=}(b_{mn} = 1) \rightarrow (\ell (m) = \ell (n) \wedge \rho (m) = \rho (n) ) \,. \end{aligned}$$

(7)

In the formula , $\mathbf {b} = (b_{mn})_{m,n \in S}$ represents a selection of a relation $R \in S \times S$ by means of binary variables (cf.  (5)) such that $b_{m,n} = 1$ iff $(m,n) \in R$. According to Lemma 1, the selection needs to include the pair $(s,s')$ and satisfy the conditions (i) and (ii). This is modelled by imposing $b_{ss'} = 1$, $\sigma (m,n)$ and $\gamma (m,n)$ for all $m,n \in S$. In particular, in (6), the variables $\mathbf {c} = (c_{u v})_{u,v \in S}$ model coupling for $(\tau (m), \tau (n))$ the condition (ii) is enforced by requiring $c_{u,v} \le b_{u,v}$ for all $u,v \in S$.

By Lemma 1, the elimination of the existential quantifiers in yields a Boolean formula with linear predicates on $\mathbf {x}$ representing the set of valuations $\llbracket s \sim _{\mathcal {F}} s' \rrbracket$. Notably, the formula is a first-order formula in the existential theory of the reals which involves only linear predicates. Therefore, quantifier elimination can be performed by using tools specialised for the linear theory of real-arithmetic, such as mjollnir [14].

6 Model Checking Constrained MRMs

In this section we consider the model checking problem of CMRMs against PRCTL formulae for the class of constrained MRMs having parameters only on state rewards. For this class, we show that the set of parameter valuations satisfying given PRCTL formula can, again, be encoded as a first-order formula in the linear theory of real-arithmetic.

In this section assume that in the CMRM $\mathcal {P} = (S,\tau , \ell , \rho , F)$, parameters occur only in the state rewards, that is, $\tau (s)(u) \in [0,1]$ for all $s,u \in S$.

For a state $s \in S$, and a PRCTL state formula $\varPhi$, we characterise $\llbracket \mathcal {P},s\,\models \,\varPhi \rrbracket$ by means of the set of valuations satisfying . The formula encodes the satisfiability of $\mathcal {P}$ in s up-to the constraints F, and it is defined by induction on the structure of $\varPhi$.

For the Boolean fragment of PRCTL, the reduction is as one may expect.

For all other formulae, it is convenient to use as short for .

where $\mathbf {p} = (p_s)_{s \in S}$, $\mathbf {r} = (r_s)_{s \in S}$, $\mathbf {q} = (q_w)_{w \in S^n}$, , and

In , the variable $p_u$ represents the probability of moving from s to u, where u satisfies the property $\varPhi$, therefore $\mathbf {1} \cdot \mathbf {p} = \sum _{u \in S}$ is the probability of moving in one step from s to a state satisfying $\varPhi$. Analogously, in , the variable $p_u$ models the probability of u satisfying the property $\varPhi \mathcal {U}\varPsi$: if u satisfies the property $\varPhi$ then $p_u$ is 1; if u satisfies neither $\varPhi$ nor $\varPsi$ or cannot reach a state satisfying $\varPsi$, then $p_u$ is 0; otherwise, $p_u$ amounts to the probability of moving in one step to some other state $u'$ and, from there, satisfying $\varPhi \mathcal {U}\varPsi$.

In , $q_w$ is the probability of executing the trace w in exactly n steps starting from s where $\beta (w)$ models that fact that w satisfies $\varPhi \mathcal {U}^n_R \varPsi$. Therefore, $\mathbf {1} \cdot \mathbf {q}$ amounts to the probability of executing from s a path that satisfies $\varPhi \mathcal {U}^n_R \varPsi$.

Finally, in , one can readily see that $\mathbf {r}$ models the unique solution of the system of linear equations (1), where formula $\alpha _u$ capture the fact that u either satisfies the property $\varPhi$ or cannot reach any state that does.

The following result states the correctness of the above characterisation.

Theorem 1

iff $\mathbf {v} \in \llbracket \mathcal {P},s\,\models \,\varPhi \rrbracket$.

Example 6

Consider the CMRM $\mathcal {F}$ and the formula $\varPhi$ from Example 5. The encoding of the satisfiability of $s_1$ with respect to $\varPhi$, namely , boils down to the following first order linear formula.

By using the tool mjollnir [14] we are able to eliminate the existential quantifiers on $\mathbf {x} = (x_1, \dots , x_7)$ obtaining the formula $\phi$ of Eq. (2).    $\square$

7 Markov Models with Stochastic Rewards

It’s common practice to model experimental measurements by means of real-valued random variables distributed according to well studied families of distributions (e.g., normal or student’s T).

In this section we introduce the notion of stochastic Markov reward models (SMRMs) where state rewards are real-valued random variables. Then, we present a PRCTL model checking framework for SMRMs.

From here on we fix the probability space $(\varOmega ,\varSigma , P)$ representing the environment where the experiments are performed, and we use $\mathbb {Y}$ to denote the set of real-valued random variables of the form $Y :\varOmega \rightarrow \mathbb {R}$.

Definition 5

A stochastic Markov reward model is a tuple $\mathcal {J} = (S,\tau ,\ell ,\rho )$ where $(S,\tau , \ell )$ is a Markov chain, and $\rho : S \rightarrow \mathbb {Y}$ is a reward function assigning a real-valued random variable to each state.

An SMRM $\mathcal {J} = (S,\tau ,\ell ,\rho )$ can be intuitively interpreted as a measurable function $\mathcal {J} :\varOmega \rightarrow \text {MRM}_{\mathcal {J}}$, where $\mathcal {J}(\omega )$ is the MRM having $(S,\tau ,\ell )$ as underlying Markov chain and $(\rho (s)(\omega ))_{s \in S}$ as vector of rewards. Such interpretation justifies the intuition of $\mathcal {J}$ being an experiment whose outcomes is a MRM.

The above intuition is formalised as follows. We denote by $\text {MRM}_{\mathcal {J}}$ the set of all MRMs having the same underlying Markov chain as $\mathcal {J}$. We construct the $\sigma$-algebra $\varSigma _{\mathcal {J}}$ as the family of sets $A \subseteq \text {MRM}_{\mathcal {J}}$ whose corresponding set of rewards vectors is Borel measurable in $\mathbb {R}^m$ ($m = |S|$). Formally,

$$\begin{aligned} A \in \varSigma _{\mathcal {J}} \quad \text {iff} \quad A \subseteq \text {MRM}_{\mathcal {J}} \text { and } \{\rho (\mathcal {R}) \mid \mathcal {R} \in A\} \in \mathcal {B}(\mathbb {R}^m) \,. \end{aligned}$$

Accordingly, the semantics of $\mathcal {J}$ is the probability space $(\text {MRM}_{\mathcal {J}}, \varSigma _{\mathcal {J}}, P[\mathcal {J}])$.

Given a SMRM $\mathcal {J}$, a state $s \in S$, and a PRCTL formula $\varPhi$, it comes natural to ask how likely is that a concrete instance of $\mathcal {J}$ satisfies $\varPhi$ at s, denoted by $P[\mathcal {J},s\,\models \,\varPhi ]$. This model checking problem is formalised as follows

$$\begin{aligned} P[\mathcal {J},s\,\models \,\varPhi ] \overset{\mathtt{def}}{=}P[\mathcal {J}](\{ \mathcal {R} \in \text {MRM}_{\mathcal {J}} \mid \mathcal {R},s\,\models \,\varPhi \}) \,. \end{aligned}$$

(8)

We study the above model checking problem for a subclass of SMRMs having random variables $(Y :\varOmega \rightarrow \mathbb {R}) \in \mathcal {E}_{\mathbf {X}}$ of the form $Y(\omega ) = \mathbf {a} \cdot \mathbf {X}(\omega ) + b$, with $\mathbf {a} \in \mathbb {Q}^k$, $b \in \mathbb {Q}$ and, where $\mathbf {X} = (X_1, \dots , X_k)$ is a vector of pairwise independent real-valued random variables¹. Observe that, elements in $\mathcal {E}_{\mathbf {X}}$ may not be independent from each other.

Hereafter we consider the SMRM $\mathcal {J} = (S,\tau ,\ell ,\rho )$ with $\rho :S \rightarrow \mathcal {E}_{\mathbf {X}}$, and we use $\mathcal {P}$ to refer to the CMRM obtained by replacing the random variables $X_i$ in $\mathcal {J}$ with the parameters $x_i$ ($i = 1, \dots , k$).

For Eq. (8) to be well-defined the set $\{ \mathcal {R} \in \text {MRM}_{\mathcal {J}} \mid \mathcal {R},s\,\models \,\varPhi \}$ needs to be a measurable event in $\varSigma _{\mathcal {J}}$. The following result ensures that.

Lemma 2

$\{ \mathcal {R} \in \text {MRM}_{\mathcal {J}} \mid \mathcal {R},s\,\models \varPhi \} \in \varSigma _{\mathcal {J}}$.

Proof

By definition of $\mathcal {P}$ we have that

$$\begin{aligned} \{ \mathcal {R} \in \text {MRM}_{\mathcal {J}} \mid \mathcal {R},s\,\models \,\varPhi \} = \{ \mathcal {P}(\mathbf {v}) \mid \mathbf {v} \in \llbracket \mathcal {P},s\,\models \,\varPhi \rrbracket \}) \end{aligned}$$

Therefore, by def. of $\varSigma _{\mathcal {J}}$ and measurability of affine transformations we have that the claim holds iff $\llbracket \mathcal {P},s\,\models \,\varPhi \rrbracket \in \mathcal {B}(\mathbb {R}^k)$. By Theorem 1, $\llbracket \mathcal {P},s\,\models \,\varPhi \rrbracket$ can be described by means of a Boolean formula with linear predicates. Since $\sigma$-algebras are closes under complement (i.e., negation), countable unions (i.e., disjunctions) and countable intersections (i.e., conjunctions) and, affine transformations are measurable, we conclude that $\{ \mathcal {R} \in \text {MRM}_{\mathcal {J}} \mid \mathcal {R},s\,\models \,\varPhi \} \in \varSigma _{\mathcal {J}}$.

The following theorem characterises the model checking problem for the SMRM $\mathcal {J}$ in terms of the model checking problem for the CMRM $\mathcal {P}$.

Theorem 2

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

Proof

The claim holds true according to the following equalities.

   $\square$

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

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

(9)

For example, we can estimate p with an error $\varepsilon = 0.01$ with a confidence of $95 \%$ (i.e., $\delta = 0.95$) by drawing $n = 18445$ samples.

Example 7

Let $\mathbf {X} = (H, C, J, A, R)$ be a vector of random variables respectively distributed as $H \sim \text {unif}(-5,0)$, $C \sim \text {unif}(1,2)$, $J \sim \mathcal {N}(2,0.1)$, $A \sim \mathcal {N}(-3,0.5)$, and $R \sim \mathcal {N}(-3,0.5)$. We define the SMRM $\mathcal {J} = (S,\tau ,\ell ,\rho )$ having as underlying Markov chain that of Fig. 1, and the following random vector of rewards

$$\rho = (0, 0, H + C, H + J, R, 0, A) \,,$$

which shall be understood as a stochastic version of the one presented in Example 4. By taking the formula $\varPhi = \mathbb {E}_{[0,10]}( ths )$ from Example 5, we can estimate $P[\mathcal {J},s_1\,\models \,\varPhi ] \cong 0.156061$ with an error $\varepsilon = 0.005$ and confidence of $99.99\%$ (i.e., $\delta = 0.0001$) by generating $n = 198070$ samples.    $\square$

8 Conclusion

We described a framework for the analysis of Markov reward models in presence of uncertain rewards. To this end we propose two extensions of the notion of MRM: (a) constrained Markov reward models, having state rewards parametric on a set variables subject to some constraints, and (b) stochastic Markov reward models, having rewards modelled as random variables.

We demonstrated that the analysis CMRMs with respect to probabilistic bisimilarity and PRCTL formulae, can be reduced to perform quantifier elimination on fist-order formulae in the linear fragment of the theory of the reals. Our reduction does not lead to an improvement on the theoretical complexity of the model checking problem for (augmented) parametric Markov chains (cf.  [9, Theorem 4]). However, we believe that our reduction is important from the perspective of implementation in practice, because it allows one to employ SMT solvers or quantifier elimination procedures specialised on linear constraints such as mjollnir [14]. It is worth noting that our reduction can be also applied with PRCTL formulas with parametric bounds, extending even further the applicability of our approach.

Finally, we provided a characterisation of the model checking problem for SMRMs in terms of the model checking problem for CMRMs. As we have shown, this result allows one to estimate the probability that a given SMRM satisfies a given specification by employing Monte Carlo simulation techniques.

All the calculations presented in the examples have been done by using a prototype implementation of the above described algorithms² coded in Mathematica [18]. For the quantifier elimination we employed mjollnir instead of the built-in solution offered by Mathematica.

Our work finds applications in model repair, where parameters need to be tuned so as to satisfy a desired specification, as well as in robustness analysis in presence of stochastic perturbations.