Markov Automata with Multiple Objectives

TL;DR

This paper develops algorithms for analyzing multiple, possibly dependent objectives in Markov automata, enabling the approximation of Pareto curves and trade-offs in complex stochastic systems.

Contribution

It introduces methods to analyze several objectives simultaneously in Markov automata, including trade-offs and combined criteria, extending beyond single-objective verification.

Findings

Algorithms successfully approximate Pareto curves.

Approach handles multiple, dependent objectives.

Experimental results demonstrate scalability.

Abstract

Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is used in reliability engineering, performance evaluation and stochastic scheduling. Their verification so far focused on single objectives such as (timed) reachability, and expected costs. In practice, often the objectives are mutually dependent and the aim is to reveal trade-offs. We present algorithms to analyze several objectives simultaneously and approximate Pareto curves. This includes, e.g., several (timed) reachability objectives, or various expected cost objectives. We also consider combinations thereof, such as on-time-within-budget objectives - which policies guarantee reaching a goal state within a deadline with at least probability $p$ while keeping the allowed average costs below a threshold? We adopt existing approaches for classical Markov decision processes. The main challenge is to treat policies exploiting state residence times, even for untimed objectives. Experimental results show the feasibility and scalability of our approach.

Tables

Table 1. Table 1: Experimental results for multi-objective MAs.

benchmark			$(◆,\mathrm{ER},{◆}^I)$		$(◆,\mathrm{ER},{◆}^I)$		$(◆,\mathrm{ER},{◆}^I)$		$(◆,\mathrm{ER},{◆}^I)$
N(-K)	#states	${\log }_{10}\left(\eta \right)$	pts	time	pts	time	pts	time	pts	time
job scheduling			$(0,3,0)$		$(0,1,1)$		$(1,3,0)$		$(1,1,2)$
10-2	12 554	$-2$	9	1.8	9	41	15	435	16	2 322
		$-3$	44	128	21	834	TO		TO
12-3	116 814	$-2$	11	42	9	798	21	2 026	TO
		$-3$	53	323	TO		TO		TO
17-2	$4.6\cdot {10}^6$	$-2$	14	1 040	TO		22	4 936	TO
		$-3$	58	2 692	TO		TO		TO
polling			$(0,2,0)$		$(0,4,0)$		$(0,0,2)$		$(0,2,2)$
3-2	1 020	$-2$	4	0.3	5	0.6	3	130	12	669
		$-3$	4	0.3	5	0.8	7	3 030	TO
3-3	9 858	$-2$	5	1.3	8	23	6	2 530	TO
		$-3$	6	2.0	19	3 199	TO		TO
4-4	827 735	$-2$	10	963	20	4 349	TO		TO
		$-3$	11	1 509	TO		TO		TO
stream			$(0,2,0)$		$(0,1,1)$		$(0,0,2)$		$(0,2,1)$
30	1 426	$-2$	20	0.9	16	90	16	55	26	268
		$-3$	51	8.8	46	2 686	38	1 341	TO
250	94 376	$-2$	31	50	15	5 830	16	4 050	TO
		$-3$	90	184	TO		TO		TO
1000	$1.5\cdot {10}^6$	$-2$	41	3 765	TO		TO		TO
		$-3$	TO		TO		TO		TO
mutex			$(0,0,3)$		$(0,0,3)$
2	13 476	$-2$	16	351	13	1 166
		$-3$	13	2 739	TO
3	38 453	$-2$	15	2 333	TO

Table 2. Table 2: Additional model details.

	N(-K)	#states	#choices	#transitions	#MS	$\lambda \max$
jobs	10-2	12 554	23 061	34 581	11 531	5.7
	12-3	116 814	225 437	450 783	112 719	8.5
	17-2	4 587 537	8 912 931	13 369 379	4 456 466	5.9
polling	3-2	1 020	1 852	2 477	508	14
	3-3	9 858	18 295	24 536	4 801	14
	4-4	827 735	1 682 325	2 146 086	465 125	16
stream	30	1 426	1 861	2 731	931	8
	250	94 376	125 501	187 751	62 751	8
	1000	1 502 501	2 002 001	3 001 001	1 001 001	8
mutex	2	13 476	31 752	36 120	216	2
	3	38 453	99 132	111 687	8 487	3

Table 3. Table 3: Results for our implementation ( Storm ) and PRISM on the multi-objective MDP benchmarks from  [ 15 ] . All run-times are in seconds.

	benchmark			PRISM			Storm
	instance	#states	$𝕆$	iter	verif	total	pts	iter	verif	total
consensus	$2\_3\_2$	691	$\mathbb{P},\mathbb{P}$	0.019	0.183	0.285	3	0.007	0.010	0.474
	$2\_4\_2$	1 517	$\mathbb{P},\mathbb{P}$	0.038	0.329	0.501	2	0.012	0.017	0.497
	$2\_5\_2$	3 169	$\mathbb{P},\mathbb{P}$	0.053	0.528	0.740	2	0.018	0.028	0.518
	$3\_3\_2$	17 455	$\mathbb{P},\mathbb{P}$	0.232	1.416	1.771	2	0.135	0.193	1.169
	$3\_4\_2$	61 017	$\mathbb{P},\mathbb{P}$	0.854	4.267	4.998	2	0.499	0.806	3.421
	$3\_5\_2$	181 129	$\mathbb{P},\mathbb{P}$	2.835	9.735	10.813	2	1.734	3.639	10.675
zeroconf(-tb)	$4$	5 449	$\mathbb{P},\mathbb{P}$	0.130	6.157	6.423	2	0.077	0.146	0.830
	$6$	10 543	$\mathbb{P},\mathbb{P}$	0.235	12.093	12.428	2	0.213	0.368	1.178
	$8$	17 221	$\mathbb{P},\mathbb{P}$	0.408	22.143	22.596	2	0.467	0.819	1.454
	$2\_14$	29 572	$\mathbb{P},\mathbb{P}$	0.285	45.715	46.311	2	0.615	1.926	2.924
	$4\_10$	19 670	$\mathbb{P},\mathbb{P}$	0.262	40.259	40.780	2	0.568	1.256	2.052
	$4\_14$	42 968	$\mathbb{P},\mathbb{P}$	0.363	96.813	97.631	1	2.706	6.216	7.469
team-form.	$3$	12 475	$\mathbb{P},𝔼$	incorrect			5	0.160	0.257	0.877
	$4$	96 665	$\mathbb{P},𝔼$	incorrect			3	1.360	6.637	9.325
	$5$	907 993	$\mathbb{P},𝔼$	incorrect			3	22.197	866.151	889.889
	$3$	12 475	$\mathbb{P},𝔼,\mathbb{P}$	not supported			10	4.060	1.432	2.020
	$4$	96 665	$\mathbb{P},𝔼,\mathbb{P}$	not supported			13	1.327	9.447	12.256
	$5$	907 993	$\mathbb{P},𝔼,\mathbb{P}$	not supported			8	48.873	894.525	918.858
sched.	$5$	31 965	$𝔼,𝔼$	error				—		1.214
	$25$	633 735	$𝔼,𝔼$	incorrect				—		13.907
	$50$	2 457 510	$𝔼,𝔼$	incorrect				—		53.119
dpm	$100$	636	${ℂ}^{\le },{ℂ}^{\le }$	0.187	0.228	0.298	6	0.143	0.145	0.355
	$200$	636	${ℂ}^{\le },{ℂ}^{\le }$	0.213	0.247	0.312	4	0.210	0.213	0.433
	$300$	636	${ℂ}^{\le },{ℂ}^{\le }$	0.239	0.285	0.360	3	0.205	0.207	0.433

Table 4. Table 4: Results for our implementation ( Storm ) and IMCA for single-objective MAs. All run-times are in seconds.

	benchmark			IMCA	Storm (multi)	Storm (single)
	instance	#states	$𝕆$	verif. time	verif. time	verif. time
jobs	10_2	12 554	${𝔼}_1$	0.009	0.047	0.021
	10_2	12 554	${\mathbb{P}}_2^{\le }$	1.054	2.977	1.702
	12_3	116 814	${𝔼}_1$	0.136	0.556	0.279
	12_3	116 814	${\mathbb{P}}_2^{\le }$	19.938	56.242	31.682
polling	3_3	9 858	${𝔼}_1$	6.254	0.102	0.095
	3_3	9 858	${\mathbb{P}}_1^{\le }$	21.948	54.350	14.163
	4_4	827 735	${𝔼}_1$	3 630.283	52.162	47.746
	4_4	827 735	${\mathbb{P}}_1^{\le }$	3 424.730	8 615.390	1 597.095
stream	30	1 426	${𝔼}_1$	0.005	0.009	0.004
	30	1 426	${\mathbb{P}}_1^{\le }$	0.481	1.578	0.509
	250	94 376	${𝔼}_1$	2.972	1.462	1.261
	250	94 376	${\mathbb{P}}_1^{\le }$	36.663	111.450	33.527
mutex	2	13 476	${\mathbb{P}}_1^{\le }$	1.785	1.217	0.4
	2	13 476	${\mathbb{P}}_4^{\le }$	6.922	4.118	1.008

Equations

$${\mathbf{P}}_{\delta }(s,\alpha ,s^{\prime })=\{\begin{array}{ll}\mathbf{P}(s,\perp ,s^{\prime })\cdot (1-e^{-\mathrm{E}(s)\delta })& \text{if }s\in \mathrm{MS},\alpha =\perp ,s\ne s^{\prime }\\ \mathbf{P}(s,\perp ,s^{\prime })\cdot (1-e^{-\mathrm{E}(s)\delta })+e^{-\mathrm{E}(s)\delta }& \text{if }s\in \mathrm{MS},\alpha =\perp ,s=s^{\prime }\\ \mathbf{P}(s,\alpha ,s^{\prime })& \text{otherwise.}\end{array}$$

$${◊}^{I}G=\{$$

$$I\cap [t,t+t({\kappa }_n)]\ne \varnothing \text{ for }t=T(pref(\pi ,n))\}.$$

$$\mathcal{M},\sigma \models \mathbb{O}⊳\mathbf{p}⟺\mathcal{M},\sigma \models {\mathbb{O}}_i{⊳}_i{p}_i\text{ for all }1\le i\le d.$$

$$⟨\hat{\pi }⟩={\mathrm{ta}}^{-1}(\hat{\pi })=\{\pi \in {FPaths}^{\mathcal{M}}\cup {IPaths}^{\mathcal{M}}\mid \mathrm{ta}(\pi )=\hat{\pi }\}.$$

$$\mathrm{ta}(\sigma )(\hat{\pi },\alpha )={\int }_{\pi \in ⟨\hat{\pi }⟩}\sigma (\pi ,\alpha )\mathrm{d}{\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(\pi \mid ⟨\hat{\pi }⟩).$$

$${\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(◊\{s_6\})={\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(⟨\bar{\pi }⟩)=1-e^{-\mathrm{E}(s_0)}={\mathrm{Pr}}_{\mathrm{ta}(\sigma )}^{{\mathcal{M}}_{\mathcal{D}}}(\bar{\pi })={\mathrm{Pr}}_{\mathrm{ta}(\sigma )}^{{\mathcal{M}}_{\mathcal{D}}}(◊\{s_6\}).$$

$${\int }_{\pi \in ⟨{\hat{\pi }}_{\alpha }⟩}{rew}^{\mathcal{M}}(\pi )\mathrm{d}{\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(\pi )$$

$${rew}^{{\mathcal{M}}_{\mathcal{D}}}({\rho }^{\mathcal{D}}{\hat{\pi }}_{\alpha })\cdot {\mathrm{Pr}}_{\mathrm{ta}(\sigma )}^{{\mathcal{M}}_{\mathcal{D}}}({\hat{\pi }}_{\alpha })={\rho }^{\mathcal{D}}(s_0,\perp )\cdot \mathrm{ta}(\sigma )(s_0\stackrel{\perp }{\to }{s}_3,\alpha )=1-e^{-1}.$$

$${\mathrm{di}(\pi)}=\big{(}s_{0}\xrightarrow{\alpha(\kappa_{0})}\!\!\big{)}^{{m_{0}}}s_{0}\xrightarrow{\alpha(\kappa_{0})}\big{(}s_{1}\xrightarrow{\alpha(\kappa_{1})}\!\!\big{)}^{{m_{1}}}s_{1}\xrightarrow{\alpha(\kappa_{1})}\dots\$$

$$[\bar{\pi }]={\mathrm{di}}^{-1}(\bar{\pi })=\{\pi \in {FPaths}^{\mathcal{M}}\cup {IPaths}^{\mathcal{M}}\mid \mathrm{di}(\pi )=\bar{\pi }\}.$$

$$\mathrm{di}(\sigma )(\bar{\pi },\alpha )={\int }_{\pi \in [\bar{\pi }]}\sigma (\pi ,\alpha )\mathrm{d}{\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(\pi \mid [\bar{\pi }]).$$

$$\mathrm{di}(\sigma )({\bar{\pi }}_2,\alpha )={\int }_{\pi \in [{\bar{\pi }}_2]}\sigma (\pi ,\alpha )\mathrm{d}{\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(\pi \mid [{\bar{\pi }}_2])=\frac{{\int }_{0.8}^{1.0}\mathrm{E}(s_0)e^{-\mathrm{E}(s_0)t}\mathrm{d}t}{{\int }_{0.8}^{1.2}\mathrm{E}(s_0)e^{-\mathrm{E}(s_0)t}\mathrm{d}t}\approx 0.55.$$

$${◊}_{\mathrm{ds}}^{J}G=\{\bar{\pi }\in {IPaths}^{{\mathcal{M}}_{\delta }}\mid \exists n\ge 0:\bar{\pi }[n]\in G\text{ and }|pref(\bar{\pi },n){|}_{\mathrm{ds}}\in J\}.$$

$${\mathrm{Pr}}_{\sigma }^{\mathcal{M}}([{◊}_{\mathrm{ds}}^{J}G])={\mathrm{Pr}}_{\mathrm{di}(\sigma )}^{{\mathcal{M}}_{\delta }}({◊}_{\mathrm{ds}}^{J}G).$$

$${\pi }_1,{\pi }_2\in {◊}^{I}G\cap [{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G]\text{ and }{\pi }_3\in {◊}^{I}G\setminus [{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G].$$

$${\epsilon }^{\downarrow }([a,b])$$

$${\epsilon }^{\uparrow }([a,b])$$

$$\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge^{I}G)\in\mathrm{Pr}^{\mathcal{M}}_{\sigma}([{\lozenge^{I}_{\mathrm{ds}}G}])+\Big{[}{-}\varepsilon^{\downarrow}(I),\,\varepsilon^{\uparrow}(I)\Big{]}$$

$$\begin{array}{r}{\mathrm{Pr}}_{\sigma }({◊}^{I}G)={\mathrm{Pr}}_{\sigma }([{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G])+{\mathrm{Pr}}_{\sigma }({◊}^{I}G\setminus [{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G])-{\mathrm{Pr}}_{\sigma }([{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G]\setminus {◊}^{I}G).\end{array}$$

$${\mathrm{Pr}}_{\sigma }^{\mathcal{M}}({◊}^{I}G\setminus [{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G])\le {\epsilon }^{\uparrow }(I)\text{and }{\mathrm{Pr}}_{\sigma }^{\mathcal{M}}([{◊}_{\mathrm{ds}}^{\mathrm{di}(I)}G]\setminus {◊}^{I}G)\le {\epsilon }^{\downarrow }(I).$$

$$\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge^{I}G)\in\mathrm{Pr}^{{\mathcal{M}_{\delta}}}_{{\mathrm{di}(\sigma)}}(\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G)+\Big{[}{-}\varepsilon^{\downarrow}(I),\,\varepsilon^{\uparrow}(I)\Big{]}$$

$$\varepsilon({\mathbb{O}},{\mathbf{p}})=\bigtimes_{i=1}^{d}\big{[}p_{i}-\varepsilon^{\downarrow}_{i},\,p_{i}+\varepsilon^{\uparrow}_{i}\big{]}\subseteq\mathbb{R}^{d}\ \text{, where }\varepsilon^{\uparrow}_{i}=\begin{cases}\varepsilon^{\uparrow}(I)&\text{if }{\mathbb{O}_{i}}={\mathbb{P}({\lozenge^{I}{G}})}\\ 0&\text{if }{\mathbb{O}_{i}}={\mathbb{E}({\#j,G})}\end{cases}$$

$$A^{-}$$

$$A^{+}$$

$${\rho }_i^{\mathcal{D}}(s,\alpha )=\{\begin{array}{ll}{\rho }_i(s,\alpha )& \text{if }s\in \mathrm{PS}\\ {\rho }_i(s,\perp )+\text{nicefrac}1\mathrm{E}(s)\cdot {\rho }_i(s)& \text{if }s\in \mathrm{MS}\text{ and }\alpha =\perp \\ 0& \text{otherwise}.\end{array}$$

$$\rho_{i}^{\delta}(s,\alpha)=\begin{cases}\rho_{i}(s,\alpha)&\text{if }s\in\mathrm{PS}\\ \big{(}\rho_{i}(s,\bot)+\nicefrac{{1}}{{{\mathrm{E}(s)}}}\cdot\rho_{i}(s)\big{)}\cdot\big{(}1-e^{-{\mathrm{E}(s)}\delta}\big{)}&\text{if }s\in\mathrm{MS}\text{ and }\alpha=\bot\\ 0&\text{otherwise}.\end{cases}$$

$${\mathrm{Pr}}_{\sigma ,\pi }^{Steps}(T)=\{\begin{array}{ll}\sum _{(0,\alpha ,s^{\prime })\in T}\sigma (\pi ,\alpha )\cdot \mathbf{P}(s,\alpha ,s^{\prime })& \text{if }s\in \mathrm{PS}\\ {\int }_{\begin{array}{c}\{t\mid (t,\perp ,s^{\prime })\in T\}\end{array}}\mathrm{E}(s)\cdot e^{-\mathrm{E}(s)t}\cdot \sum _{(t,\perp ,s^{\prime })\in T}\mathbf{P}(s,\perp ,s^{\prime })\mathrm{d}t& \text{if }s\in \mathrm{MS}\end{array}$$

$$Cyl(\Pi )=\{\pi \stackrel{{\kappa }_n}{\to }{s}_{n+1}\stackrel{{\kappa }_{n+1}}{\to }\cdots \in {IPaths}^{\mathcal{M}}\mid \pi \in \Pi \}.$$

$${rew}^{\mathcal{M}}({\pi }^{\prime })=\sum _{i=0}^{|{\pi }^{\prime }|-1}\rho (s_i)\cdot t({\kappa }_i)+\rho (s_i,\alpha ({\kappa }_i)).$$

$${rew}^{\mathcal{M}}(\rho ,\pi ,G)=\{\begin{array}{ll}{rew}^{\mathcal{M}}(pref(\pi ,n))& \text{ if }n=\min \{i\ge 0\mid s_i\in G\}\\ {\lim }_{n\to \infty }{rew}^{\mathcal{M}}(pref(\pi ,n))& \text{ if }{s}_i\notin G\text{ for all }i\ge 0.\end{array}$$

$${\mathrm{ER}}_{\sigma }^{\mathcal{M}}(\rho ,G)={\int }_{\pi \in {IPaths}^{\mathcal{M}}}{rew}^{\mathcal{M}}(\rho ,\pi ,G)\mathrm{d}{\mathrm{Pr}}_{\sigma }^{\mathcal{M}}(\pi ).$$

Full text

1 Introduction

Markov automata [1, 2] extend labeled transition systems with probabilistic branching and exponentially distributed delays. They are a compositional variant of continuous-time Markov decision processes (CTMDPs), in a similar vein as Segala’s probabilistic automata extend classical MDPs. Transitions of a Markov automaton (MA) lead from states to probability distributions over states, and are either labeled with actions (allowing for interaction) or real numbers (rates of exponential distributions). MAs are used in reliability engineering [3], hardware design [4], data-flow computation [5], dependability [6] and performance evaluation [7], as MAs are a natural semantic framework for modeling formalisms such as AADL, dynamic fault trees, stochastic Petri nets, stochastic activity networks, SADF etc. The verification of MAs so far focused on single objectives such as reachability, timed reachability, expected costs, and long-run averages [8, 9, 10, 11, 12]. These analyses cannot treat objectives that are mutually influencing each other, like quickly reaching a target is more costly. The aim of this paper is to analyze multiple objectives on MAs at once and to facilitate trade–off analysis by approximating Pareto curves.

Consider the stochastic job scheduling problem of [13]: perform $n$ jobs with exponential service times on $k$ identical processors under a pre-emptive scheduling policy. Once a job finishes, all $k$ processors can be assigned any of the $m$ remaining jobs. When $n{-}m$ jobs are finished, this yields $\binom{m}{k}$ non-deterministic choices.

The largest-expected-service-time-first-policy is optimal to minimize the expected time to complete all jobs [13]. It is unclear how to schedule when imposing extra constraints, e.g., requiring a high probability to finish a batch of $c$ jobs within a tight deadline (to accelerate their post-processing), or having a low average waiting time. These multiple objectives involve non-trivial trade–offs. Our algorithms analyze such trade–offs. Fig. 1, e.g., shows the obtained result for 12 jobs and 3 processors. It approximates the set of points $(p_{1},p_{2})$ for schedules achieving that (1) the expected time to complete all jobs is at most $p_{1}$ and (2) the probability to finish half of the jobs within an hour is at least $p_{2}$.

This paper presents techniques to verify MAs with multiple objectives. We consider multiple (un)timed reachability and expected reward objectives as well as their combinations. Put shortly, we reduce all these problems to instances of multi-objective verification problems on classical MDPs. For multi-objective queries involving (combinations of) untimed reachability and expected reward objectives, corresponding algorithms on the underlying MDP can be used. In this case, the MDP is simply obtained by ignoring the timing information, see Fig. 2(b). The crux is in relating MA schedulers—that can exploit state sojourn times to optimize their decisions—to MDP schedulers. For multiple timed reachability objectives, digitization [8, 9] is employed to obtain an MDP, see Fig. 2(c). The key is to mimic sojourn times by self-loops with appropriate probabilities. This provides a sound arbitrary close approximation of the timed behavior and also allows to combine timed reachability objectives with other types of objectives. The main contribution is to show that digitization is sound for all possible MA schedulers. This requires a new proof strategy as the existing ones are tailored to optimizing a single objective. All proofs can be found in the appendix. Experiments on instances of four MA benchmarks show encouraging results. Multiple untimed reachability and expected reward objectives can be efficiently treated for models with millions of states. As for single objectives [9], timed reachability is more expensive. Our implementation is competitive to PRISM for multi-objective MDPs [14, 15] and to IMCA [9] for single-objective MAs.

Related work.

Multi-objective decision making for MDPs with discounting and long-run objectives has been well investigated; for a recent survey, see [16]. Etessami et al. [17] consider verifying finite MDPs with multiple $\omega$-regular objectives. Other multiple objectives include expected rewards under worst-case reachability [18, 19], quantiles and conditional probabilities [20], mean pay-offs and stability [21], long-run objectives [22, 23], total average discounted rewards under PCTL [24], and stochastic shortest path objectives [25]. This has been extended to MDPs with unknown cost function [26], infinite-state MDPs [27] arising from two-player timed games in a stochastic environment, and stochastic two-player games [28]. To the best of our knowledge, this is the first work on multi-objective MDPs extended with random timing.

2 Preliminaries

Notations.

The set of real numbers is denoted by $\mathbb{R}$, and we write $\mathbb{R}_{>0}=\{x\in\mathbb{R}\mid x>0\}$ and $\mathbb{R}_{\geq 0}=\mathbb{R}_{>0}\cup\{0\}$. For a finite set $S$, $\mathit{Dist}(S)$ denotes the set of probability distributions over $S$. $\mu\in\mathit{Dist}(S)$ is Dirac if $\mu(s)=1$ for some $s\in S$.

2.1 Models

Markov automata generalize both Markov decision processes (MDPs) and continuous time Markov chains (CTMCs). They are extended with rewards (or, equivalently, costs) to allow modelling, e.g., energy consumption.

Definition 1 (Markov automaton)

A Markov automaton (MA) is a tuple $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ where $S$ is a finite set of states with initial state ${s_{0}}\in S$, $\mathit{Act}$ is a finite set of actions with $\bot\in\mathit{Act}$ and $\mathit{Act}\cap\mathbb{R}_{\geq 0}=\emptyset$,

• •

{\rightarrow}\subseteq S\times(\mathit{Act}\mathbin{\mathchoice{\ooalign{\displaystyle\cup\cr\raise 0.55556pt\hbox{\set@color\displaystyle\cdot}}}{\ooalign{\textstyle\cup\cr\raise 0.55556pt\hbox{\set@color\textstyle\cdot}}}{\ooalign{\scriptstyle\cup\cr\raise 0.38889pt\hbox{\set@color\scriptstyle\cdot}}}{\ooalign{\scriptscriptstyle\cup\cr\raise 0.27779pt\hbox{\set@color\scriptscriptstyle\cdot}}}}\mathbb{R}_{>0})\times\mathit{Dist}(S) is a set of transitions such that for all $s\in S$ there is at most one transition $(s,\lambda,\mu)\in{\rightarrow}$ with $\lambda\in\mathbb{R}_{>0}$, and

• •

$\rho_{1},\dots,\rho_{\ell}$ with $\ell\geq 0$ are reward functions \rho_{i}\colon S\mathbin{\mathchoice{\ooalign{\displaystyle\cup\cr\raise 0.55556pt\hbox{\set@color\displaystyle\cdot}}}{\ooalign{\textstyle\cup\cr\raise 0.55556pt\hbox{\set@color\textstyle\cdot}}}{\ooalign{\scriptstyle\cup\cr\raise 0.38889pt\hbox{\set@color\scriptstyle\cdot}}}{\ooalign{\scriptscriptstyle\cup\cr\raise 0.27779pt\hbox{\set@color\scriptscriptstyle\cdot}}}}(S\times\mathit{Act})\to\mathbb{R}_{\geq 0}.

In the remainder of the paper, let $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ denote an MA. A transition $(s,\gamma,\mu)\in{\rightarrow}$, denoted by $s\xrightarrow{\gamma}\mu$, is called probabilistic if $\gamma\in\mathit{Act}$ and Markovian if $\gamma\in\mathbb{R}_{>0}$. In the latter case, $\gamma$ is the rate of an exponential distribution, modeling a time-delayed transition. Probabilistic transitions fire instantaneously. The successor state is determined by $\mu$, i.e., we move to $s^{\prime}$ with probability $\mu(s^{\prime})$. Probabilistic (Markovian) states PS (MS) have an outgoing probabilistic (Markovian) transition, respectively: $\mathrm{PS}=\{s\in S\mid s\xrightarrow{\alpha}\mu,\alpha\in\mathit{Act}\}$ and $\mathrm{MS}=\{s\in S\mid s\xrightarrow{\lambda}\mu,\lambda\in\mathbb{R}_{>0}\}$. The exit rate ${\mathrm{E}(s)}$ of $s\in\mathrm{MS}$ is uniquely given by $s\xrightarrow{{\mathrm{E}(s)}}\mu$. The transition probabilities of $\mathcal{M}$ are given by the function $\mathbf{P}\colon S\times\mathit{Act}\times S\to[0,1]$ satisfying $\mathbf{P}(s,\alpha,s^{\prime})=\mu(s^{\prime})$ if either $s\xrightarrow{\alpha}\mu$ or ($\alpha=\bot$ and $s\xrightarrow{{\mathrm{E}(s)}}\mu$) and $\mathbf{P}(s,\alpha,s^{\prime})=0$ in all other cases. The value $\mathbf{P}(s,\alpha,s^{\prime})$ corresponds to the probability to move from $s$ with action $\alpha$ to $s^{\prime}$. The enabled actions at state $s$ are given by $\mathit{Act}(s)=\{\alpha\in\mathit{Act}\mid\exists s^{\prime}\in S\colon\mathbf{P}(s,\alpha,s^{\prime})>0\}$.

Example 1

Fig. 2(a) shows an MA $\mathcal{M}$. We do not depict Dirac probability distributions. Markovian transitions are illustrated by dashed arrows.

We assume action-deterministic MAs: $|\{\mu\in\mathit{Dist}(S)\mid s\xrightarrow{\alpha}\mu\}|\leq 1$ holds for all $s\in S$ and $\alpha\in\mathit{Act}$. Terminal states $s\notin\mathrm{PS}\cup\mathrm{MS}$ are excluded by adding a Markovian self-loop. As standard for MAs [1, 2], we impose the maximal progress assumption, i.e., probabilistic transitions take precedence over Markovian ones. Thus, we remove transitions $s\xrightarrow{\lambda}\mu$ for $s\in\mathrm{PS}$ and $\lambda\in\mathbb{R}_{>0}$ which yields S=\mathrm{PS}\mathbin{\mathchoice{\ooalign{\displaystyle\cup\cr\raise 0.55556pt\hbox{\set@color\displaystyle\cdot}}}{\ooalign{\textstyle\cup\cr\raise 0.55556pt\hbox{\set@color\textstyle\cdot}}}{\ooalign{\scriptstyle\cup\cr\raise 0.38889pt\hbox{\set@color\scriptstyle\cdot}}}{\ooalign{\scriptscriptstyle\cup\cr\raise 0.27779pt\hbox{\set@color\scriptscriptstyle\cdot}}}}\mathrm{MS}. MAs with Zeno behavior, where infinitely many actions can be taken within finite time with non-zero probability, are unrealistic and considered a modeling error.

A reward function $\rho_{i}$ defines state rewards and action rewards. When sojourning in a state $s$ for $t$ time units, the state reward $\rho_{i}(s)\cdot t$ is obtained. Upon taking a transition $s\xrightarrow{\gamma}\mu$, we collect action reward $\rho_{i}(s,\gamma)$ (if $\gamma\in\mathit{Act}$) or $\rho(s,\bot)$ (if $\gamma\in\mathbb{R}_{>0}$). For presentation purposes, in the remainder of this section, rewards are omitted. Full definitions with rewards can be found in App. 0.A.1.

Definition 2 (Markov decision process [29])

A Markov decision process (MDP) is a tuple $\mathcal{D}=(S,\mathit{Act},\mathbf{P},{s_{0}},\emptyset)$ with $S,{s_{0}},\mathit{Act}$ as in Def. 1 and $\mathbf{P}\colon S\times\mathit{Act}\times S\to[0,1]$ are the transition probabilities satisfying $\sum_{s^{\prime}\in S}\mathbf{P}(s,\alpha,s^{\prime})\in\{0,1\}$ for all $s\in S$ and $\alpha\in\mathit{Act}$.

MDPs are MAs without Markovian states and thus without timing aspects, i.e., MDPs exhibit probabilistic branching and non-determinism. Zeno behavior is not a concern, as we do not consider timing aspects. The underlying MDP of an MA abstracts away from its timing:

Definition 3 (Underlying MDP)

The MDP ${\mathcal{M}_{\mathcal{D}}}=(S,\mathit{Act},\mathbf{P},{s_{0}},\emptyset)$ is the underlying MDP of MA $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\emptyset)$ with transition probabilities $\mathbf{P}$.

The digitization ${\mathcal{M}_{\delta}}$ of $\mathcal{M}$ w.r.t. some digitization constant $\delta\in\mathbb{R}_{>0}$ is an MDP which digitizes the time [8, 9]. The main difference between ${\mathcal{M}_{\mathcal{D}}}$ and ${\mathcal{M}_{\delta}}$ is that the latter also introduces self-loops which describe the probability to stay in a Markovian state for $\delta$ time units. More precisely, the outgoing transitions of states $s\in\mathrm{MS}$ in ${\mathcal{M}_{\delta}}$ represent that either (1) a Markovian transition in $\mathcal{M}$ was taken within $\delta$ time units, or (2) no transition is taken within $\delta$ time units – which is captured by taking the self-loop in ${\mathcal{M}_{\delta}}$. Counting the taken self-loops at $s\in\mathrm{MS}$ allows to approximate the sojourn time in $s$.

Definition 4 (Digitization of an MA)

For MA $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\emptyset)$ with transition probabilities $\mathbf{P}$ and digitization constant $\delta\in\mathbb{R}_{>0}$, the digitization of $\mathcal{M}$ w.r.t. $\delta$ is the MDP ${\mathcal{M}_{\delta}}=(S,\mathit{Act},\mathbf{P}_{\delta},{s_{0}},\emptyset)$ where

[TABLE]

Example 2

Fig. 2 shows an MA $\mathcal{M}$ with its underlying MDP ${\mathcal{M}_{\mathcal{D}}}$ and a digitization ${\mathcal{M}_{\delta}}$ for unspecified $\delta\in\mathbb{R}_{>0}$.

Paths and schedulers.

Paths represent runs of $\mathcal{M}$ starting in the initial state. Let $t(\kappa)=0$ and $\alpha(\kappa)=\kappa$, if $\kappa\in\mathit{Act}$, and $t(\kappa)=\kappa$ and $\alpha(\kappa)=\bot$, if $\kappa\in\mathbb{R}_{\geq 0}$.

Definition 5 (Infinite path)

An infinite path of MA $\mathcal{M}$ with transition probabilities $\mathbf{P}$ is an infinite sequence $\pi=s_{0}\xrightarrow{\kappa_{0}}s_{1}\xrightarrow{\kappa_{1}}\dots$ of states $s_{0},s_{1},\dots\in S$ and stamps \kappa_{0},\kappa_{1},\dots\in\mathit{Act}\mathbin{\mathchoice{\ooalign{\displaystyle\cup\cr\raise 0.55556pt\hbox{\set@color\displaystyle\cdot}}}{\ooalign{\textstyle\cup\cr\raise 0.55556pt\hbox{\set@color\textstyle\cdot}}}{\ooalign{\scriptstyle\cup\cr\raise 0.38889pt\hbox{\set@color\scriptstyle\cdot}}}{\ooalign{\scriptscriptstyle\cup\cr\raise 0.27779pt\hbox{\set@color\scriptscriptstyle\cdot}}}}\mathbb{R}_{\geq 0} such that (1) $\sum_{i=0}^{\infty}t(\kappa_{i})=\infty$, and for any $i\geq 0$ it holds that (2) $\mathbf{P}(s_{i},\alpha(\kappa_{i}),s_{i+1})>0$, (3) $s_{i}\in\mathrm{PS}$ implies $\kappa_{i}\in\mathit{Act}$, and (4) $s_{i}\in\mathrm{MS}$ implies $\kappa_{i}\in\mathbb{R}_{\geq 0}$.

An infix $s_{i}\xrightarrow{\kappa_{i}}s_{i+1}$ of a path $\pi$ represents that we stay at $s_{i}$ for $t(\kappa_{i})$ time units and then perform action $\alpha(\kappa_{i})$ and move to state $s_{i+1}$. Condition (1) excludes Zeno paths, condition (2) ensures positive transition probabilities, and conditions (3) and (4) assert that stamps $\kappa_{i}$ match the transition type at $s_{i}$.

A finite path is a finite prefix $\pi^{\prime}=s_{0}\xrightarrow{\kappa_{0}}\dots\xrightarrow{\kappa_{n-1}}s_{n}$ of an infinite path. The length of $\pi^{\prime}$ is $\lvert\pi^{\prime}\rvert=n$, its last state is $\mathit{last}(\pi^{\prime})=s_{n}$, and the time duration is $\mathit{T}(\pi^{\prime})=\sum_{0\leq i<\lvert\pi^{\prime}\rvert}t(\kappa_{i})$. We denote the sets of finite and infinite paths of $\mathcal{M}$ by ${\mathit{FPaths}^{\mathcal{M}}}$ and ${\mathit{IPaths}^{\mathcal{M}}}$, respectively. The superscript $\mathcal{M}$ is omitted if the model is clear from the context. For a finite or infinite path $\pi=s_{0}\xrightarrow{\kappa_{0}}s_{1}\xrightarrow{\kappa_{1}}\dots$ the prefix of $\pi$ of length $n$ is denoted by $\mathit{pref}(\pi,n)$. The $i$th state visited by $\pi$ is given by ${\pi[i]}=s_{i}$. The time-abstraction $\mathrm{ta}(\pi)$ of $\pi$ removes all sojourn times and is a path of the underlying MDP ${\mathcal{M}_{\mathcal{D}}}$: $\mathrm{ta}(\pi)=s_{0}\xrightarrow{\alpha(\kappa_{0})}s_{1}\xrightarrow{\alpha(\kappa_{1})}\dots$ . Paths of ${\mathcal{M}_{\mathcal{D}}}$ are also referred to as the time-abstract paths of $\mathcal{M}$.

Definition 6 (Generic scheduler)

A generic scheduler for $\mathcal{M}$ is a measurable function $\sigma\colon{\mathit{FPaths}}\times\mathit{Act}\to[0,1]$ such that $\sigma(\pi,\cdot)\in\mathit{Dist}(\mathit{Act}(\mathit{last}(\pi)))$ for each $\pi\in{\mathit{FPaths}}$.

A scheduler $\sigma$ for $\mathcal{M}$ resolves the non-determinism of $\mathcal{M}$: $\sigma(\pi,\alpha)$ is the probability to take transition $\mathit{last}(\pi)\xrightarrow{\alpha}\mu$ after observing the run $\pi$. The set of such schedulers is denoted by ${\mathrm{GM}^{\mathcal{M}}}$ (${\mathrm{GM}}$ if $\mathcal{M}$ is clear from the context). $\sigma\in{\mathrm{GM}}$ is deterministic if the distribution $\sigma(\pi,\cdot)$ is Dirac for any $\pi$. Time-abstract schedulers behave independently of the time-stamps of the given path, i.e., $\sigma(\pi,\alpha)=\sigma(\pi^{\prime},\alpha)$ for all actions $\alpha$ and paths $\pi,\pi^{\prime}$ with $\mathrm{ta}(\pi)=\mathrm{ta}(\pi^{\prime})$. We write ${\mathrm{TA}^{\mathcal{M}}}$ to denote the set of time-abstract schedulers of $\mathcal{M}$. GM is the most general scheduler class for MAs. For MDPs, the most general scheduler class is ${\mathrm{TA}}$.

2.2 Objectives

An objective ${\mathbb{O}_{i}}$ is a representation of a quantitative property like the probability to reach an error state, or the expected energy consumption. To express Boolean properties (e.g., the probability to reach an error state is below $p_{i}$), ${\mathbb{O}_{i}}$ is combined with a threshold $\vartriangleright_{i}p_{i}$ where $\vartriangleright_{i}\,\in\{<,\leq,>,\geq\}$ is a threshold relation and $p_{i}\in\mathbb{R}$ is a threshold value. Let $\mathcal{M},\sigma\models{\mathbb{O}_{i}}\vartriangleright_{i}p_{i}$ denote that the MA $\mathcal{M}$ under scheduler $\sigma\in{\mathrm{GM}}$ satisfies the property ${\mathbb{O}_{i}}\vartriangleright_{i}p_{i}$.

Reachability objectives.

$I\subseteq\mathbb{R}$ is a time interval if it is of the form $I=[a,b]$ or $I=[a,\infty)$, where $0\leq a<b$. The set of paths reaching a set of goal states $G\subseteq S$ in time $I$ is defined as

[TABLE]

We write $\lozenge G$ instead of $\lozenge^{[0,\infty)}G$. A probability measure $\mathrm{Pr}^{\mathcal{M}}_{\sigma}$ on sets of infinite paths is defined, which generalizes both the standard probability measure on MDPs and on CTMCs. A formal definition is given in App. 0.A.2.1.

Definition 7 (Reachability objective)

A reachability objective has the form ${\mathbb{P}({\lozenge^{I}{G}})}$ for time interval $I$ and goal states $G$. The objective is timed if $I\neq[0,\infty)$ and untimed otherwise. For MA $\mathcal{M}$ and scheduler $\sigma\in{\mathrm{GM}}$, let $\mathcal{M},\sigma\models{\mathbb{P}({\lozenge^{I}{G}})}\vartriangleright_{i}p_{i}$ iff $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge^{I}G)\vartriangleright_{i}p_{i}$.

Expected reward objectives.

Expected rewards $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho_{j},G)$ define the expected amount of reward collected (w.r.t. $\rho_{j}$) until a goal state in $G\subseteq S$ is reached. This is a straightforward generalization of the notion on CTMCs and MDPs. A formal definition is found in App. 0.A.2.2.

Definition 8 (Expected reward objective)

An expected reward objective has the form ${\mathbb{E}({\#j,G})}$ where $j$ is the index of reward function $\rho_{j}$ and $G\subseteq S$. For MA $\mathcal{M}$ and scheduler $\sigma\in{\mathrm{GM}}$, let $\mathcal{M},\sigma\models{\mathbb{E}({\#j,G})}\vartriangleright_{i}p_{i}$ iff $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho_{j},G)\vartriangleright_{i}p_{i}$.

Expected time objectives ${\mathbb{E}({\mathit{T},G})}$ are expected reward objectives that consider the reward function $\rho_{\mathit{T}}$ with $\rho_{\mathit{T}}(s)=1$ if $s\in\mathrm{MS}$ and all other rewards are zero.

3 Multi-objective Model Checking

Standard model checking considers objectives individually. This approach is not feasible when we are interested in multiple objectives that should be fulfilled by the same scheduler, e.g., a scheduler that maximizes the expected profit might violate certain safety constraints. Multi-objective model checking aims to analyze multiple objectives at once and reveals possible trade-offs.

Definition 9 (Satisfaction of multiple objectives)

Let $\mathcal{M}$ be an MA and $\sigma\in{\mathrm{GM}}$. For objectives ${\mathbb{O}}=({\mathbb{O}_{1}},\dots,{\mathbb{O}_{d}})$ with threshold relations ${\vartriangleright}=(\vartriangleright_{1},\dots,\vartriangleright_{d})\in\{<,\leq,>,\geq\}^{d}$ and threshold values ${\mathbf{p}}=(p_{1},\dots,p_{d})\in\mathbb{R}^{d}$ let

[TABLE]

Furthermore, let $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\iff\exists\sigma\in{\mathrm{GM}}$ such that $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$.

If $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$, the point ${\mathbf{p}}\in\mathbb{R}^{d}$ is achievable in $\mathcal{M}$ with scheduler $\sigma$. The set of achievable points of $\mathcal{M}$ w.r.t. ${\mathbb{O}}$ and ${\mathbf{p}}$ is $\{{\mathbf{p}}\in\mathbb{R}^{d}\mid\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\}.$ This definition is compatible with the notions on MDPs as given in [15, 17].

Example 3

Fig. 3(b) and Fig. 3(c) depict the set of achievable points of the MA $\mathcal{M}$ from Fig. 3(a) w.r.t. relations ${\vartriangleright}=(\geq,\geq)$ and objectives $({\mathbb{P}({\lozenge\{s_{2}\}})},{\mathbb{P}({\lozenge\{s_{4}\}})})$ and $({\mathbb{P}({\lozenge\{s_{2}\}})},{\mathbb{P}({\lozenge^{[0,2]}{\{s_{4}\}}})})$, respectively. Using the set of achievable points, we can answer Pareto, numerical, and achievability queries as considered in [15], e.g., the Pareto front lies on the border of the set.

Schedulers.

For single-objective model checking on MAs, it suffices to consider deterministic schedulers [30]. For untimed reachability and expected rewards even time-abstract deterministic schedulers suffice [30]. Multi-objective model checking on MDPs requires history-dependent, randomized schedulers [17]. On MAs, schedulers may also employ timing information to make optimal choices, even if only untimed objectives are considered.

Example 4

Consider the MA $\mathcal{M}$ in Fig. 3(a) with untimed objectives ${\mathbb{P}({\lozenge\{s_{2}\}})}\geq 0.5$ and ${\mathbb{P}({\lozenge\{s_{4}\}})}\geq 0.5$. A simple graph argument yields that both properties are only satisfied if action $\alpha$ is taken with probability exactly a half. Thus, on the underlying MDP, no deterministic scheduler satisfies both objectives. On the MA however, paths can be distinguished by their sojourn time in $s_{0}$. As the probability mass to stay in $s_{0}$ for at most $\ln(2)$ is exactly $0.5$, a timed scheduler $\sigma$ with $\sigma(s_{0}\xrightarrow{t}s_{1},\alpha)=1$ if $t\leq\ln(2)$ and [math] otherwise does satisfy both objectives.

Theorem 3.1 ()

For some MA $\mathcal{M}$ with $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$, no deterministic time-abstract scheduler $\sigma$ satisfies $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$.

The geometric shape of the achievable points.

Like for MDPs [17], the set of achievable points of any combination of aforementioned objectives is convex.

Proposition 1 ()

The set $\{{\mathbf{p}}\in\mathbb{R}^{d}\mid\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\}$ is convex.

For MDPs, the set of achievable points is a convex polytope where the vertices can be realized by deterministic schedulers that use memory bounded by the number of objectives. As there are finitely many such schedulers, the polytope is finite [17], i.e., it can be represented by a finite number of vertices. This result does not carry over to MAs. For example, the achievable points of the MA from Fig. 3(a) together with the objectives $({\mathbb{P}({\lozenge\{s_{2}\}})},{\mathbb{P}({\lozenge^{[0,2]}{\{s_{4}\}}})})$ form the infinite polytope shown in Fig. 3(c). The insight here is that for any sojourn time $t\leq 2$ in $s_{0}$, the timing information is relevant for optimal schedulers: The shorter the sojourn time in $s_{0}$, the higher the probability to reach $s_{4}$ within the time bound.

Theorem 3.2 ()

For some MA $\mathcal{M}$ and objectives ${\mathbb{O}}$, the polytope $\{{\mathbf{p}}\in\mathbb{R}^{d}\mid\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\}$ is not finite.

As infinite convex polytopes cannot be represented by a finite number of vertices, any method extending the approach of [15] – which computes these vertices – can only approximate the set of achievable points.

Problem statement.

For an MA and objectives with threshold relations, construct arbitrarily tight over- and under-approximations of the achievable points.

4 Analysis of Markov Automata with Multiple Objectives

The state-of-the-art in single-objective model checking of MA is to reduce the MA to an MDP, cf. [8, 9, 10], for which efficient algorithms exist. We aim to lift this approach to multi-objective model checking. Assume MA $\mathcal{M}$ and objectives ${\mathbb{O}}$ with threshold relations $\vartriangleright$. We discuss how the set of achievable points of $\mathcal{M}$ relates to the set of achievable points of an MDP. The key challenge is to deal with timing information—even for untimed objectives—and to consider schedulers beyond those optimizing single objectives. We obtain:

• •

For untimed reachability and expected reward objectives, the achievable points of $\mathcal{M}$ equal those of its underlying MDP, cf. Theorems 4.1 and 4.2.

• •

For timed reachability objectives, the set of achievable points of a digitized MDP ${\mathcal{M}_{\delta}}$ provides a sound approximation of the achievable points of $\mathcal{M}$, cf. Theorem 4.3. Corollary 1 gives the precision of the approximation.

4.1 Untimed Reachability Objectives

Although timing information is essential for deterministic schedulers, cf. Theorem 3.1, timing information does not strengthen randomized schedulers:

Theorem 4.1 ()

For MA $\mathcal{M}$ and untimed reachability objectives ${\mathbb{O}}$ it holds that $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\iff\mathit{achieve}^{{\mathcal{M}_{\mathcal{D}}}}({\mathbb{O}}\vartriangleright{\mathbf{p}}).$

The main idea for proving Theorem 4.1 is to construct for scheduler $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ a time-abstract scheduler ${\mathrm{ta}(\sigma)}\in{\mathrm{TA}^{{\mathcal{M}_{\mathcal{D}}}}}$ such that they both induce the same untimed reachability probabilities. To this end, we discuss the connection between probabilities of paths of MA $\mathcal{M}$ and paths of MDP ${\mathcal{M}_{\mathcal{D}}}$.

Definition 10 (Induced paths of a time-abstract path)

The set of induced paths on MA $\mathcal{M}$ of a path $\hat{\pi}$ of ${\mathcal{M}_{\mathcal{D}}}$ is given by

[TABLE]

The set $\langle{\hat{\pi}}\rangle$ contains all paths of $\mathcal{M}$ where replacing sojourn times by $\bot$ yields $\hat{\pi}$.

For $\sigma\in{\mathrm{GM}}$, the probability distribution $\sigma(\pi,\cdot)\in\mathit{Dist}(\mathit{Act})$ might depend on the sojourn times of the path $\pi$. The time-abstract scheduler ${\mathrm{ta}(\sigma)}$ weights the distribution $\sigma(\pi,\cdot)$ with the probability masses of the paths $\pi\in\langle{\hat{\pi}}\rangle$.

Definition 11 (Time-abstraction of a scheduler)

The time-abstraction of $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ is defined as ${\mathrm{ta}(\sigma)}\in{\mathrm{TA}^{{\mathcal{M}_{\mathcal{D}}}}}$ such that for any $\hat{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\mathcal{D}}}}}$

[TABLE]

The term $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\pi\mid\langle{\hat{\pi}}\rangle)$ represents the probability for a path in $\langle{\hat{\pi}}\rangle$ to have sojourn times as given by $\pi$. The value ${\mathrm{ta}(\sigma)}(\hat{\pi},\alpha)$ coincides with the probability that $\sigma$ picks action $\alpha$, given that the time-abstract path $\hat{\pi}$ was observed.

Example 5

Consider the MA $\mathcal{M}$ in Fig. 2(a) and the scheduler $\sigma$ choosing $\alpha$ at state $s_{3}$ iff the sojourn time at $s_{0}$ is at most one. Then ${\mathrm{ta}(\sigma)}(s_{0}\xrightarrow{\bot}s_{3},\alpha)=1-e^{-{\mathrm{E}(s_{0})}}$, the probability that $s_{0}$ is left within one time unit. For $\bar{\pi}=s_{0}\xrightarrow{\bot}s_{3}\xrightarrow{\alpha}s_{6}$ we have

[TABLE]

In the example, the considered scheduler and its time-abstraction induce the same untimed reachability probabilities. We generalize this observation.

Lemma 1 ()

For any $\hat{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\mathcal{D}}}}}$ we have $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\langle{\hat{\pi}}\rangle)=\mathrm{Pr}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\hat{\pi}).$

The result is lifted to untimed reachability probabilities.

Proposition 2 ()

For any $G\subseteq S$ it holds that $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge G)=\mathrm{Pr}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\lozenge G).$

As the definition of ${\mathrm{ta}(\sigma)}$ is independent of the considered set of goal states $G\subseteq S$, Proposition 2 can be lifted to multiple untimed reachability objectives.

Proof of Theorem 4.1 (sketch).

By applying Proposition 2, we can show that $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}\iff{\mathcal{M}_{\mathcal{D}}},{\mathrm{ta}(\sigma)}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$ for any scheduler $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ and untimed reachability objectives ${\mathbb{O}}=({\mathbb{P}({\lozenge G_{1}})},\dots,{\mathbb{P}({\lozenge G_{d}})})$ with thresholds $\vartriangleright{\mathbf{p}}$. Theorem 4.1 is a direct consequence of this.

4.2 Expected Reward Objectives

The results for expected reward objectives are similar to untimed reachability objectives: An analysis of the underlying MDP suffices. We show the following extension of Theorem 4.1 to expected reward objectives.

Theorem 4.2 ()

For MA $\mathcal{M}$ and untimed reachability and expected reward objectives ${\mathbb{O}}$: $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\iff\mathit{achieve}^{{\mathcal{M}_{\mathcal{D}}}}({\mathbb{O}}\vartriangleright{\mathbf{p}}).$

To prove this, we show that a scheduler $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ and its time-abstraction ${\mathrm{ta}(\sigma)}\in{\mathrm{TA}}$ induce the same expected rewards on $\mathcal{M}$ and ${\mathcal{M}_{\mathcal{D}}}$, respectively. Theorem 4.2 follows then analogously to Theorem 4.1.

Proposition 3 ()

Let $\rho$ be some reward function of $\mathcal{M}$ and let $\rho^{\mathcal{D}}$ be its counterpart for ${\mathcal{M}_{\mathcal{D}}}$. For $G\subseteq S$ we have $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,G)=\mathrm{ER}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\rho^{\mathcal{D}},G).$

Notice that $\rho^{\mathcal{D}}$ encodes the expected reward of $\mathcal{M}$ obtained in a state $s$ by assuming the sojourn time to be the expected sojourn time $\nicefrac{{1}}{{E(s)}}$. Although the claim is similar to Proposition 2, its proof cannot be adapted straightforwardly. In particular, the analogon to Lemma 1 does not hold: The expected reward collected along a time-abstract path $\hat{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\mathcal{D}}}}}$ does in general not coincide for $\mathcal{M}$ and ${\mathcal{M}_{\mathcal{D}}}$.

Example 6

We consider standard notations for rewards as detailed in App. 0.A.2.2. Let $\mathcal{M}$ be the MA with underlying MDP ${\mathcal{M}_{\mathcal{D}}}$ as shown in Fig. 2. Let $\rho(s_{0})=1$ and zero otherwise. Reconsider the scheduler $\sigma$ from Example 5. Let $\hat{\pi}_{\alpha}=s_{0}\xrightarrow{\bot}s_{3}\xrightarrow{\alpha}s_{6}$. The probability $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\{s_{0}\xrightarrow{t}s_{3}\xrightarrow{\alpha}s_{6}\in\langle{\hat{\pi}_{\alpha}}\rangle\mid t>1\})$ is zero since $\sigma$ chooses $\beta$ on such paths. For the remaining paths in $\langle{\hat{\pi}_{\alpha}}\rangle$, action $\alpha$ is chosen with probability one. The expected reward in $\mathcal{M}$ along $\hat{\pi}_{\alpha}$ is:

[TABLE]

The expected reward in ${\mathcal{M}_{\mathcal{D}}}$ along $\hat{\pi}_{\alpha}$ differs as

[TABLE]

The intuition is as follows: If path $s_{0}\xrightarrow{t}s_{3}\xrightarrow{\alpha}s_{6}$ of $\mathcal{M}$ under $\sigma$ occurs, we have $t\leq 1$ since $\sigma$ chose $\alpha$. Hence, the reward collected from paths in $\langle{\hat{\pi}_{\alpha}}\rangle$ is at most $1\cdot\rho(s_{0})=1$. There is thus a dependency between the choice of the scheduler at $s_{3}$ and the collected reward at $s_{0}$. This dependency is absent in ${\mathcal{M}_{\mathcal{D}}}$ as the reward at a state is independent of the subsequent performed actions.

Let $\hat{\pi}_{\beta}=s_{0}\xrightarrow{\bot}s_{3}\xrightarrow{\beta}s_{4}$. The expected reward along $\hat{\pi}_{\beta}$ is $2e^{-1}$ for $\mathcal{M}$ and $e^{-1}$ for ${\mathcal{M}_{\mathcal{D}}}$. As the rewards for $\hat{\pi}_{\alpha}$ and $\hat{\pi}_{\beta}$ sum up to one in both $\mathcal{M}$ and ${\mathcal{M}_{\mathcal{D}}}$, the expected reward along all paths of length two coincides for $\mathcal{M}$ and ${\mathcal{M}_{\mathcal{D}}}$.

This observation can be generalized to arbitrary MA and paths of arbitrary length.

Proof of Proposition 3 (sketch).

For every $n\geq 0$, the expected reward collected along paths of length at most $n$ coincides for $\mathcal{M}$ under $\sigma$ and ${\mathcal{M}_{\mathcal{D}}}$ under ${\mathrm{ta}(\sigma)}$. The proposition follows by letting $n$ approach infinity.

Thus, queries on MA with mixtures of untimed reachability and expected reward objectives can be analyzed on the underlying MDP ${\mathcal{M}_{\mathcal{D}}}$.

4.3 Timed Reachability Objectives

Timed reachability objectives cannot be analyzed on ${\mathcal{M}_{\mathcal{D}}}$ as it abstracts away from sojourn times. We lift the digitization approach for single-objective timed reachability [8, 9] to multiple objectives. Instead of abstracting timing information, it is digitized. Let ${\mathcal{M}_{\delta}}$ denote the digitization of $\mathcal{M}$ for arbitrary digitization constant $\delta\in\mathbb{R}_{>0}$, see Def. 4. A time interval $I\subseteq\mathbb{R}_{\geq 0}$ of the form $[a,\infty)$ or $[a,b]$ with $\mathrm{di}_{a}\coloneqq\nicefrac{{a}}{{\delta}}\in\mathbb{N}$ and $\mathrm{di}_{b}\coloneqq\nicefrac{{b}}{{\delta}}\in\mathbb{N}$ is called well-formed. For the remainder, we only consider well-formed intervals, ensured by an appropriate digitization constant. An interval for time-bounds $I$ is transformed to digitization step bounds ${\mathrm{di}(I)}\subseteq\mathbb{N}$. Let $a=\inf I$, we set ${\mathrm{di}(I)}=\{\nicefrac{{t}}{{\delta}}\in\mathbb{N}\mid t\in I\}\setminus\{0\mid a>0\}$.

We first relate paths in $\mathcal{M}$ to paths in its digitization.

Definition 12 (Digitization of a path)

The digitization ${\mathrm{di}(\pi)}$ of path $\pi=s_{0}\xrightarrow{\kappa_{0}}s_{1}\xrightarrow{\kappa_{1}}\dots$ in $\mathcal{M}$ is the path in ${\mathcal{M}_{\delta}}$ given by

[TABLE]

where ${m_{i}}=\max\{{m}\in\mathbb{N}\mid{m}\delta\leq t(\kappa_{i})\}$ for each $i\geq 0$.

Example 7

For the path $\pi=s_{0}\xrightarrow{1.1}s_{3}\xrightarrow{\beta}s_{4}\xrightarrow{\eta}s_{5}\xrightarrow{0.3}s_{4}$ of the MA $\mathcal{M}$ in Fig. 2(a) and $\delta=0.4$, we get ${\mathrm{di}(\pi)}=s_{0}\xrightarrow{\bot}s_{0}\xrightarrow{\bot}s_{0}\xrightarrow{\bot}s_{3}\xrightarrow{\beta}s_{4}\xrightarrow{\eta}s_{5}\xrightarrow{\bot}s_{4}$.

The ${m_{i}}$ in the definition above represent a digitization of the sojourn times $t(\kappa_{i})$ such that ${m_{i}}\delta\leq t(\kappa_{i})<({m_{i}}{+}1)\delta$. These digitized times are incorporated into the digitization of a path by taking the self-loop at state $s_{i}\in\mathrm{MS}$ ${m_{i}}$ times. We also refer to the paths of ${\mathcal{M}_{\delta}}$ as digital paths (of $\mathcal{M}$). The number ${\lvert\bar{\pi}\rvert_{\mathrm{ds}}}$ of digitization steps of a digital path $\bar{\pi}$ is the number of transitions emerging from Markovian states, i.e., ${\lvert\bar{\pi}\rvert_{\mathrm{ds}}}=\lvert\{i<\lvert\bar{\pi}\rvert\mid{\bar{\pi}[i]}\in\mathrm{MS}\}\rvert$. One digitization step represents the elapse of at most $\delta$ time units—either by staying at some $s\in\mathrm{MS}$ for $\delta$ time or by leaving $s$ within $\delta$ time. The number ${\lvert{\mathrm{di}(\pi)}\rvert_{\mathrm{ds}}}$ multiplied with $\delta$ yields an estimate for the duration $\mathit{T}(\pi)$. A digital path $\bar{\pi}$ can be interpreted as representation of the set of paths of $\mathcal{M}$ whose digitization is $\bar{\pi}$.

Definition 13 (Induced paths of a digital path)

The set of induced paths of a (finite or infinite) digital path $\bar{\pi}$ of ${\mathcal{M}_{\delta}}$ is

[TABLE]

For sets of digital paths $\Pi$ we define the induced paths $[{\Pi}]=\bigcup_{\bar{\pi}\in\Pi}[{\bar{\pi}}]$. To relate timed reachability probabilities for $\mathcal{M}$ under scheduler $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ with $\mathrm{ds}$-bounded reachability probabilities for ${\mathcal{M}_{\delta}}$, relating $\sigma$ to a scheduler for ${\mathcal{M}_{\delta}}$ is necessary.

Definition 14 (Digitization of a scheduler)

The * digitization* of $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ is given by ${\mathrm{di}(\sigma)}\in{\mathrm{TA}^{{\mathcal{M}_{\delta}}}}$ such that for any $\bar{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$ with $\mathit{last}(\bar{\pi})\in\mathrm{PS}$

[TABLE]

The digitization ${\mathrm{di}(\sigma)}$ is similar to the time-abstraction ${\mathrm{ta}(\sigma)}$ as both schedulers get a path with restricted timing information as input and mimic the choice of $\sigma$. However, while ${\mathrm{ta}(\sigma)}$ receives no information regarding sojourn times, ${\mathrm{di}(\sigma)}$ receives the digital estimate. Intuitively, ${\mathrm{di}(\sigma)}(\bar{\pi},\alpha)$ considers $\sigma(\pi,\alpha)$ for each $\pi\in[{\bar{\pi}}]$, weighted with the probability that the sojourn times of a path in $[{\bar{\pi}}]$ are as given by $\pi$. The restriction $\mathit{last}(\bar{\pi})\in\mathrm{PS}$ asserts that $\bar{\pi}$ does not end with a self-loop on a Markovian state, implying $[{\bar{\pi}}]\neq\emptyset$.

Example 8

Let MA $\mathcal{M}$ in Fig. 2(a) and $\delta=0.4$. Again, $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ chooses $\alpha$ at state $s_{3}$ iff the sojourn time at $s_{0}$ is at most one. Consider the digital paths $\bar{\pi}_{m}=(s_{0}\xrightarrow{\bot}\!)^{m}s_{0}\xrightarrow{\bot}s_{3}$. For $\pi\in[{\bar{\pi}_{1}}]=\{s_{0}\xrightarrow{t}s_{3}\mid 0.4\leq t<0.8\}$ we have $\sigma(\pi,\alpha)=1$. It follows ${\mathrm{di}(\sigma)}(\pi_{1},\alpha)=1$. For $\pi\in[{\bar{\pi}_{2}}]=\{s_{0}\xrightarrow{t}s_{3}\mid 0.8\leq t<1.2\}$ it is unclear whether $\sigma$ chooses $\alpha$ or $\beta$. Hence, ${\mathrm{di}(\sigma)}$ randomly guesses:

[TABLE]

On ${\mathcal{M}_{\delta}}$ we consider $\mathrm{ds}$-bounded reachability instead of timed reachability.

Definition 15 ($\mathrm{ds}$-bounded reachability)

The set of infinite digital paths that reach $G\subseteq S$ within the interval $J\subseteq\mathbb{N}$ of consecutive natural numbers is

[TABLE]

The timed reachability probabilities for $\mathcal{M}$ are estimated by $\mathrm{ds}$-bounded reachability probabilities for ${\mathcal{M}_{\delta}}$. The induced $\mathrm{ds}$-bounded reachability probability for $\mathcal{M}$ (under $\sigma$) coincides with $\mathrm{ds}$-bounded reachability probability on ${\mathcal{M}_{\delta}}$ (under ${\mathrm{di}(\sigma)}$).

Proposition 4 ()

Let $\mathcal{M}$ be an MA with $G\subseteq S$, $\sigma\in{\mathrm{GM}}$, and digitization ${\mathcal{M}_{\delta}}$. Further, let $J\subseteq\mathbb{N}$ be a set of consecutive natural numbers. It holds that

[TABLE]

Thus, induced $\mathrm{ds}$-bounded reachability on MAs can be computed on their digitization. Next, we relate $\mathrm{ds}$-bounded and timed reachability on MAs, i.e., we quantify the maximum difference between time-bounded and $\mathrm{ds}$-bounded reachability probabilities.

Example 9

Let $\mathcal{M}$ be the MA given in Fig. 4(a). We consider the well-formed time interval $I=[0,5\delta]$, yielding digitization step bounds ${\mathrm{di}(I)}=\{0,\dots,5\}$. The digitization constant $\delta\in\mathbb{R}_{>0}$ remains unspecified in this example. Fig. 4(b) illustrates paths $\pi_{1}$, $\pi_{2}$, and $\pi_{3}$ of $\mathcal{M}$. We depict sojourn times by arrow length. A black dot indicates that the path stays at the current state for a multiple of $\delta$ time units. All depicted paths reach $G=\{s_{3}\}$ within $5\delta$ time units. However, the digitizations of $\pi_{1}$, $\pi_{2}$, and $\pi_{3}$ reach $G$ within $5$, $4$, and $6$ digitization steps, respectively. This yields

[TABLE]

Let $\lambda=\max\{{\mathrm{E}(s)}\mid s\in\mathrm{MS}\}$ be the maximum exit rate of $\mathcal{M}$. For $a\neq 0$ define

[TABLE]

$\varepsilon^{\downarrow}(I)$ and $\varepsilon^{\uparrow}(I)$ approach [math] for small digitization constants $\delta\in\mathbb{R}_{>0}$.

Proposition 5 ()

For MA $\mathcal{M}$, scheduler $\sigma\in{\mathrm{GM}}$, goal states $G\subseteq S$, digitization constant $\delta\in\mathbb{R}_{>0}$ and time interval $I$

[TABLE]

Proof (sketch).

The sets $\lozenge^{I}G$ and $[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$ are illustrated in Fig. 5. We have

[TABLE]

One then shows

[TABLE]

To this end, show for any $k\in\mathbb{N}$ that $1-(1+\lambda\delta)^{k}\cdot e^{-\lambda\delta k}$ is an upper bound for the probability of paths that induce more then $k$ digitization steps within the the first $k\delta$ time units. Then, this probability can be related to the probability of paths in $\lozenge^{I}G\setminus[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$ and $[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\setminus\lozenge^{I}G$, respectively.

From Prop. 4 and Prop. 5, we immediately have Cor. 1, which ensures that the value $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge^{I}G)$ can be approximated with arbitrary precision by computing $\mathrm{Pr}^{{\mathcal{M}_{\delta}}}_{{\mathrm{di}(\sigma)}}(\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G)$ for a sufficiently small $\delta$.

Corollary 1 ()

For MA $\mathcal{M}$, scheduler $\sigma\in{\mathrm{GM}}$, goal states $G\subseteq S$, digitization constant $\delta\in\mathbb{R}_{>0}$ and time interval $I$

[TABLE]

This generalizes existing results [8, 9] that only consider schedulers which maximize (or minimize) the corresponding probabilities. More details are given in App. 0.F.

Next, we lift Cor. 1 to multiple objectives ${\mathbb{O}}=({\mathbb{O}_{1}},\dots,{\mathbb{O}_{d}})$. We define the satisfaction of a timed reachability objective ${\mathbb{P}({\lozenge^{I}{G}})}$ for the digitization ${\mathcal{M}_{\delta}}$ as ${\mathcal{M}_{\delta}},\sigma\models{\mathbb{P}({\lozenge^{I}{G}})}\vartriangleright_{i}p_{i}\text{ iff }\mathrm{Pr}^{{\mathcal{M}_{\delta}}}_{\sigma}(\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G)\vartriangleright_{i}p_{i}$. This allows us to consider notations like $\mathit{achieve}^{{\mathcal{M}_{\delta}}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$, where ${\mathbb{O}}$ contains one or more timed reachability objectives. For a point ${\mathbf{p}}=(p_{1},\dots,p_{d})\in\mathbb{R}^{d}$ we consider the hyperrectangle

[TABLE]

and $\varepsilon^{\downarrow}_{i}$ is defined similarly. The next example shows how the set of achievable points of $\mathcal{M}$ can be approximated using achievable points of ${\mathcal{M}_{\delta}}$.

Example 10

Let ${\mathbb{O}}=({\mathbb{P}({\lozenge^{I_{1}}{G_{1}}})},{\mathbb{P}({\lozenge^{I_{2}}{G_{2}}})})$ be two timed reachability objectives for an MA $\mathcal{M}$ with digitization ${\mathcal{M}_{\delta}}$ such that $\varepsilon^{\downarrow}_{1}=0.13$, $\varepsilon^{\uparrow}_{1}=0.22$, $\varepsilon^{\downarrow}_{2}=0.07$, and $\varepsilon^{\uparrow}_{2}=0.15$. The blue rectangle in Fig. 6(a) illustrates the set $\varepsilon({\mathbb{O}},{\mathbf{p}})$ for the point ${\mathbf{p}}=(0.4,0.3)$. Assume $\mathit{achieve}^{{\mathcal{M}_{\delta}}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$ holds for threshold relations ${\vartriangleright}=\{\geq,\geq\}$, i.e., ${\mathbf{p}}$ is achievable for the digitization ${\mathcal{M}_{\delta}}$. From Cor. 1, we infer that $\varepsilon({\mathbb{O}},{\mathbf{p}})$ contains at least one point ${\mathbf{p}}^{\prime}$ that is achievable for $\mathcal{M}$. Hence, the bottom left corner point of the rectangle is achievable for $\mathcal{M}$. This holds for any rectangle $\varepsilon({\mathbb{O}},{\mathbf{q}})$ with ${\mathbf{q}}\in A$, where $A$ is the set of achievable points of ${\mathcal{M}_{\delta}}$ denoted by the gray area111In the figure, $A^{-}$ partly overlaps $A$, i.e., the green area also belongs to $A$. in Fig. 6(b). It follows that any point in $A^{-}$ (depicted by the green area) is achievable for $\mathcal{M}$. On the other hand, an achievable point of $\mathcal{M}$ has to be contained in a set $\varepsilon({\mathbb{O}},{\mathbf{q}})$ for at least one ${\mathbf{q}}\in A$. The red area depicts the points $\mathbb{R}^{d}\setminus A^{+}$ for which this is not the case, i.e., points that are not achievable for $\mathcal{M}$. The digitization constant $\delta$ controls the accuracy of the resulting approximation. Fig. 6(c) depicts a possible result when a smaller digitization constant $\tilde{\delta}<\delta$ is considered.

The observations from the example above are formalized in the following theorem. The theorem also covers unbounded reachability objectives by considering the time interval $I=[0,\infty)$. For expected reward objectives of the form ${\mathbb{E}({\#j,G})}$ it can be shown that $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho_{j},G)=\mathrm{ER}^{{\mathcal{M}_{\delta}}}_{{\mathrm{di}(\sigma)}}(\rho_{j}^{\delta},G)$. This claim is similar to Proposition 3 and can be shown analogously. This enables multi-objective model checking of MAs with timed reachability objectives.

Theorem 4.3 ()

Let $\mathcal{M}$ be an MA with digitization ${\mathcal{M}_{\delta}}$. Furthermore, let ${\mathbb{O}}$ be (un)timed reachability or expected reward objectives with threshold relations ${\vartriangleright}$ and $|{\mathbb{O}}|=d$. It holds that $A^{-}\subseteq\{{\mathbf{p}}\in\mathbb{R}^{d}\mid\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\}\subseteq A^{+}$ with:

[TABLE]

5 Experimental Evaluation

Implementation.

We implemented multi-objective model checking of MAs into Storm [31]. The input model is given in the PRISM language222We slightly extend the PRISM language in order to describe MAs. and translated into a sparse representation. For MA $\mathcal{M}$, the implementation performs a multi-objective analysis on the underlying MDP ${\mathcal{M}_{\mathcal{D}}}$ or a digitization ${\mathcal{M}_{\delta}}$ and infers (an approximation of) the achievable points of $\mathcal{M}$ by exploiting the results from Sect. 4. For computing the achievable points of ${\mathcal{M}_{\mathcal{D}}}$ and ${\mathcal{M}_{\delta}}$, we apply the approach of [15]. It repeatedly checks weighted combinations of the objectives (by means of value iteration [29] – a standard technique in single-objective MDP model checking) to refine an approximation of the set of achievable points. This procedure is extended as follows. Full details can be found in [32].

• •

We support $\mathrm{ds}$-bounded reachability objectives by combining the approach of [15] (which supports step-bounded reachability on MDPs) with techniques from single-objective MA analysis [8]. Roughly, we reduce $\mathrm{ds}$-bounded reachability to untimed reachability by storing the digitized time-epoch (i.e., the current number of digitization steps) into the state space. A blow-up of the resulting model is avoided by considering each time-epoch separately.

• •

In contrast to [15], we allow a simultaneous analysis of minimizing and maximizing expected reward objectives. This is achieved by performing additional preprocessing steps that comprise an analysis of end components.

The source code including all material to reproduce the experiments is available at http://www.stormchecker.org/benchmarks.html.

Setup.

Our implementation uses a single core (2GHz) of a 48-core HP BL685C G7 limited to 20GB RAM. The timeout (TO) is two hours. For a model, a set of objectives, and a precision $\eta\in\mathbb{R}_{>0}$, we measure the time to compute an $\eta$-approximation333An $\eta$-approximation of $A\subseteq\mathbb{R}^{d}$ is given by $A^{-},A^{+}\subseteq\mathbb{R}^{d}$ with $A^{-}\subseteq A\subseteq A^{+}$ and for all ${\mathbf{p}}\in A^{+}$ exists a ${\mathbf{q}}\in A^{-}$ such that the distance between ${\mathbf{p}}$ and ${\mathbf{q}}$ is at most $\eta$. of the set of achievable points. This set-up coincides with Pareto queries as discussed in [15]. The digitization constant $\delta$ is chosen heuristically such that recalculations with smaller constants $\tilde{\delta}<\delta$ are avoided. We set the precision for value-iteration to $\varepsilon=10^{-6}$. We use classical value iteration; the use of improved algorithms [33] is left for future work.

Results for MAs.

We consider four case studies: (i) a job scheduler [13], see Sect. 1; (ii) a polling system [34, 35] containing a server processing jobs that arrive at two stations; (iii) a video streaming client buffering received packages and deciding when to start playback; and (iv) a randomized mutual exclusion algorithm [35], a variant of [36] with a process-dependent random delay in the critical section. Details on the benchmarks and the objectives are given in App. 0.G.1.

Tab. 1 lists results. For each instance we give the defining constants, the number of states of the MA and the used $\eta$-approximation. A multi-objective query is given by the triple $(l,m,n)$ indicating $l$ untimed, $m$ expected reward, and $n$ timed objectives. For each MA and query we depict the total run-time of our implementation (time) and the number of vertices of the obtained under-approximation (pts).

Queries analyzed on the underlying MDP are solved efficiently on large models with up to millions of states. For timed objectives the run-times increase drastically due to the costly analysis of digitized reachability objectives on the digitization, cf. [9]. Queries with up to four objectives can be dealt with within the time limit. Furthermore, for an approximation one order of magnitude better, the number of vertices of the result increases approximately by a factor three. In addition, a lower digitization constant has then to be considered which often leads to timeouts in experiments with timed objectives.

Comparison with PRISM [14] and IMCA [9].

We compared the performance of our implementation with both PRISM and IMCA. Verification times are summarized in Fig. 7: On points above the diagonal, our implementation is faster. For the comparison with PRISM (no MAs), we considered the multi-objective MDP benchmarks from [15, 18]. Both implementations are based on [15]. For the comparison with IMCA (no multi-objective queries) we used the benchmarks from Tab. 1, with just a single objective. We observe that our implementation is competitive. Details are given in App. 0.G.2 and App. 0.G.3.

6 Conclusion

We considered multi-objective verification of Markov automata, including in particular timed reachability objectives. The next step is to apply our algorithms to the manifold applications of MA, such as generalized stochastic Petri nets to enrich the analysis possibilities of such nets.

6.0.1 Acknowledgement.

This work was supported by the CDZ project CAP (GZ 1023).

Appendix 0.A Additional Preliminaries

0.A.1 Models with Rewards

We extend the models with rewards.

Definition 16 (Markov decision process [29])

A Markov decision process (MDP) is a tuple $\mathcal{D}=(S,\mathit{Act},\mathbf{P},{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$, where $S,{s_{0}},\mathit{Act},\ell$ are as in Definition 1, $\rho_{1},\dots,\rho_{\ell}$ are action reward functions $\rho_{i}\colon S\times\mathit{Act}\to\mathbb{R}_{\geq 0}$, and $\mathbf{P}\colon S\times\mathit{Act}\times S\to[0,1]$ is a transition probability function satisfying $\sum_{s^{\prime}\in S}\mathbf{P}(s,\alpha,s^{\prime})\in\{0,1\}$ for all $s\in S$ and $\alpha\in\mathit{Act}$.

The reward $\rho(s,\alpha)$ is collected when choosing action $\alpha$ at state $s$. Note that we do not consider state rewards for MDPs.

Definition 17 (Underlying MDP)

For MA $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ with transition probabilities $\mathbf{P}$ the underlying MDP of $\mathcal{M}$ is given by ${\mathcal{M}_{\mathcal{D}}}=(S,\mathit{Act},\mathbf{P},{s_{0}},\{\rho_{1}^{\mathcal{D}},\dots,\rho_{\ell}^{\mathcal{D}}\})$, where for each $i\in\{1,\dots,\ell\}$

[TABLE]

The reward functions $\rho_{1}^{\mathcal{D}},\dots,\rho_{\ell}^{\mathcal{D}}$ incorporate the action and state rewards of $\mathcal{M}$ where the state rewards are multiplied with the expected sojourn times $\nicefrac{{1}}{{{\mathrm{E}(s)}}}$ of states $s\in\mathrm{MS}$.

Definition 18 (Digitization of an MA)

For an MA $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\allowbreak\dots,\rho_{\ell}\})$ with transition probabilities $\mathbf{P}$ and a digitization constant $\delta\in\mathbb{R}_{>0}$, the digitization of $\mathcal{M}$ w.r.t. $\delta$ is given by the MDP ${\mathcal{M}_{\delta}}=(S,\mathit{Act},\mathbf{P}_{\delta},{s_{0}},\{\rho_{1}^{\delta},\dots,\rho_{\ell}^{\delta}\})$, where $\mathbf{P}_{\delta}$ is as in Definition 4 and for each $i\in\{1,\dots,\ell\}$

[TABLE]

0.A.2 Measures

0.A.2.1 Probability measure.

Given a scheduler $\sigma\in{\mathrm{GM}}$, the probability measure $\mathrm{Pr}^{\mathcal{M}}_{\sigma}$ is defined for measurable sets of infinite paths of MA $\mathcal{M}$. This is achieved by considering the probability measure $\mathrm{Pr}^{\mathit{Steps}}_{\sigma,\pi}$ for transition steps. For a history $\pi\in{\mathit{FPaths}}$ with $s=\mathit{last}(\pi)$ and a measurable set of transition steps $T\subseteq\mathbb{R}_{\geq 0}\times\mathit{Act}\times S$ we have

[TABLE]

$\mathrm{Pr}^{\mathcal{M}}_{\sigma}$ is obtained by lifting $\mathrm{Pr}^{\mathit{Steps}}_{\sigma,\pi}$ to sequences of transition steps (i.e., paths). More information can be found in [37, 8]. To simplify the notations, we write $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\pi)$ instead of $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\{\pi\})$. For a set of finite paths $\Pi\subseteq{\mathit{FPaths}^{\mathcal{M}}}$ we set $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\Pi)$ = $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\mathit{Cyl}(\Pi))$, where $\mathit{Cyl}(\Pi)$ is the Cylinder of $\Pi$ given by

[TABLE]

0.A.2.2 Expected reward.

We fix a reward function $\rho$ of the MA $\mathcal{M}$. The reward of a finite path $\pi^{\prime}=s_{0}\xrightarrow{\kappa_{0}}\dots\xrightarrow{\kappa_{n-1}}s_{n}\in{\mathit{FPaths}}$ is given by

[TABLE]

Intuitively, $\mathit{rew}^{\mathcal{M}}(\pi^{\prime})$ is the sum over the rewards obtained in every step $s_{i}\xrightarrow{\kappa_{i}}$ depicted in the path $\pi^{\prime}$. The reward obtained in step $i$ is composed of the state reward of $s_{i}$ multiplied with the sojourn time $t(\kappa_{i})$ as well as the action reward given by $s_{i}$ and $\alpha(\kappa_{i})$. State rewards assigned to probabilistic states do not affect the reward of a path as the sojourn time in such states is zero.

For an infinite path $\pi=s_{0}\xrightarrow{\kappa_{0}}s_{1}\xrightarrow{\kappa_{1}}\dots\in{\mathit{IPaths}}$, the reward of $\pi$ up to a set of goal states $G\subseteq S$ is given by

[TABLE]

Intuitively, we stop collecting reward as soon as $\pi$ reaches a state in $G$. If no state in $G$ is reached, reward is accumulated along the infinite path, which potentially yields an infinite reward. The expected reward $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,G)$ is the expected value of the function $\mathit{rew}^{\mathcal{M}}(\rho,\cdot,G)\colon{\mathit{IPaths}^{\mathcal{M}}}\to\mathbb{R}_{\geq 0}$, i.e.,

[TABLE]

Appendix 0.B Proofs About Sets of Achievable Points

0.B.1 Proof of Theorem 3.1

See 3.1

Proof

Consider the MA $\mathcal{M}$ in Fig. 3(a) with objectives ${\mathbb{O}}=({\mathbb{P}({\lozenge\{s_{2}\}})},{\mathbb{P}({\lozenge\{s_{4}\}})})$, relations ${\vartriangleright}=(\geq,\geq)$, and point ${\mathbf{p}}=(0.5,0.5)$. We have $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$ (A scheduler achieving both objectives is given in Example 4). However, there are only two deterministic time abstract schedulers for $\mathcal{M}$:

[TABLE]

and it holds that $\mathcal{M},\sigma_{\alpha}\not\models{\mathbb{P}({\lozenge\{s_{4}\}})}\geq 0.5$ and $\mathcal{M},\sigma_{\beta}\not\models{\mathbb{P}({\lozenge\{s_{2}\}})}\geq 0.5$. ∎

0.B.2 Proof of Proposition 1

See 1

Proof

Let $\mathcal{M}$ be an MA and let ${\mathbb{O}}=({\mathbb{O}_{1}},\dots,{\mathbb{O}_{d}})$ be objectives with relations ${\vartriangleright}=(\vartriangleright_{1},\dots,\vartriangleright_{d})$ and points ${\mathbf{p}}_{1},{\mathbf{p}}_{2}\in\mathbb{R}^{d}$ such that $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}}_{1})$ and $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}}_{2})$ holds. For $i\in{1,2}$, let $\sigma_{i}\in{\mathrm{GM}}$ be a scheduler satisfying $\mathcal{M},\sigma_{i}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}_{i}$. Consider some $w\in[0,1]$. The point ${\mathbf{p}}=w\cdot{\mathbf{p}}_{1}+(1-w)\cdot{\mathbf{p}}_{2}$ is achievable with the scheduler that makes an initial one-off random choice:

• •

with probability $w$ mimic $\sigma_{1}$ and

• •

with probability $1-w$ mimic $\sigma_{2}$.

Hence, $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$, implying that the set of achievable points is convex. ∎

0.B.3 Proof of Theorem 3.2

See 3.2

Proof

We show that the claim holds for the MA $\mathcal{M}$ in Fig. 3(a) with objectives ${\mathbb{O}}=({\mathbb{P}({\lozenge\{s_{2}\}})},{\mathbb{P}({\lozenge^{[0,2]}{\{s_{4}\}}})})$ and relations ${\vartriangleright}=(\geq,\geq)$.

For the sake of contradiction assume that the polytope $A=\{{\mathbf{p}}\in\mathbb{R}^{2}\mid\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})\}$ is finite. Then, there must be two distinct vertices ${\mathbf{p}}_{1},{\mathbf{p}}_{2}$ of $A$ such that $\{w\cdot{\mathbf{p}}_{1}+(1-w)\cdot{\mathbf{p}}_{2}\mid w\in[0,1]\}$ is a face of $A$. In particular, this means that ${\mathbf{p}}=0.5\cdot{\mathbf{p}}_{1}+0.5\cdot{\mathbf{p}}_{2}$ is achievable but ${\mathbf{p}}_{\varepsilon}={\mathbf{p}}+(0,\varepsilon)$ is not achievable for all $\varepsilon>0$. We show that there is in fact an $\varepsilon$ for which ${\mathbf{p}}_{\varepsilon}$ is achievable, contradicting our assumption that $A$ is finite.

For $i\in{1,2}$, let $\sigma_{i}\in{\mathrm{GM}}$ be a scheduler satisfying $\mathcal{M},\sigma_{i}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}_{i}$. $\sigma_{1}\neq\sigma_{2}$ has to hold as the schedulers achieve different vertices of $A$. The point ${\mathbf{p}}$ is achievable with the randomized scheduler $\sigma$ that mimics $\sigma_{1}$ with probability 0.5 and mimics $\sigma_{2}$ otherwise. Consider $t=-\log(\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge\{s_{2}\}))$ and the deterministic scheduler $\sigma^{\prime}$ given by

[TABLE]

$\sigma^{\prime}$ satisfies $\mathrm{Pr}^{\mathcal{M}}_{\sigma^{\prime}}(\lozenge\{s_{2}\})=e^{-t}=\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge\{s_{2}\})$. Moreover, we have

[TABLE]

where the last inequality is due to $\sigma\neq\sigma^{\prime}$. While the probability to reach $s_{3}$ is equal under both schedulers, $s_{3}$ is reached earlier when $\sigma^{\prime}$ is considered. This increases the probability to reach $s_{4}$ in time, i.e., $\mathrm{Pr}^{\mathcal{M}}_{\sigma^{\prime}}(\lozenge^{[0,2]}\{s_{4}\})>\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge^{[0,2]}\{s_{4}\})$. It follows that $\mathcal{M},\sigma^{\prime}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}_{\varepsilon}$ for some $\varepsilon>0$. ∎

Appendix 0.C Proofs for Untimed Reachability

0.C.1 Proof of Lemma 1

See 1

Proof

The proof is by induction over the length of the considered path $\lvert\hat{\pi}\rvert=n$. Let $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ and ${\mathcal{M}_{\mathcal{D}}}=(S,\mathit{Act},\mathbf{P},{s_{0}},\{\rho_{1}^{\mathcal{D}},\dots,\rho_{\ell}^{\mathcal{D}}\})$. If $n=0$, then $\{\hat{\pi}\}=\langle{\hat{\pi}}\rangle=\{{s_{0}}\}$. Hence, $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\langle{\hat{\pi}}\rangle)=1=\mathrm{Pr}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\hat{\pi})$. In the induction step, we assume that the lemma holds for a fixed path $\hat{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\mathcal{D}}}}}$ with length $\lvert\hat{\pi}\rvert=n$ and $\mathit{last}(\hat{\pi})=s$. Consider the path $\hat{\pi}\xrightarrow{\alpha}s^{\prime}\in{\mathit{FPaths}^{{\mathcal{M}_{\mathcal{D}}}}}$.

Case $s\in\mathrm{PS}$:

It follows that

[TABLE]

Case $s\in\mathrm{MS}$:

As $s\in\mathrm{MS}$ we have $\alpha=\bot$ and it follows

[TABLE]

∎

0.C.2 Proof of Proposition 2

See 2

Proof

Let $\Pi$ be the set of finite time-abstract paths of ${\mathcal{M}_{\mathcal{D}}}$ that end at the first visit of a state in $G$, i.e.,

[TABLE]

Every path $\pi\in\lozenge G\subseteq{\mathit{IPaths}^{\mathcal{M}}}$ has a unique prefix $\pi^{\prime}$ with $\mathrm{ta}(\pi^{\prime})\in\Pi$. We have

[TABLE]

The claim follows with Lemma 1 since

[TABLE]

∎

0.C.3 Proof of Theorem 4.1

See 4.1

Proof

Let ${\mathbb{O}}=({\mathbb{P}({\lozenge G_{1}})},\dots,{\mathbb{P}({\lozenge G_{d}})})$ be the considered list of objectives with threshold relations ${\vartriangleright}=(\vartriangleright_{1},\dots,\vartriangleright_{d})$. The following equivalences hold for any $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ and ${\mathbf{p}}\in\mathbb{R}^{d}$.

[TABLE]

Assume that $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$ holds, i.e., there is a $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ such that $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$. It follows that ${\mathcal{M}_{\mathcal{D}}},{\mathrm{ta}(\sigma)}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$ which means that $\mathit{achieve}^{{\mathcal{M}_{\mathcal{D}}}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$ holds as well. For the other direction assume $\mathit{achieve}^{{\mathcal{M}_{\mathcal{D}}}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$, i.e., ${\mathcal{M}_{\mathcal{D}}},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$ for some time-abstract scheduler $\sigma\in{\mathrm{TA}}$. We have ${\mathrm{ta}(\sigma)}=\sigma$. It follows that ${\mathcal{M}_{\mathcal{D}}},{\mathrm{ta}(\sigma)}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$. Applying the equivalences above yields $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$ and thus $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}})$. ∎

Appendix 0.D Proofs for Expected Reward

0.D.1 Proof of Proposition 3

Let $n\geq 0$ and $G\subseteq S$. The set of time-abstract paths that end after $n$ steps or at the first visit of a state in $G$ is denoted by

[TABLE]

For $\mathcal{M}$ under $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ and ${\mathcal{M}_{\mathcal{D}}}$ under ${\mathrm{ta}(\sigma)}\in{\mathrm{TA}}$, we define the expected reward collected along the paths of ${\Pi_{G}^{n}}$ as

[TABLE]

respectively. Intuitively, $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,{\Pi_{G}^{n}})$ corresponds to $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,G)$ assuming that no more reward is collected after the $n$-th transition. It follows that the value $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,{\Pi_{G}^{n}})$ approaches $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,G)$ for large $n$. Similarly, $\mathrm{ER}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\rho^{\mathcal{D}},{\Pi_{G}^{n}})$ approaches $\mathrm{ER}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\rho^{\mathcal{D}},G)$ for large $n$. This observation is formalized by the following lemma.

Lemma 2 ()

For MA $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ with $G\subseteq S$, $\sigma\in{\mathrm{GM}}$, and reward function $\rho$ it holds that

[TABLE]

Furthermore, any reward function $\rho^{\mathcal{D}}$ for ${\mathcal{M}_{\mathcal{D}}}$ satisfies

[TABLE]

Proof

We show the first claim. The second claim follows analogously. For each $n\geq 0$, consider the function $f_{n}\colon{\mathit{IPaths}^{\mathcal{M}}}\to\mathbb{R}_{\geq 0}$ given by

[TABLE]

for every path $\pi=s_{0}\xrightarrow{\kappa_{0}}s_{1}\xrightarrow{\kappa_{1}}\dots\in{\mathit{IPaths}^{\mathcal{M}}}$. Intuitively, $f_{n}(\pi)$ is the reward collected on $\pi$ within the first $n$ steps and only up to the first visit of $G$. This allows us to express the expected reward collected along the paths of ${\Pi_{G}^{n}}$ as

[TABLE]

It holds that $\lim_{n\to\infty}f_{n}(\pi)=\mathit{rew}^{\mathcal{M}}(\rho,\pi,G)$ which is a direct consequence from the definition of the reward of $\pi$ up to $G$ (cf. App. 0.A.2.2). Furthermore, note that the sequence of functions $f_{0},f_{1},\dots$ is non-decreasing, i.e., we have $f_{n}(\pi)\leq f_{n+1}(\pi)$ for all $n\geq 0$ and $\pi\in{\mathit{IPaths}^{\mathcal{M}}}$. By applying the monotone convergence theorem [38] we obtain

[TABLE]

∎

The next step is to show that the expected reward collected along the paths of ${\Pi_{G}^{n}}$ coincides for $\mathcal{M}$ under $\sigma$ and ${\mathcal{M}_{\mathcal{D}}}$ under ${\mathrm{ta}(\sigma)}$.

Lemma 3 ()

Let $\rho$ be some reward function of $\mathcal{M}$ and let $\rho^{\mathcal{D}}$ be its counterpart for ${\mathcal{M}_{\mathcal{D}}}$. Let $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ be an MA with $G\subseteq S$ and $\sigma\in{\mathrm{GM}}$. For all $G\subseteq S$ and $n\geq 0$ it holds that

[TABLE]

Proof

The proof is by induction over the path length $n$. To simplify the notation, we often omit the reward functions $\rho$ and $\rho^{\mathcal{D}}$ and write, e.g., $\mathit{rew}^{{\mathcal{M}_{\mathcal{D}}}}(\pi)$ instead of $\mathit{rew}^{{\mathcal{M}_{\mathcal{D}}}}(\rho^{\mathcal{D}}\pi)$ or $\mathrm{ER}^{\mathcal{M}}_{\sigma}({\Pi_{G}^{n}})$ instead of $\mathrm{ER}^{\mathcal{M}}_{\sigma}(\rho,{\Pi_{G}^{n}})$.

If $n=0$, then ${\Pi_{G}^{n}}=\{{s_{0}}\}$. The claim holds since $\mathit{rew}^{\mathcal{M}}({s_{0}})=\mathit{rew}^{{\mathcal{M}_{\mathcal{D}}}}({s_{0}})=0$.

In the induction step, we assume that the lemma is true for some fixed $n\geq 0$. We split the term $\mathrm{ER}^{\mathcal{M}}_{\sigma}({\Pi_{G}^{n+1}})$ into the reward that is obtained by paths which reach $G$ within $n$ steps and the reward obtained by paths of length $n+1$. In a second step, we consider the sum of the reward collected within the first $n$ steps and the reward obtained in the $(n+1)$-th step:

[TABLE]

where we define $\mathit{pref}(\pi,n)$ for paths with $\lvert\pi\rvert\leq n$ such that $\mathit{pref}(\pi,n)=\pi$. The two terms (1) and (2) are treated separately.

Term (1):

Let ${\Lambda^{\leq n}_{G}}=\{\hat{\pi}\in{\Pi_{G}^{n+1}}\mid\lvert\hat{\pi}\rvert\leq n\}$ be the paths in ${\Pi_{G}^{n+1}}$ of length at most $n$. We have ${\Lambda^{\leq n}_{G}}\subseteq{\Pi_{G}^{n}}$ and every path in ${\Lambda^{\leq n}_{G}}$ visits a state in $G$. Correspondingly, ${\Lambda^{=n}_{\neg G}}={\Pi_{G}^{n}}\setminus{\Lambda^{\leq n}_{G}}$ is the set of time-abstract paths of length $n$ that do not visit a state in $G$. Hence, the paths in ${\Pi_{G}^{n+1}}$ with length $n+1$ have a prefix in ${\Lambda^{=n}_{\neg G}}$. The set ${\Pi_{G}^{n+1}}$ is partitioned such that

[TABLE]

The reward obtained within the first $n$ steps is independent of the $(n+1)$-th transition. To show this formally, we fix a path $\hat{\pi}^{\prime}\in{\Lambda^{=n}_{\neg G}}$ with $\mathit{last}(\hat{\pi}^{\prime})=s$ and derive

[TABLE]

With the above-mentioned partition of the set ${\Pi_{G}^{n+1}}$, it follows that the expected reward obtained within the first $n$ steps is given by

[TABLE]

Term (2):

For the expected reward obtained in step $n+1$, consider a path $\hat{\pi}=\hat{\pi}^{\prime}\xrightarrow{\alpha}s^{\prime}\in{\Pi_{G}^{n+1}}$ such that $\lvert\hat{\pi}^{\prime}\rvert=n$ and $\mathit{last}(\hat{\pi}^{\prime})=s$.

• •

If $s\in\mathrm{MS}$, we have $\hat{\pi}=\hat{\pi}^{\prime}\xrightarrow{\bot}s^{\prime}$. It follows that

[TABLE]

• •

If $s\in\mathrm{PS}$, then $\int_{\pi=\pi^{\prime}\xrightarrow{\alpha}s^{\prime}\in\langle{\hat{\pi}}\rangle}\rho(s,\alpha)\,\mathrm{d}\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\pi)=\rho^{\mathcal{D}}(s,\alpha)\cdot\mathrm{Pr}^{{\mathcal{M}_{\mathcal{D}}}}_{{\mathrm{ta}(\sigma)}}(\hat{\pi})$ follows similarly.

Combining the two results yields

[TABLE]

∎

We now show Proposition 3.

See 3

Proof

The proposition is a direct consequence of Lemma 2 and Lemma 3 as

[TABLE]

∎

0.D.2 Proof of Theorem 4.2

See 4.2

Proof

Let ${\mathbb{O}}=({\mathbb{O}_{1}},\dots,{\mathbb{O}_{d}})$ be the considered list of untimed reachability and expected reward objectives with threshold relations ${\vartriangleright}=(\vartriangleright_{1},\dots,\vartriangleright_{d})$. The following equivalences hold for any $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ and ${\mathbf{p}}\in\mathbb{R}^{d}$.

[TABLE]

where for the equivalence marked with $\ast$ we consider two cases: If ${\mathbb{O}_{i}}$ is of the form ${\mathbb{P}({\lozenge G})}$, Proposition 2 yields

[TABLE]

Otherwise, ${\mathbb{O}_{i}}$ is of the form ${\mathbb{E}({\#j,G})}$ and with Proposition 3 it follows that

[TABLE]

The remaining steps of the proof are completely analogous to the proof of Theorem 4.1 conducted on page 0.C.3. ∎

Appendix 0.E Proofs for Timed Reachability

0.E.1 Proof of Proposition 4

Let $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ be an MA and let ${\mathcal{M}_{\delta}}$ be the digitization of $\mathcal{M}$ with respect to some $\delta\in\mathbb{R}_{>0}$. We consider the infinite paths of $\mathcal{M}$ that are represented by a finite digital path.

Definition 19 (Induced cylinder of a digital path)

Given a digital path $\bar{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$ of MA $\mathcal{M}$, the induced cylinder of $\bar{\pi}$ is given by

[TABLE]

Recall the definition of the cylinder of a set of finite paths (cf. App. 0.A.2.1). If $\bar{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$ does not end with a self-loop at a Markovian state, then $[{\bar{\pi}}]_{\mathit{cyl}}=\mathit{Cyl}([{\bar{\pi}}])$ holds.

Example 11

Let $\mathcal{M}$ and ${\mathcal{M}_{\delta}}$ be as in Fig. 2. We consider the path $\bar{\pi}_{1}=s_{0}\xrightarrow{\bot}s_{0}\xrightarrow{\bot}s_{0}\xrightarrow{\bot}s_{3}\xrightarrow{\beta}s_{4}$ and digitization constant $\delta=0.4$. The set $[{\bar{\pi}_{1}}]_{\mathit{cyl}}$ contains each infinite path whose digitization has the prefix $\bar{\pi}_{1}$, i.e.,

[TABLE]

We observe that these are exactly the paths that have a prefix in $[{\bar{\pi}_{1}}]$. Put differently, we have $[{\bar{\pi}_{1}}]_{\mathit{cyl}}=\mathit{Cyl}([{\bar{\pi}_{1}}])$.

Next, consider the digital path $\bar{\pi}_{2}=s_{0}\xrightarrow{\bot}s_{0}\xrightarrow{\bot}s_{0}$. Note that there is no path $\pi\in{\mathit{FPaths}^{\mathcal{M}}}$ with ${\mathrm{di}(\pi)}=\bar{\pi}_{2}$, implying $[{\bar{\pi}_{2}}]=\emptyset$. Intuitively, $\bar{\pi}_{2}$ depicts a sojourn time at $\mathit{last}(\bar{\pi}_{2})$ but finite paths of MAs do not depict sojourn times at their last state. On the other hand, the induced cylinder of $\bar{\pi}_{2}$ contains all paths that sojourn at least $2\delta$ time units at $s_{0}$, i.e.,

[TABLE]

The schedulers $\sigma$ and ${\mathrm{di}(\sigma)}$ induce the same probabilities for a given digital path. This is formalized by the following lemma. Note that a similar statement for ${\mathrm{ta}(\sigma)}$ and time-abstract paths was shown in Lemma 1.

Lemma 4

Let $\mathcal{M}$ be an MA with scheduler $\sigma\in{\mathrm{GM}}$, digitization ${\mathcal{M}_{\delta}}$, and digital path $\bar{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$. It holds that

[TABLE]

Proof

The proof is by induction over the length $n$ of $\bar{\pi}$. Let $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\{\rho_{1},\dots,\rho_{\ell}\})$ and ${\mathcal{M}_{\delta}}=(S,\mathit{Act},\mathbf{P}_{\delta},{s_{0}},\{\rho_{1}^{\delta},\dots,\rho_{\ell}^{\delta}\})$. If $n=0$, then $\bar{\pi}={s_{0}}$ and $[{\bar{\pi}}]_{\mathit{cyl}}={\mathit{IPaths}^{\mathcal{M}}}$. Hence, $\mathrm{Pr}^{\mathcal{M}}_{\sigma}([{{s_{0}}}]_{\mathit{cyl}})=1=\mathrm{Pr}^{{\mathcal{M}_{\delta}}}_{{\mathrm{di}(\sigma)}}({s_{0}})$. In the induction step it is assumed that the lemma holds for a fixed path $\bar{\pi}\in{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$ with $\lvert\bar{\pi}\rvert=n$ and $\mathit{last}(\bar{\pi})=s$. Consider a path $\bar{\pi}\xrightarrow{\alpha}s^{\prime}\in{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$. We distinguish the following cases.

Case $s\in\mathrm{PS}$:

It follows that $[{\bar{\pi}\xrightarrow{\alpha}s^{\prime}}]_{\mathit{cyl}}=\mathit{Cyl}([{\bar{\pi}\xrightarrow{\alpha}s^{\prime}}])$ since $\bar{\pi}\xrightarrow{\alpha}s^{\prime}$ ends with a probabilistic transition. Hence,

[TABLE]

Case $s\in\mathrm{MS}$:

As $s\in\mathrm{MS}$ we have $\alpha=\bot$ and it follows

[TABLE]

Assume that a path $\pi\in[{\bar{\pi}}]_{\mathit{cyl}}$ has been observed, i.e., $\mathit{pref}({\mathrm{di}(\pi)},m)=\bar{\pi}$ holds for some $m\geq 0$. The term $\mathrm{Pr}^{\mathcal{M}}_{\sigma}([{\bar{\pi}\xrightarrow{\bot}s^{\prime}}]_{\mathit{cyl}}\mid[{\bar{\pi}}]_{\mathit{cyl}})$ coincides with the probability that also $\mathit{pref}({\mathrm{di}(\pi)},m+1)=\bar{\pi}\xrightarrow{\bot}s^{\prime}$ holds. We have either

• •

$s\neq s^{\prime}$ which means that the transition from $s$ to $s^{\prime}$ has to be taken during a period of $\delta$ time units or

• •

$s=s^{\prime}$ where we additionally have to consider the case that no transition is taken at $s$ for $\delta$ time units.

It follows that

[TABLE]

We conclude that

[TABLE]

∎

We apply Lemma 4 to show Proposition 4. The idea of the proof is similar to the proof of Proposition 2 conducted on page 0.C.2. See 4

Proof

Consider the set $\Pi_{G}^{J}\subseteq{\mathit{FPaths}^{{\mathcal{M}_{\delta}}}}$ of paths that (i) visit $G$ within $J$ digitization steps and (ii) do not have a proper prefix that satisfies (i). Every path in $\lozenge^{J}_{\mathrm{ds}}G$ has a unique prefix in $\Pi_{G}^{J}$, yielding

[TABLE]

For the corresponding paths of $\mathcal{M}$ we obtain

[TABLE]

The proposition follows with Lemma 4 since

[TABLE]

∎

0.E.2 Proof of Proposition 5

The notation ${\lvert\bar{\pi}\rvert_{\mathrm{ds}}}$ for paths $\bar{\pi}$ of ${\mathcal{M}_{\delta}}$ is also applied to paths of $\mathcal{M}$, where ${\lvert\pi\rvert_{\mathrm{ds}}}={\lvert{\mathrm{di}(\pi)}\rvert_{\mathrm{ds}}}$ for any $\pi\in{\mathit{FPaths}^{\mathcal{M}}}$. Intuitively, one digitization step represents the elapse of at most $\delta$ time units. Consequently, the duration of a path with $k\in\mathbb{N}$ digitization steps is at most $k\delta$.

Lemma 5

For a path $\pi\in{\mathit{FPaths}^{\mathcal{M}}}$ and digitization constant $\delta$ it holds that

[TABLE]

Proof

Let $\pi=s_{0}\xrightarrow{\kappa_{0}}\dots\xrightarrow{\kappa_{n-1}}s_{n}$ and let ${m_{i}}=\max\{{m}\in\mathbb{N}\mid{m}\delta\leq t(\kappa_{i})\}$ for each $i\in\nobreak\{0,\dots,n-1\}$ (as in Definition 12). The number ${\lvert\pi\rvert_{\mathrm{ds}}}$ is given by $\sum_{0\leq i<n,\,s_{i}\in\mathrm{MS}}({m_{i}}+1)$. With $t(\kappa_{i})\leq({m_{i}}+1)\delta$ it follows that

[TABLE]

∎

For a path $\pi$ and $t\in\mathbb{R}_{\geq 0}$, the prefix of $\pi$ up to time point $t$ is given by $\mathit{pref}_{\!\mathit{T}}(\pi,t)=\mathit{pref}(\pi,\max\{n\mid\mathit{T}(\mathit{pref}(\pi,n))\leq t\})$. For the proof of Proposition 5, we focus on the probability that (under a given scheduler $\sigma$) the digitization approach yields an inaccurate estimate of the actual time. This is the probability that more than $k\in\mathbb{N}$ digitization steps have been performed within $k\delta$ time units. We denote this value by $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\#[{k\delta}]^{{>}{k}})$.

Definition 20 (Digitization step bounded paths)

Assume an MA $\mathcal{M}$ and a digitization constant $\delta\in\mathbb{R}_{>0}$. For some $t\in\mathbb{R}_{\geq 0}$, $k\in\mathbb{N}$, and ${\vartriangleright}\in\{<,\leq,>,\geq\}$ the set of paths whose prefix up to time point $t$ has $\vartriangleright j$ digitization steps is defined as

[TABLE]

Example 12

Let $\mathcal{M}$ be the MA given in Fig. 8(a). We consider the set $\#[{5\delta}]^{{\leq}{5}}$. The digitization constant $\delta$ remains unspecified in this example. Fig. 8(b) illustrates paths $\pi_{1}$, $\pi_{2}$, and $\pi_{3}$ of $\mathcal{M}$. We depict sojourn times by arrow length. For instance, the path $\pi_{1}$ corresponds to $s_{0}\xrightarrow{2.5\delta}s_{0}\xrightarrow{1.8\delta}s_{1}\xrightarrow{1.7\delta}\dots\in{\mathit{IPaths}^{\mathcal{M}}}$. Digitization steps that are “earned” by sojourning at some state for a multiple of $\delta$ time units are indicated by black dots. Transitions of $\pi_{i}$ (where $i\in\{1,2,3\}$) that do not belong to $\mathit{pref}_{\!\mathit{T}}(\pi_{i},5\delta)$ are depicted in gray. We obtain

[TABLE]

Note that only the digitization steps of the prefix up to time point $5\delta$ are considered. For example, the step of $\pi_{2}$ at time point $4.5\delta$ is not considered since the corresponding transition is not part of $\mathit{pref}_{\!\mathit{T}}(\pi_{2},5\delta)$. However, we have ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi_{2},5.5\delta)\rvert_{\mathrm{ds}}}=6$, implying $\pi_{2}\notin\#[{5.5\delta}]^{{\leq}{5}}$.

All considered paths reach $G=\{s_{1}\}$ within $5\delta$ time units but $\pi_{3}\in\#[{5\delta}]^{{>}{5}}$ requires more than $5$ digitization steps.

The following lemma gives an upper bound for the probability $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\#[{k\delta}]^{{>}{k}})$.

Lemma 6

Let $\mathcal{M}$ be an MA with $\sigma\in{\mathrm{GM}}$ and maximum rate $\lambda=\max\{{\mathrm{E}(s)}\mid s\in\mathrm{MS}\}$. Further, let $\delta\in\mathbb{R}_{>0}$ and $k\in\mathbb{N}$. It holds that

[TABLE]

For the proof of Lemma 6 we employ the following auxiliary lemma.

Lemma 7

Let $\mathcal{M}$ be an MA with $\sigma\in{\mathrm{GM}}$ and maximum rate $\lambda=\max\{{\mathrm{E}(s)}\mid s\in\mathrm{MS}\}$. For each $\delta\in\mathbb{R}_{>0}$, $k\in\mathbb{N}$, and $t\in\mathbb{R}_{\geq 0}$ it holds that

[TABLE]

Proof

First, we show that the set $\#[{k\delta+t}]^{{\leq}{k}}$ corresponds to the paths of $\#[{k\delta}]^{{\leq}{k}}$ with the additional requirement that no transition is taken between the time points $k\delta$ and $k\delta+t$, i.e.,

[TABLE]

• “$\subseteq$”:

If $\pi\in\#[{k\delta+t}]^{{\leq}{k}}$, then $\pi\in\#[{k\delta}]^{{\leq}{k}}$ follows immediately. Furthermore, assume towards a contradiction that there is a prefix $\pi^{\prime}$ of $\pi$ with $k\delta<\mathit{T}(\pi^{\prime})\leq k\delta+t$. Then, $k<\nicefrac{{\mathit{T}(\pi^{\prime})}}{{\delta}}\leq{\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}$ (cf. Lemma 5). As $\mathit{T}(\pi^{\prime})\leq k\delta+t$, this means that ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi,k\delta+t)\rvert_{\mathrm{ds}}}\geq{\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}>k$ which contradicts $\pi\in\#[{k\delta+t}]^{{\leq}{k}}$.

• “$\supseteq$”:

For $\pi\in\#[{k\delta}]^{{\leq}{k}}$ with no prefix $\pi^{\prime}$ such that $k\delta<\mathit{T}(\pi^{\prime})\leq k\delta+t$, it holds that $\mathit{pref}_{\!\mathit{T}}(\pi,k\delta+t)=\mathit{pref}_{\!\mathit{T}}(\pi,k\delta)$. Hence, ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi,k\delta+t)\rvert_{\mathrm{ds}}}={\lvert\mathit{pref}_{\!\mathit{T}}(\pi,k\delta)\rvert_{\mathrm{ds}}}\leq k$ and it follows that $\pi\in\#[{k\delta+t}]^{{\leq}{k}}$.

The probability for no transition to be taken between $k\delta$ and $k\delta+t$ only depends on the current state at time point $k\delta$. More precisely, for some state $s\in\mathrm{MS}$ assume the set of paths $\{\pi\in\#[{k\delta}]^{{\leq}{k}}\mid\mathit{last}(\mathit{pref}_{\!\mathit{T}}(\pi,k\delta))=s\}$. The probability that a path in this set takes no transition between time points $k\delta$ and $k\delta+t$ is given by $e^{-{\mathrm{E}(s)}t}$. With $\lambda\geq{\mathrm{E}(s)}$ for all $s\in\mathrm{MS}$ it follows that

[TABLE]

∎

Proof (of Lemma 6)

Let $\mathcal{M}=(S,\mathit{Act},\rightarrow,{s_{0}},\emptyset)$. By induction over $k$ we show that

[TABLE]

The claim follows as $\#[{k\delta}]^{{>}{k}}={\mathit{IPaths}^{\mathcal{M}}}\setminus\#[{k\delta}]^{{\leq}{k}}$.

For $k=0$, we have $\pi\in\#[{0\cdot\delta}]^{{\leq}{0}}$ iff $\pi$ takes no Markovian transition at time point zero. As this happens with probability one, it follows that

[TABLE]

We assume in the induction step that the proposition holds for some fixed $k$. We distinguish between two cases for the initial state ${s_{0}}$ of $\mathcal{M}$.

Case ${s_{0}}\in\mathrm{MS}$:

We partition the set \#[{k\delta+\delta}]^{{\leq}{k+1}}=\Lambda^{\geq\delta}\mathbin{\mathchoice{\ooalign{\displaystyle\cup\cr\raise 0.55556pt\hbox{\set@color\displaystyle\cdot}}}{\ooalign{\textstyle\cup\cr\raise 0.55556pt\hbox{\set@color\textstyle\cdot}}}{\ooalign{\scriptstyle\cup\cr\raise 0.38889pt\hbox{\set@color\scriptstyle\cdot}}}{\ooalign{\scriptscriptstyle\cup\cr\raise 0.27779pt\hbox{\set@color\scriptscriptstyle\cdot}}}}\Lambda^{<\delta} with

[TABLE]

Hence, $\Lambda^{\geq\delta}$ contains the paths where we wait at least $\delta$ time units at ${s_{0}}$ and $\Lambda^{<\delta}$ contains the paths where the first transition is taken within $t<\delta$ time units. It follows that $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\#[{k\delta+\delta}]^{{\leq}{k+1}})=\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\Lambda^{\geq\delta})+\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\Lambda^{<\delta})$. We consider the probabilities for $\Lambda^{\geq\delta}$ and $\Lambda^{<\delta}$ separately.

• •

$\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\Lambda^{\geq\delta})$: For a path ${s_{0}}\xrightarrow{t+\delta}s_{1}\xrightarrow{\kappa_{1}}\dots\in\Lambda^{\geq\delta}$, after the first $\delta$ time units there are at most $k$ digitization steps within the next $k\delta$ time units, i.e.,

[TABLE]

The probability for $\Lambda^{\geq\delta}$ can therefore be derived from the probability to wait at ${s_{0}}$ for at least $\delta$ time units and the probability for $\#[{k\delta}]^{{\leq}{k}}$. In order to apply this, we need to modify the considered scheduler as it might depend on the sojourn time in ${s_{0}}$. Let $\sigma_{\delta}$ be the scheduler for $\mathcal{M}$ that mimics $\sigma$ on paths where the first transition is delayed by $\delta$, i.e., $\sigma_{\delta}$ satisfies

[TABLE]

for all ${s_{0}}\xrightarrow{t}\dots\xrightarrow{\kappa_{n-1}}s_{n}\in{\mathit{FPaths}^{\mathcal{M}}}$ and $\alpha\in\mathit{Act}$. It holds that

[TABLE]

• •

$\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\Lambda^{<\delta})$: For a path ${s_{0}}\xrightarrow{t}s_{1}\xrightarrow{\kappa_{1}}\dots\in\Lambda^{<\delta}$, the first digitization step happens at less than $\delta$ time units, i.e., $0\leq t<\delta$. It follows that there are at most $k$ digitization steps in the remaining $k\delta+\delta-t$ time units, i.e.,

[TABLE]

where $\#^{s_{1}}[{k\delta+\delta-t}]^{{\leq}{k}}$ refers to the paths $\#[{k\delta+\delta-t}]^{{\leq}{k}}$ of ${\mathcal{M}^{s_{1}}}=(S,\mathit{Act},\allowbreak\rightarrow,s_{1},\rho_{1},\dots,\rho_{\ell})$, the MA obtained from $\mathcal{M}$ by changing the initial state to $s_{1}$. Hence, the probability for $\Lambda^{<\delta}$ can be derived from the probability to take a transition from ${s_{0}}$ to some state $s$ within $t<\delta$ time units and the probability for $\#^{s}[{k\delta+\delta-t}]^{{\leq}{k}}$. Again, we need to adapt the considered scheduler. Let $\pi\in{\mathit{FPaths}^{\mathcal{M}}}$ with $\mathit{last}(\pi)=s$. The scheduler ${\sigma[{\pi}]}$ for ${\mathcal{M}^{s}}$ mimics the scheduler $\sigma$ for $\mathcal{M}$, where $\pi$ is prepended to the given path, i.e., we set

[TABLE]

for all $s\xrightarrow{\kappa_{j}}\dots\xrightarrow{\kappa_{n-1}}s_{n}\in{\mathit{FPaths}^{{\mathcal{M}^{s}}}}$ and $\alpha\in\mathit{Act}$. With Lemma 7 it follows that

[TABLE]

Combining the results for $\Lambda^{\geq\delta}$ and $\Lambda^{<\delta}$ (i.e., Equations 8 and 9), we obtain

[TABLE]

where the inequality marked with $\ast$ is due to

[TABLE]

Case ${s_{0}}\in\mathrm{PS}$:

Since $\mathcal{M}$ is non-zeno, a state $s\in\mathrm{MS}$ is reached from ${s_{0}}$ within zero time almost surely (i.e., with probability one). From the previous case, it already follows that the Proposition holds for ${\mathcal{M}^{s}}$ with $s\in\mathrm{MS}$ and the set $\#^{s}[{k\delta+\delta}]^{{\leq}{k+1}}$. With $\Pi_{\mathrm{MS}}=\{s_{0}\xrightarrow{\kappa_{0}}\dots\xrightarrow{\kappa_{n-1}}s_{n}\in{\mathit{FPaths}^{\mathcal{M}}}\mid s_{n}\in\mathrm{MS}\text{ and }\forall i<n\colon s_{i}\in\mathrm{PS}\}$ we obtain

[TABLE]

∎ We now present the proof of Proposition 5. See 5

Proof

In Section 4.3 we already discussed that

[TABLE]

The main part of the proof is to show that

[TABLE]

Then, the proposition follows directly. We show Equation 10 for the different forms of the time interval $I$.

Case $I=[0,\infty)$:

In this case we have ${\mathrm{di}(I)}=\mathbb{N}$. It follows that

[TABLE]

Hence,

[TABLE]

Case $I=[0,b]$ for $b=\mathrm{di}_{b}\delta$:

We have ${\mathrm{di}(I)}=\{0,1,\dots,\mathrm{di}_{b}\}$.

• •

We show that $[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\subseteq\lozenge^{I}G$ which implies

[TABLE]

Let $\pi\in[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$ and let $\pi^{\prime}$ be the smallest prefix of $\pi$ with $\mathit{last}(\pi^{\prime})\in G$. It follows that $\mathrm{di}(\pi^{\prime})$ is also the smallest prefix of ${\mathrm{di}(\pi)}$ with $\mathit{last}(\mathrm{di}(\pi^{\prime}))\in G$. Since ${\mathrm{di}(\pi)}\in\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G$, it follows that ${\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}={\lvert\mathrm{di}(\pi^{\prime})\rvert_{\mathrm{ds}}}\leq\mathrm{di}_{b}$. From Lemma 5 we obtain

[TABLE]

Hence, the prefix $\pi^{\prime}$ reaches $G$ within $b$ time units, implying $\pi\in\lozenge^{I}G$.

• •

Next, we show $\lozenge^{I}G\setminus[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\subseteq\#[{b}]^{{>}{\mathrm{di}_{b}}}$. With Lemma 6 we obtain

[TABLE]

Consider a path $\pi\in\lozenge^{I}G\setminus[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$. Note that $\pi$ reaches $G$ within $b$ time units but with more than $\mathrm{di}_{b}$ digitization steps. Hence, the prefix of $\pi$ up to time point $b$ certainly has more than $\mathrm{di}_{b}$ digitization steps, i.e., $\pi$ satisfies ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi,b)\rvert_{\mathrm{ds}}}>\mathrm{di}_{b}$ which means $\pi\in\#[{b}]^{{>}{\mathrm{di}_{b}}}$.

Case $I=[a,\infty)$ for $a=\mathrm{di}_{a}\delta$:

We have ${\mathrm{di}(I)}=\{\mathrm{di}_{a}+1,\mathrm{di}_{a}+2,\dots\}$.

• •

We show that $[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\setminus\lozenge^{I}G\subseteq\#[{a}]^{{>}{\mathrm{di}_{a}}}$. With Lemma 6 we obtain

[TABLE]

Consider a path $\pi\in[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\setminus\lozenge^{I}G$. As $\pi\notin\lozenge^{I}G$, it follows that $\pi$ has to reach (and leave) $G$ within less than $a$ time units. Let $\bar{\pi}$ be the largest prefix of ${\mathrm{di}(\pi)}$ that satisfies $\mathit{last}(\bar{\pi})\in G$. Our observations yield that $\pi$ leaves $\mathit{last}(\bar{\pi})$ before time point $a$. Hence, $\bar{\pi}$ is a prefix of $\mathrm{di}(\mathit{pref}_{\!\mathit{T}}(\pi,a))$. Moreover, ${\lvert\bar{\pi}\rvert_{\mathrm{ds}}}\in{\mathrm{di}(I)}$ as ${\mathrm{di}(\pi)}\in\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G$. It follows that ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi,a)\rvert_{\mathrm{ds}}}\geq{\lvert\bar{\pi}\rvert_{\mathrm{ds}}}>\mathrm{di}_{a}$ which implies $\pi\in\#[{a}]^{{>}{\mathrm{di}_{a}}}$.

• •

Now consider a path $\pi\in\lozenge^{I}G\setminus[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$. $\pi$ visits $G$ at least once since $\pi\in\lozenge^{I}G$. Moreover, ${\mathrm{di}(\pi)}$ does not visit $G$ after $\mathrm{di}_{a}$ digitization steps due to $\pi\notin[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$. This means $\pi$ visits $G$ only finitely often. Let $\pi^{\prime}=s_{0}\xrightarrow{\kappa_{0}}\dots\xrightarrow{\kappa_{n-1}}s_{n}$ be the largest prefix of $\pi$ such that $s_{n}\in G$. Notice that ${\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}\leq\mathrm{di}_{a}$ holds. Let $\pi^{\prime}\xrightarrow{\kappa}s$ be the prefix of $\pi$ of length $\lvert\pi^{\prime}\rvert+1$. We show by contradiction that $a\leq\mathit{T}(\pi^{\prime}\xrightarrow{\kappa}s)<a+\delta$ holds:

• –

If $\mathit{T}(\pi^{\prime}\xrightarrow{\kappa}s)<a$, then $\mathit{last}(\pi^{\prime})\in G$ is left before time point $a$ which contradicts $\pi\in\lozenge^{I}G$.

• –

Further, assume that $\mathit{T}(\pi^{\prime}\xrightarrow{\kappa}s)\geq a+\delta$. With Lemma 5 we obtain

[TABLE]

Hence, $\pi$ stays at $\mathit{last}(\pi^{\prime})$ for at least $(j+1-{\lvert\pi^{\prime}\rvert_{\mathrm{ds}}})\cdot\delta$ time units which means that \mathrm{di}(\pi^{\prime})\big{(}{\xrightarrow{\bot}}\mathit{last}(\pi^{\prime})\big{)}^{j+1-{\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}}=\bar{\pi} is a prefix of ${\mathrm{di}(\pi)}$. Since ${\lvert\bar{\pi}\rvert_{\mathrm{ds}}}=j+1$, this contradicts $\pi\notin[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$.

We infer that $\pi$ takes at least one transition in the time interval $[a,a+\delta)$. The probability for this can be upper bounded by $1-e^{-\lambda\delta}$, i.e.,

[TABLE]

Case $I=[a,b]$ for $a=\mathrm{di}_{a}\delta$ and $b=\mathrm{di}_{b}\delta$:

We have ${\mathrm{di}(I)}=\{\mathrm{di}_{a}+1,\mathrm{di}_{a}+2,\dots,\mathrm{di}_{b}\}$.

• •

As in the case “$I=[a,\infty)$”, we show that $[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\setminus\lozenge^{I}G\subseteq\#[{a}]^{{>}{\mathrm{di}_{a}}}$. With Lemma 6 we obtain

[TABLE]

Let $\pi\in[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]\setminus\lozenge^{I}G$ and let $\bar{\pi}$ be the largest prefix of ${\mathrm{di}(\pi)}$ with $\mathit{last}(\bar{\pi})\in G$ and ${\lvert\bar{\pi}\rvert_{\mathrm{ds}}}\in{\mathrm{di}(I)}$. Such a prefix exists due to $\pi\in[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$. $\pi$ reaches $\mathit{last}(\bar{\pi})$ with at most $\mathrm{di}_{b}$ digitization steps and therefore within at most $b$ time units (cf. Lemma 5). As $\pi\notin\lozenge^{I}G$, we conclude that $\pi$ has to reach (and leave) $\mathit{last}(\bar{\pi})$ within less than $a$ time units. It follows that ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi,a)\rvert_{\mathrm{ds}}}\geq{\lvert\bar{\pi}\rvert_{\mathrm{ds}}}>\mathrm{di}_{a}$ which implies $\pi\in\#[{a}]^{{>}{\mathrm{di}_{a}}}$.

• •

Next, let $\pi\in\lozenge^{I}G\setminus[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$ and let $\pi^{\prime}=s_{0}\xrightarrow{\kappa_{0}}\dots\xrightarrow{\kappa_{n-1}}s_{n}$ be the largest prefix of $\pi$ such that $s_{n}\in G$ and $\mathit{T}(\pi^{\prime})\leq b$. Such a prefix exists due to $\pi\in\lozenge^{I}G$. We distinguish two cases.

• –

If ${\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}>\mathrm{di}_{b}$, then $\pi\in\#[{b}]^{{>}{\mathrm{di}_{b}}}$ since ${\lvert\mathit{pref}_{\!\mathit{T}}(\pi,b)\rvert_{\mathrm{ds}}}\geq{\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}>\mathrm{di}_{b}$.

• –

If ${\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}\leq\mathrm{di}_{b}$, then ${\lvert\pi^{\prime}\rvert_{\mathrm{ds}}}\leq\mathrm{di}_{a}$ holds due to $\pi\notin[{\lozenge^{{\mathrm{di}(I)}}_{\mathrm{ds}}G}]$. Similar to the case “$I=[a,\infty)^{\prime\prime}$ we can show that $\pi$ takes at least one transition in time interval $[a,a+\delta)$.

It follows that

[TABLE]

Hence,

[TABLE]

∎

0.E.3 Proof of Theorem 4.3

See 4.3

Proof

For simplicity, we assume that only the threshold relation $\geq$ is considered, i.e., ${\vartriangleright}=(\geq,\dots,\geq)$. Furthermore, we restrict ourself to (un)timed reachability objectives. The remaining cases are treated analogously.

First assume a point ${\mathbf{p}}^{\prime}=(p_{1}^{\prime},\dots,p_{d}^{\prime})\in A^{-}$. Consider the point ${\mathbf{p}}=(p_{1},\dots,p_{d})$ satisfying $p_{i}^{\prime}=p_{i}-\varepsilon^{\downarrow}_{i}$ for each index $i$. It follows that ${\mathbf{p}}^{\prime}\in\varepsilon({\mathbb{O}},{\mathbf{p}})$ and thus ${\mathcal{M}_{\delta}},\bar{\sigma}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$ for some scheduler $\bar{\sigma}\in{\mathrm{TA}^{{\mathcal{M}_{\delta}}}}$. Consider the scheduler $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ given by $\sigma(\pi,\alpha)=\bar{\sigma}({\mathrm{di}(\pi)},\alpha)$ for each path $\pi\in{\mathit{FPaths}^{\mathcal{M}}}$ and action $\alpha\in\mathit{Act}$. Notice that $\bar{\sigma}={\mathrm{di}(\sigma)}$. For an index $i$ let ${\mathbb{O}_{i}}$ be the objective ${\mathbb{P}({\lozenge^{I}{G}})}$. It follows that

[TABLE]

With Corollary 1 it follows that

[TABLE]

As this observation holds for all objectives in ${\mathbb{O}}$, it follows that $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}^{\prime}$, implying $\mathit{achieve}^{\mathcal{M}}({\mathbb{O}}\vartriangleright{\mathbf{p}}^{\prime})$.

The proof of the second inclusion is similar. Assume that $\mathcal{M},\sigma\models{\mathbb{O}}\vartriangleright{\mathbf{p}}^{\prime}$ holds for a point ${\mathbf{p}}^{\prime}=(p_{1}^{\prime},\dots,p_{d}^{\prime})\in\mathbb{R}^{d}$ and a scheduler $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$. For some index $i$, consider ${\mathbb{O}_{i}}={\mathbb{P}({\lozenge^{I}{G}})}$. It follows that $\mathrm{Pr}^{\mathcal{M}}_{\sigma}(\lozenge^{I}G)\geq p_{i}^{\prime}$. With Corollary 1 we obtain

[TABLE]

Applying this for all objectives in ${\mathbb{O}}$ yields ${\mathcal{M}_{\delta}},{\mathrm{di}(\sigma)}\models{\mathbb{O}}\vartriangleright{\mathbf{p}}$, where the point ${\mathbf{p}}=(p_{1},\dots,p_{d})\in\mathbb{R}^{d}$ satisfies $p_{i}=p_{i}^{\prime}-\varepsilon^{\uparrow}_{i}$ or, equivalently, $p_{i}^{\prime}=p_{i}+\varepsilon^{\uparrow}_{i}$ for each index $i$. Note that ${\mathbf{p}}^{\prime}\in\varepsilon({\mathbb{O}},{\mathbf{p}})$ which implies ${\mathbf{p}}^{\prime}\in A^{+}$. ∎

Appendix 0.F Comparison to Single-objective Analysis

Corollary 1 generalizes existing results from single-objective timed reachability analysis: For MA $\mathcal{M}$, goal states $G$, time bound $b\in\mathbb{R}_{>0}$, and digitization constant $\delta\in\mathbb{R}_{>0}$ with $\nicefrac{{b}}{{\delta}}=\mathrm{di}_{b}\in\mathbb{N}$, [9, Theorem 5.3] states that

[TABLE]

Corollary 1 generalizes this result by explicitly referring to the schedulers $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$ and ${\mathrm{di}(\sigma)}\in{\mathrm{TA}^{{\mathcal{M}_{\delta}}}}$ under which the claim holds. This extension is necessary as a multi-objective analysis can not be restricted to schedulers that only optimize a single objective.

We remark that the proof in [9, Theorem 5.3] can not be adapted to show our result. The main reason is that the proof relies on an auxiliary lemma which claims that444We adapt [9, Lemma G.2] to our notations from Appendix 0.E.2.

[TABLE]

holds for all schedulers $\sigma\in{\mathrm{GM}^{\mathcal{M}}}$. We show that this claim does not hold. The intuition is as follows. Assume we observe that at most one Markovian transition is taken in $\mathcal{M}$ within the first $\delta$ time units (i.e., we observe a path in $\#[{\delta}]^{{<}{2}}$). The lemma claims that under this observation the probability to reach $G$ within $b$ time units does not increase. We give a counterexample to illustrate that there are schedulers for which this is not true. Consider the MA $\mathcal{M}$ from Figure 9 and let $\sigma$ be the scheduler for $\mathcal{M}$ satisfying

[TABLE]

Hence, $\sigma$ chooses $\alpha$ iff there are less than two digitization steps within the first $\delta$ time units. It follows that the probability to reach $G=\{s_{3}\}$ on a path in $\#[{\delta}]^{{\geq}{2}}$ is zero. We conclude that

[TABLE]

which contradicts Equation 11.

Appendix 0.G Further Details for the Experiments

0.G.1 Benchmark Details

We depict additional information regarding our experiments on multi-objective MAs.

Job scheduling.

The job scheduling case study originates from [13] and was already discussed in Section 1. We consider $N$ jobs that are executed on $K$ identical processors. Each of the $N$ jobs gets a different rate between 1 and 3. We consider the following objectives.

• $\mathbb{E}_{1}$:

Minimize the expected time until all jobs are completed.

• $\mathbb{E}_{2}$:

Minimize the expected time until $\lceil\nicefrac{{N}}{{2}}\rceil$ jobs are completed.

• $\mathbb{E}_{3}$:

Minimize the expected waiting time of the jobs.

• $\mathbb{P}$:

Minimize the probability that the job with the lowest rate is completed before the job with the highest rate.

• $\mathbb{P}_{1}^{\leq}$:

Maximize the probability that all jobs are completed within $\nicefrac{{N}}{{2K}}$ time units.

• $\mathbb{P}_{2}^{\leq}$:

Maximize the probability that $\lceil\nicefrac{{N}}{{2}}\rceil$ jobs are completed within $\nicefrac{{N}}{{4K}}$ time units.

The objectives have been combined as follows: (${\mathbb{O}}^{i}$ refers to the objectives considered in Column $i$ of Table 1):

[TABLE]

Polling.

The polling system is based on [34, 35]. It considers two stations, each having a separate queue storing up to $K$ jobs of $N$ different types. The jobs arrive at Station $i$ (for $i\in\{1,2\}$) with some rate $\lambda_{i}$ as long as the queue of the station is not full. A server polls the two stations and processes the jobs by (nondeterministically) taking a job from a non-empty queue. The time for processing a job is given by a rate which depends on the type of the job. Erasing a job from a queue is unreliable, i.e., there is a $10\,\%$ chance that an already processed job stays in the queue. For $i\in\{1,2\}$ we assume the following objectives:

• $\mathbb{E}_{i}$:

Maximize the expected number of processed jobs of Station $i$ until its queue is full.

• $\mathbb{E}_{2+i}$:

Minimize the expected sum of all waiting times of the jobs arriving at Station $i$ until the queue of Station $i$ is full.

• $\mathbb{P}^{\leq}_{i}$:

Minimize the probability that the queue of Station $i$ is full within two time units.

The objectives have been combined as follows: (${\mathbb{O}}^{i}$ refers to the objectives considered in Column $i$ of Table 1):

[TABLE]

Stream.

This case study considers a client of a video streaming platform. The client consecutively receives $N$ data packages and stores them into a buffer. The buffered packages are processed during the playback of the video. The time it takes to receive (or to process) a single package is modeled by an exponentially distributed delay. Whenever a package is received and the video is not playing, the client nondeterministically chooses whether it starts the playback or whether it keeps on buffering. The latter choice is not reliable, i.e., there is a $1\,\%$ chance that the playback is started anyway. In case of a buffer underrun555A buffer underrun occurs when the next package needs to be processed while the buffer is empty., the playback is paused and the client waits for new packages to arrive. We analyzed the following objectives:

• $\mathbb{E}_{1}$:

Minimize the expected buffering time until the playback is finished.

• $\mathbb{E}_{2}$:

Minimize the expected number of buffer underruns during the playback.

• $\mathbb{E}_{3}$:

Minimize the expected time to start the playback.

• $\mathbb{P}^{\leq}_{1}$:

Minimize the probability for a buffer underrun within 2 time units.

• $\mathbb{P}^{\leq}_{2}$:

Maximize the probability that the playback starts within 0.5 time units.

The objectives have been combined as follows: (${\mathbb{O}}^{i}$ refers to the objectives considered in Column $i$ of Table 1):

[TABLE]

Mutex.

This case study regards a randomized mutual exclusion protocol based on [36, 35]. Three processes nondeterministically choose a job for which they need to enter the critical section. The amount of time a process spends in its critical section is given by a rate which depends on the chosen job. There are $N$ different types of jobs. For each $i\in\{1,2,3\}$ the following objective are considered:

• $\mathbb{P}^{\leq}_{i}$:

Maximize the probability that Process $i$ enters its critical section within 0.5 time units.

• $\mathbb{P}^{\leq}_{3+i}$:

Maximize the probability that Process $i$ enters its critical section within 1 time unit.

The objectives have been combined as follows: (${\mathbb{O}}^{i}$ refers to the objectives considered in Column $i$ of Table 1):

[TABLE]

0.G.2 Comparison with PRISM

We considered PRISM 4.3.1 obtained from its website www.prismmodelchecker.org. We conducted our experiments on PRISM with both variants of the value iteration-based implementation (standard and Gauss-Seidel) and chose the faster variant for each benchmark instance. For all experiments the approximation precision $\eta=0.001$ was considered.

The detailed results are given in Table 3. We depict the different benchmark instances with the number of states of the MDP (Column #states) and the considered combination of objectives ($\mathbb{P}$ represents an (untimed) probabilistic objective, $\mathbb{E}$ an expected reward objective, and $\mathbb{C}^{\leq}$ a step-bounded reward objective). Column iter lists the time required for the iterative exploration of the set of achievable points as described in [15]. In Column verif we depict the verification time – including the time for the iterations as well as the conducted preprocessing steps. Column total indicates the total runtime of the tool which includes model building time and verification time. For our implementation, we also list the number of vertices of the obtained under-approximation (Column pts).

During our experiments we observed some issues considering the implementation in PRISM. For example PRISM does not detect that both objectives considered for the sched.-instances yield infinite rewards under every possible resolution of non-determinism. Instead of that, PRISM gives an incorrect answer.

0.G.3 Comparison with IMCA

We consider IMCA 1.6 obtained from https://github.com/buschko/imca. The experiments on IMCA have been conducted with and without enabling value-iteration and we chose the faster variant for each benchmark instance. For timed reachability objectives, the precision $\eta=0.01$ was considered in all experiments.

The resulting verification times are given in Table 4. We depict the different benchmark instances with the number of states of the MA (Column #states) and the considered objective (as discussed in App. 0.G.1). Besides the run-times of IMCA, we depict the run-times of our implementation (effectively performing multi-objective model checking with only one objective) in Column Storm (multi). Column Storm (single) shows the run-times obtained when Storm is invoked with standard (single-objective) model checking methods.