Verification and Control of Turn-Based Probabilistic Real-Time Games

TL;DR

This paper introduces a new model for turn-based probabilistic timed multi-player games, enabling quantitative verification of probabilistic, real-time, multi-agent systems with applications in security and scheduling.

Contribution

It extends probabilistic timed automata to multi-player settings with nondeterminism and real-time clocks, providing methods to compute probabilities and expected costs for verification.

Findings

Successfully computed probabilities and costs in case studies.

Extended verification techniques to multi-player probabilistic real-time systems.

Demonstrated applicability in security and task scheduling scenarios.

Abstract

Quantitative verification techniques have been developed for the formal analysis of a variety of probabilistic models, such as Markov chains, Markov decision process and their variants. They can be used to produce guarantees on quantitative aspects of system behaviour, for example safety, reliability and performance, or to help synthesise controllers that ensure such guarantees are met. We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. Building on the digital clocks approach for the simpler model of probabilistic timed automata, we show how to compute the key measures that underlie quantitative verification, namely the probability and expected cumulative price to reach a target. We illustrate this on case studies from computer security and task scheduling.

Equations

$$\begin{array}[]{rcl}\mathbb{P}^{\sigma}_{\sf G}(F)&\;\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}&{\mathit{Prob}}^{\sigma}(\{\pi\in\mathit{IPaths}^{\sigma}\mid\pi(i)\in F\;\mbox{for some}\;i\in\mathbb{N}\})\\ \mathbb{E}^{\sigma}_{\sf G}(F)&\;\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}&\int_{\pi\in\mathit{IPaths}^{\sigma}}\mathit{rew}(\pi,F)\>\mathrm{d}{\mathit{Prob}}^{\sigma}\end{array}$$

$$\begin{array}[]{rcl}\mathit{rew}(\pi,F)&\;\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}&\sum_{i=0}^{k_{F}}R(\pi(i),\pi[i])\end{array}$$

$$\begin{array}[]{rcl}\mathbb{P}^{C}_{\sf G}(F)&\;\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}&\sup_{\sigma_{1}\in\Sigma^{1}}\inf_{\sigma_{2}\in\Sigma^{2}}\mathbb{P}^{\sigma_{1},\sigma_{2}}_{{\sf G}^{C}}(F)\\ \mathbb{E}^{C}_{\sf G}(F)&\;\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}&\sup_{\sigma_{1}\in\Sigma^{1}}\inf_{\sigma_{2}\in\Sigma^{2}}\mathbb{E}^{\sigma_{1},\sigma_{2}}_{{\sf G}^{C}}(F)\end{array}$$

$$\begin{array}[]{rcl}\sup_{\sigma_{1}\in\Sigma^{1}}\inf_{\sigma_{2}\in\Sigma^{2}}\mathbb{P}^{\sigma_{1},\sigma_{2}}(F)&\;=&\inf_{\sigma_{2}\in\Sigma^{2}}\sup_{\sigma_{1}\in\Sigma^{1}}\mathbb{P}^{\sigma_{1},\sigma_{2}}(F)\,.\end{array}$$

$$\begin{array}[]{rcl}\mu(l^{\prime},v^{\prime})&=&\sum\limits_{X\subseteq{\mathcal{X}}\wedge v^{\prime}{=}(v{+}t)[X{:=}0]}\mathit{prob}(l,a)(X,l^{\prime})\end{array}$$

$$\displaystyle\mathbb{E}^{\sigma}_{n+1}(\pi,F_{\mathbb{T}})=\left\{\begin{array}[]{cl}0&\;\mbox{if $(l,v)\in F_{\mathbb{T}}$}\\ {r}_{L}(l){\cdot}t+{r}_{{\mathit{Act}}}(l,a)+\sum\limits_{s^{\prime}\in S}\mu(s^{\prime})\cdot\mathbb{E}^{\sigma}_{n}(\pi\xrightarrow{t,a}s^{\prime},F_{\mathbb{T}})&\;\mbox{otherwise.}\end{array}\right.$$

$${\mathbb{E}}_n^{{\sigma }_1^{lb},{\sigma }_2^{lb}}(F_{\mathbb{N}})⩽{\mathbb{E}}_n^{{\sigma }_1,{\sigma }_2}(F_{\mathbb{R}})⩽{\mathbb{E}}_n^{{\sigma }_1^{ub},{\sigma }_2^{ub}}(F_{\mathbb{N}}).$$

$${\mathbb{E}}_n^{{\sigma }_1,{\sigma }_2}(F_{\mathbb{N}})={\mathbb{E}}_n^{{\sigma }_1^{\prime },{\sigma }_2^{\prime }}(F_{\mathbb{R}}).$$

$$\begin{array}[]{c}\sup\nolimits_{\sigma_{1}^{\prime}\in\Sigma^{1}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}}\!\!\inf\nolimits_{\sigma_{2}^{\prime}\in\Sigma^{2}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}}\mathbb{E}^{\sigma_{1}^{\prime},\sigma_{2}^{\prime}}_{n}(F_{\mathbb{N}})\;=\;\sup\nolimits_{\sigma_{1}\in\Sigma^{1}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}}\!\!\inf\nolimits_{\sigma_{2}\in\Sigma^{2}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}}\mathbb{E}^{\sigma_{1},\sigma_{2}}_{n}(F_{\mathbb{R}})\,.\end{array}$$

$$\begin{array}[]{c}\lim\limits_{n\rightarrow\infty}\sup\nolimits_{\sigma_{1}^{\prime}\in\Sigma^{1}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}}\!\!\inf\nolimits_{\sigma_{2}^{\prime}\in\Sigma^{2}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}}\mathbb{E}^{\sigma_{1}^{\prime},\sigma_{2}^{\prime}}_{n}(F_{\mathbb{N}})=\lim\limits_{n\rightarrow\infty}\sup\nolimits_{\sigma_{1}\in\Sigma^{1}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}}\!\!\inf\nolimits_{\sigma_{2}\in\Sigma^{2}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}}\mathbb{E}^{\sigma_{1},\sigma_{2}}_{n}(F_{\mathbb{R}})\end{array}$$

$$\begin{array}[]{c}\sup\nolimits_{\sigma_{1}^{\prime}\in\Sigma^{1}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}}\!\!\inf\nolimits_{\sigma_{2}^{\prime}\in\Sigma^{2}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}}\mathbb{E}^{\sigma_{1}^{\prime},\sigma_{2}^{\prime}}(F_{\mathbb{N}})\;=\;\sup\nolimits_{\sigma_{1}\in\Sigma^{1}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}}\!\!\inf\nolimits_{\sigma_{2}\in\Sigma^{2}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}}\mathbb{E}^{\sigma_{1},\sigma_{2}}(F_{\mathbb{R}})\,.\end{array}$$

$$[t]_{\varepsilon}=\left\{\begin{array}[]{cl}\lfloor t\rfloor&\mbox{if $t\leqslant\lfloor t\rfloor+\varepsilon$}\\ \lceil t\rceil&\mbox{otherwise}.\end{array}\right.$$

$$\begin{array}[]{c}[\pi]_{\varepsilon}=(\bar{l},\mathbf{0})\xrightarrow{t_{1}^{\prime},a_{0}}(l_{1},[v_{1}]_{\varepsilon})\xrightarrow{t_{1}^{\prime},a_{1}}\cdots\end{array}$$

$${\mathit{Prob}}^{\sigma}(\Pi)\;=\;{\mathit{Prob}}^{\sigma}(\{\pi^{\prime}\in\mathit{IPaths}^{\sigma}\mid\exists\pi\in\Pi.\,(\mbox{$\pi$ is a prefix of $\pi^{\prime}$})\})$$

$$\pi \stackrel{t,a}{\to }\stackrel{\text{mbox}\mathrm{def}}{=}\{{\pi }^{\prime }\in {FPaths}^{\sigma }\mid \exists s\in S.({\pi }^{\prime }=\pi \stackrel{t,a}{\to }s)\}.$$

$${\sigma }_i^{\epsilon }(\pi )(t,a)=\frac{{Prob}^{\sigma }([\pi \stackrel{t,a}{\to }{]}_{\epsilon }^{-1})}{{Prob}^{\sigma }([\pi {]}_{\epsilon }^{-1})}$$

$${\mathit{Prob}}^{\sigma^{\varepsilon}}(\pi)={\mathit{Prob}}^{\sigma}([\pi]_{\varepsilon}^{-1})\;\;\mbox{for all $\pi\in\mathit{FPaths}^{\sigma^{\varepsilon}}$}$$

$${Prob}^{{\sigma }^{\epsilon }}(\pi )={Prob}^{{\sigma }^{\epsilon }}({\pi }^{\prime })\cdot {\sigma }_i^{\epsilon }({\pi }^{\prime })(a)\cdot \mu (s^{\prime })$$

$$={Prob}^{\sigma }([{\pi }^{\prime }{]}_{\epsilon }^{-1})\cdot {\sigma }_i^{\epsilon }({\pi }^{\prime })(t,a)\cdot \mu (s^{\prime })$$

$$={Prob}^{\sigma }([{\pi }^{\prime }{]}_{\epsilon }^{-1})\cdot \frac{{Prob}^{\sigma }([{\pi }^{\prime }\stackrel{t,a}{\to }{]}_{\epsilon }^{-1})}{{Prob}^{\sigma }([{\pi }^{\prime }{]}_{\epsilon }^{-1})}\cdot \mu (s^{\prime })$$

$$={Prob}^{\sigma }([{\pi }^{\prime }\stackrel{t,a}{\to }{]}_{\epsilon }^{-1})\cdot \mu (s^{\prime })$$

$$={Prob}^{\sigma }\{\pi \in {FPaths}^{{\sigma }_1,{\sigma }_2}\mid [\pi {]}_{\epsilon }={\pi }^{\prime }\stackrel{t,a}{\to }{s}^{\prime }\}$$

$$={Prob}^{\sigma }([\pi {]}_{\epsilon }^{-1})$$

$$\pi (i)\in F_{\mathbb{R}}$$

$${\mathbb{P}}^{\sigma }(F_{\mathbb{R}})$$

$$={Prob}^{{\sigma }^{\prime }}([\{\pi \in {IPaths}^{\sigma }\mid \pi (i)\in F\text{mbox}forsomei\in \mathbb{N}\}{]}_{\epsilon }^{-1})$$

$${\mathbb{P}}^{\sigma }(F_{\mathbb{R}})$$

$$={\mathbb{P}}^{{\sigma }^{\prime }}(F_{\mathbb{N}})$$

$${\inf }_{{\sigma }_2\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{R}}^C}^2}{\mathbb{P}}^{{\sigma }_1,{\sigma }_2}(F_{\mathbb{R}})⩾{\inf }_{{\sigma }_2^{\prime }\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{N}}^C}^2}{\mathbb{P}}^{{\sigma }_1^{\prime },{\sigma }_2^{\prime }}(F_{\mathbb{N}}).$$

$${\inf }_{{\sigma }_2\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{R}}^C}^2}{\mathbb{P}}^{{\sigma }_1,{\sigma }_2}(F_{\mathbb{R}})⩽{\inf }_{{\sigma }_2^{\prime }\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{N}}^C}^2}{\mathbb{P}}^{{\sigma }_1^{\prime },{\sigma }_2^{\prime }}(F_{\mathbb{N}})$$

$${\inf }_{{\sigma }_2\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{R}}^C}^2}{\mathbb{P}}^{{\sigma }_1,{\sigma }_2}(F_{\mathbb{R}})={\inf }_{{\sigma }_2^{\prime }\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{N}}^C}^2}{\mathbb{P}}^{{\sigma }_1^{\prime },{\sigma }_2^{\prime }}(F_{\mathbb{N}}).$$

$${\sup }_{{\sigma }_1\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{R}}^C}^1}{\inf }_{{\sigma }_2\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{R}}^C}^2}{\mathbb{P}}^{{\sigma }_1,{\sigma }_2}(F_{\mathbb{R}})={\sup }_{{\sigma }_1^{\prime }\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{N}}^C}^1}{\inf }_{{\sigma }_2^{\prime }\in {\Sigma }_{[[\mathsf{P}]{]}_{\mathbb{N}}^C}^2}{\mathbb{P}}^{{\sigma }_1^{\prime },{\sigma }_2^{\prime }}(F_{\mathbb{N}})$$

$$\max \{\mathbf{cx}\mid \mathbf{x}⩾0\wedge \mathbf{Ax}⩽\mathbf{b}\}=\min \{\mathbf{yb}\mid \mathbf{y}⩾0\wedge \mathbf{yA}⩾\mathbf{c}\}$$

$$\displaystyle\mathbb{A}^{\sigma}_{n+1}(\pi,F_{\mathbb{T}})\;=\;\left\{\begin{array}[]{cl}0&\;\mbox{if $(l,v)\in F_{\mathbb{T}}$}\\ {r}_{{\mathit{Act}}}(l,a)+\sum\limits_{s^{\prime}\in S}\mu(s^{\prime})\cdot\mathbb{A}^{\sigma}_{n}(\pi\xrightarrow{t,a}s^{\prime},F_{\mathbb{T}})&\;\mbox{otherwise.}\end{array}\right.$$

Full text

1 Introduction

Probability is a crucial tool for modelling computerised systems. We can use it to model uncertainty, for example in the operating environment of an autonomous vehicle or a wireless sensor network, and we can reason about systems that use randomisation, from probabilistic routing in anonymity network protocols to symmetry breaking in communication protocols.

Formal verification of such systems can provide us with rigorous guarantees on, for example, the performance and reliability of computer networks [7], the amount of inadvertent information leakage by a security protocol [5], or the safety level of an airbag control system [2]. To do so requires us to model and reason about a range of quantitative aspects of a system’s behaviour: probability, time, resource usage, and many others.

Quantitative verification techniques have been developed for a wide range of probabilistic models. The simplest are Markov chains, which model the evolution of a stochastic system over discrete time. Markov decision processes (MDPs) additionally include nondeterminism, which can be used either to model the uncontrollable behaviour of an adversary or to determine an optimal strategy (or policy) for controlling the system. Generalising this model further still, we can add a notion of real time, yielding the model of probabilistic timed automata (PTAs). This is done in the same way as for the widely used model of timed automata (TAs), adding real-valued variables called clocks to the model. Tools such as PRISM [34] and Storm [21] support verification of a wide range of properties of these different probabilistic models.

Another dimension that we can add to these models and verification techniques is game-theoretic aspects. These can be used to represent, for example, the interaction between an attacker and a defender in a computer security protocol [4], between a controller and its environment, or between participants in a communication protocol who have opposing goals [28]. Stochastic multi-player games include choices made by multiple players who can either collaborate or compete to achieve their goals. Tool support for verification of stochastic games, e.g. PRISM-games [41], has also been developed and deployed successfully in a variety of application domains.

In this paper, we consider a modelling formalism that captures all these aspects: probability, nondeterminism, time and multiple players. We define a model called turn-based probabilistic timed multi-player games (TPTGs), which can be seen as either an extension of PTAs to incorporate multiple players, or a generalisation of stochastic multi-player games to include time. Building on known techniques for the simpler classes of models, we show how to compute key properties of these models, namely probabilistic reachability (the probability of reaching a set of target states) and expected price reachability (the expected price accumulated before reaching a set of target states).

Existing techniques for PTAs largely fall into two classes: zone-based and digital clocks, both of which construct and analyse a finite-state abstraction of the model. Zones are symbolic expressions representing sets of clock values. Zone-based approaches for analysing PTAs were first introduced in [39, 40, 33] and recent work extended them to the analysis of expected time [29] and expected price reachability [35]. The digital clocks approach works by mapping real-valued clocks to integer-valued ones, reducing the problem of solving a PTA to solving a (discrete-time) MDP. This approach was developed for PTAs in [38] and recently extended to the analysis of partially observable PTAs in [46].

In this paper, we show how a similar idea can be used to reduce the verification problem for TPTGs to an equivalent one over (discrete-time) stochastic games. More precisely, for the latter, we use turn-based stochastic games (TSGs). We first present the model of TPTGs and give two alternative semantics: one using real-valued clocks and the other using (integer-valued) digital clocks. Then, we prove the correspondence between these two semantics. Next, we demonstrate the application of this approach to two case studies from the domains of computer security and task scheduling. Using a translation from TPTGs to TSGs and the model checking tool PRISM-games, we show that a variety of useful properties can be studied on these case studies.

Related Work. Timed games were introduced and shown to be decidable in [43, 6, 1]. These games have since been extensively studied; we mention [52, 19], where efficient algorithms are investigated, and [47], which concerns the synthesis of strategies that are robust to stochastic perturbation in clock values. Also related is the tool UPPAAL TIGA [8], which allows the automated analysis of reachability and safety problems for timed games.

Priced (or weighted) timed games were introduced in [49, 3, 11], which extend timed games by associating integer costs with locations and transitions, and optimal cost reachability was shown to be decidable under certain restrictions. The problem has since been shown to be undecidable for games with three or more clocks [17, 10]. Priced timed games have recently been extended to allow partial observability [18] and to energy games [14].

Two-player (concurrent) probabilistic timed games were introduced in [24]. The authors demonstrated that such games are not determined (even when all clock constraints are closed) and investigated the complexity of expected time reachability for such games. Stochastic timed games [13, 16] are turn-based games where time delays are exponentially distributed. A similar model, based on interactive Markov chains [27], is considered in [15].

2 Background

We start with some background and notation on turn-based stochastic games (TSGs). For a set $X$, let ${\mathit{Dist}}(X)$ denote the set of discrete probability distributions over $X$ and $\mathbb{R}$ the set of non-negative real numbers.

Definition 1 (Turn-based stochastic multi-player game)

A turn-based stochastic multi-player game (TSG) is a tuple ${\sf G}{=}(\Pi,S,{\bar{s}},\mathit{A},\langle S_{i}\rangle_{i\in\Pi},\delta,R)$ where $\Pi$ is a finite set of players, $S$ is a (possibly infinite) set of states, ${\bar{s}}\in S$ is an initial state, $\mathit{A}$ is a (possibly infinite) set of actions, $\langle S_{i}\rangle_{i\in\Pi}$ is a partition of the state space, $\delta:S{\times}\mathit{A}\rightarrow{\mathit{Dist}}(S)$ is a (partial) transition function and $R:S{\times}\mathit{A}\rightarrow\mathbb{R}$ is a price (or reward) function.

The transition function is partial in the sense that $\delta$ need not be defined for all state-action pairs. For each state $s$ of a TSG ${\sf G}$, there is a set of available actions given by $A(s)\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\{a\in\mathit{A}\mid\delta(s,a)\;\mbox{is defined}\}$. The choice of which available action is taken in state $s$ is under the control of a single player: the player $i$ such that $s\in S_{i}$. If player $i$ selects action $a\in\mathit{A}(s)$ in $s$, then the probability of transitioning to state $s^{\prime}$ equals $\delta(s,a)(s^{\prime})$ and a price of $R(s,a)$ is accumulated.

Paths and strategies. A path of a TSG ${\sf G}$ is a sequence $\pi=s_{0}\xrightarrow{a_{0}}s_{1}\xrightarrow{a_{1}}\cdots$ such that $s_{i}\in S$, $a_{i}\in A(s_{i})$ and $\delta(s_{i},a_{i})(s_{i+1}){>}0$ for all $i{\geqslant}0$. For a path $\pi$, we denote by $\pi(i)$ the $(i{+}1)$th state of the path, $\pi[i]$ the action associated with the $(i{+}1)$th transition and, if $\pi$ is finite, $\mathit{last}(\pi)$ the final state. The length of a path $\pi$, denoted $|\pi|$, equals the number of transitions. For a path $\pi$ and $k{<}|\pi|$, let $\pi^{(k)}$ be the $k$th prefix of $\pi$. Let $\mathit{FPaths}_{\sf G}$ and $\mathit{IPaths}_{\sf G}$ equal the sets of finite and infinite paths starting in the initial state ${\bar{s}}$.

A strategy for player $i\in\Pi$ is a way of resolving the choice of action in each state under the control of player $i$, based on the game’s execution so far. Formally, a strategy $\sigma$ for player $i\in\Pi$ is a function $\sigma_{i}:\{\pi\in\mathit{FPaths}_{\sf G}\mid\mathit{last}(\pi)\in S_{i}\}\rightarrow{\mathit{Dist}}(\mathit{A})$ such that, if $\sigma_{i}(\pi)(a){>}0$, then $a\in A(\mathit{last}(\pi))$. The set of all strategies of player $i\in\Pi$ is represented by $\Sigma^{i}_{\sf G}$ (when clear from the context we will drop the subscript ${\sf G}$). A strategy for player $i$ is deterministic if it always selects actions with probability 1, and memoryless if it makes the same choice for any paths that end in the same state.

A strategy profile for ${\sf G}$ takes the form $\sigma{=}\langle\sigma_{i}\rangle_{i\in\Pi}$, listing a strategy for each player. We use $\mathit{FPaths}^{\sigma}$ and $\mathit{IPaths}^{\sigma}$ for the sets of finite and infinite paths corresponding to the choices made by the profile $\sigma$ when starting in the initial state. For a given profile $\sigma$, the behaviour of ${\sf G}$ is fully probabilistic and we can define a probability measure ${\mathit{Prob}}^{\sigma}$ over the set of infinite paths $\mathit{IPaths}^{\sigma}$ [31].

Properties. Two fundamental properties of quantitative models are the probability of reaching a set of target states and the expected price accumulated before doing so. For a strategy profile $\sigma$ and set of target states $F$ of a TSG ${\sf G}$, the probability of reaching $F$ and expected price accumulated before reaching $F$ from the initial state ${\bar{s}}$ under the profile $\sigma$ are given by the following (again, when it is clear from the context, we will drop the subscript ${\sf G}$):

[TABLE]

where for any infinite path $\pi$:

[TABLE]

and $k_{F}{=}\min\{k{-}1\mid\pi(k)\in F\}$ if $\pi(k)\in F$ for some $k\in\mathbb{N}$ and $k_{F}{=}\infty$ otherwise.

To quantify the above properties over the strategies of the players, we consider a coalition $C\subseteq\Pi$ who try to maximise the property of interest, while the remaining players $\Pi{\setminus}C$ try to minimise it. Formally, we have the following definition:

[TABLE]

where ${\sf G}^{C}$ is the two-player game constructed from ${\sf G}$ where the states controlled by player 1 equal $\cup_{i\in C}S_{i}$ and the states controlled by player 2 equal $\cup_{i\in\Pi{\setminus}C}S_{i}$.

The above definition yields the optimal value of ${\sf G}$ if it is determined, i.e., if the maximum value that the coalition $C$ can ensure equals the minimum value that the coalition $\Pi\setminus C$ can ensure. Formally, the definition of determinacy and optimal strategies for probabilistic reachability properties of TSGs are given below, and the case of expected reachability is analogous (replacing $\mathbb{P}$ with $\mathbb{E}$).

Definition 2

For a TSG ${\sf G}$, target $F$ and coalition of players $C$, we say the game ${\sf G}^{C}$ is determined with respect to probabilistic reachability if:

[TABLE]

Furthermore, a strategy $\sigma_{1}^{\star}\in\Sigma_{1}$ is optimal if $\mathbb{P}^{\sigma_{1}^{\star},\sigma_{2}}(F)\geqslant\mathbb{P}^{C}_{\sf G}(F)$ for all $\sigma_{2}\in\Sigma^{2}$ and strategy $\sigma_{2}^{\star}\in\Sigma_{2}$ is optimal if $\mathbb{P}^{\sigma_{1},\sigma_{2}^{\star}}(F)\leqslant\mathbb{P}^{C}_{\sf G}(F)$ for all $\sigma_{1}\in\Sigma^{1}$.

As we shall demonstrate, the games we consider are determined with respect to probabilistic and expected reachability, and optimal strategies exist. In particular, finite-state and finite-branching TSGs are determined [32] and efficient techniques exist to approximate optimal values and optimal strategies [20, 22]. These techniques underlie the model checking algorithms for logics such as rPATL, defined for TSGs and implemented in the tool PRISM-games [41].

3 Turn-based Probabilistic Timed Multi-Player Games

We now introduce turn-based probabilistic timed multi-player games (TPTGs), a framework for modelling systems which allows probabilistic, non-deterministic, real-time and competitive behaviour. Let $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$ be the time domain of either the non-negative reals or natural numbers.

Clocks, valuations and clock constraints. We assume a finite set of clocks $\mathcal{X}$. A clock valuation is a function $v:\mathcal{X}\rightarrow\mathbb{T}$; the set of all clock valuations is denoted $\mathbb{T}^{\mathcal{X}}$. Let $\mathbf{0}$ be the clock valuation that assigns the value 0 to all clocks. For any set of clocks $X\subseteq\mathcal{X}$ and clock valuation $v\in\mathbb{T}^{\mathcal{X}}$, let $v[X{:=}0]$ be the clock valuation such that, for any clock $x$, we have $v[X{:=}0](x)$ equals [math] if $x\in X$ and $v(x)$ otherwise. Furthermore, for any time instant $t\in\mathbb{T}$, let $v{+}t$ be the clock valuation such that $(v{+}t)(x)=v(x){+}t$ for all $x\in\mathcal{X}$. A closed, diagonal-free clock constraint111A constraint is closed if does not contain strict inequalities and diagonal-free if there are no inequalities of the form $x{-}y\sim c$ for $x,y\in\mathcal{X}$, $\sim\in\{<,\leqslant,\geqslant,>\}$ and $c\in\mathbb{N}$. $\zeta$ is a conjunction of inequalities of the form $x{\leqslant}c$ or $x{\geqslant}c$, where $x\in\mathcal{X}$ and $c\in\mathbb{N}$. We write $v{\,\models\,}\zeta$ if the clock valuation $v$ satisfies the clock constraint $\zeta$ and use $\mathit{CC}({\mathcal{X}})$ for the set of all clock constraints over $\mathcal{X}$.

We are now in a position to present the syntax and semantics of TPTGs.

Definition 3 (TPTG syntax)

A turn-based probabilistic timed multi-player game (TPTG) is a tuple $\mathsf{P}{=}(\Pi,\mathit{L},\overline{l},\mathcal{X},{\mathit{Act}},\langle\mathit{L}_{i}\rangle_{i\in\Pi},\mathit{inv},\mathit{enab},\mathit{prob},{r})$ where:

• •

$\Pi$ is a finite set of players;

• •

$\mathit{L}$ is a finite set of locations and $\overline{l}\in\mathit{L}$ is an initial location;

• •

$\mathcal{X}$ is a finite set of clocks;

• •

${\mathit{Act}}$ is a finite set of actions;

• •

$\langle\mathit{L}_{i}\rangle_{i\in\Pi}$ is a partition of $\mathit{L}$;

• •

$\mathit{inv}:\mathit{L}\rightarrow\mathit{CC}({\mathcal{X}})$ is an invariant condition;

• •

$\mathit{enab}:\mathit{L}{\times}\mathit{A}\rightarrow\mathit{CC}({\mathcal{X}})$ is an enabling condition;

• •

$\mathit{prob}:\mathit{L}{\times}\mathit{A}\rightarrow{\mathit{Dist}}(2^{\mathcal{X}}{\times}\mathit{L})$ is a (partial) probabilistic transition function;

• •

${r}=({r}_{L},{r}_{{\mathit{Act}}})$ is a price structure where ${r}_{L}:L\rightarrow\mathbb{N}$ is a location price function and ${r}_{{\mathit{Act}}}:L{\times}{\mathit{Act}}\rightarrow\mathbb{N}$ an action price function.

As for PTAs [45], a state of a TPTG $\mathsf{P}$ is a location-clock valuation pair $(l,v)$ such that the clock valuation satisfies the invariant $\mathit{inv}(l)$. The transition choice in $(l,v)$ is under the control of the player $i$ where $l\in L_{i}$. A transition is a time-action pair $(t,a)$ which represents letting time $t$ elapse and then performing action $a$. Time can elapse if the invariant of the current location remains continuously satisfied and action $a$ can be performed only if the enabling condition is satisfied. If action $a$ is taken in location $l$, then the probability of moving to location $l^{\prime}$ and resetting the set of clocks $X$ equals $\mathit{prob}(l,a)(X,l^{\prime})$. TPTGs have both location prices, which are accumulated at rate ${r}_{L}(l)$ when time passes in location $l$, and action prices, where ${r}_{{\mathit{Act}}}(l,a)$ is accumulated when performing action $a$ in location $l$. Formally, the semantics of a TPTG is a TSG defined as follows.

Definition 4 (TPTG semantics)

For any time domain $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$ and TPTG $\mathsf{P}{=}(\Pi,\mathit{L},\overline{l},\mathcal{X},{\mathit{Act}},\langle\mathit{L}_{i}\rangle_{i\in\Pi},\mathit{inv},\mathit{enab},\mathit{prob},{r})$ the semantics of $\mathsf{P}$ with respect to the time domain $\mathbb{T}$ is the TSG ${[\![{{\sf P}}]\!]_{\mathbb{T}}}{=}(\Pi,S,{\bar{s}},\mathit{A},\langle S_{i}\rangle_{i\in\Pi},\delta,R)$ where:

• •

$S=\{(l,v)\in\mathit{L}{\times}\mathbb{T}^{\mathcal{X}}\mid v{\,\models\,}\mathit{inv}(l)\}$ and ${\bar{s}}=(\overline{l},\mathbf{0});$

• •

$\mathit{A}=\mathbb{T}{\times}{\mathit{Act}}$;

• •

$S_{i}=\{(l,v)\in S\mid l\in\mathit{L}_{i}\}$ for $i\in\Pi$;

• •

for any $(l,v)\in S$ and $(t,a)\in\mathit{A}$ we have $\delta((l,v),(t,a))=\mu$ if and only if $v{+}t^{\prime}{\,\models\,}\mathit{inv}(l)$ for all $0{\leqslant}t^{\prime}{\leqslant}t$, $v{+}t{\,\models\,}\mathit{enab}(l,a)$ and for any $(l^{\prime},v^{\prime})\in S$:

[TABLE]

• •

$R((l,v),(t,a))=t{\cdot}{r}_{L}(l)+{r}_{{\mathit{Act}}}(l,a)$ for all $(l,v)\in S$ and $(t,a)\in\mathit{A}$.

We follow the approach of [30, 24, 29] and use time-action pairs in the transition function of Definition 4. As explained in [29], this yields a more expressive semantics than having separate time and action transitions.

Example 1

Consider the TPTG in Fig. 1 which represents a simple communication protocol. There are two players: the sender and the medium, with the medium controlling the location $\mathit{medium}$ and the sender all other locations. The TPTG has two clocks: $x$ is used to keep track of the time it takes to send a message and $y$ the elapsed time. In the initial location $\mathit{send}$, the sender waits between 1 and 2 time units before sending the message. The message then passes through the medium that can either delay the message for between 1 and 2 time units after which it arrives with probability 0.5, or delay the message for 4 time units after which it arrives with probability 1. If the message does not arrive, then the sender tries to send it again until reaching a timeout after 24 time units.

As for PTAs, in the standard (dense-time) semantics for a TPTG the time domain $\mathbb{T}$ equals $\mathbb{R}$. This yields an infinite state model which is not amenable to verification. One approach that yields a finite state representation used in the case of PTAs is the digital clocks semantics [38]. This is based on replacing the real-valued clocks with clocks taking only values from a bounded set of integers. In order to give the definition for a TPTG $\mathsf{P}$, for any clock $x$ of $\mathsf{P}$ we define $k_{x}$ to be the greatest constant to which $x$ is compared in the clock constraints of $\mathsf{P}$. This allows us to use bounded clock values since, if the value of the clock $x$ exceeds $k_{x}$, then the exact value will not affect the satisfaction of the invariants and enabling conditions of $\mathsf{P}$, and therefore does not influence the behaviour.

Definition 5 (Digital clocks semantics)

The digital clocks semantics of a TPTG $\mathsf{P}$, denoted ${[\![{{\sf P}}]\!]_{\mathbb{N}}}$, is obtained from Definition 4, by setting $\mathbb{T}$ equal to $\mathbb{N}$ and for any $v\in\mathbb{N}^{\mathcal{X}}$, $t\in\mathbb{N}$ and $x\in\mathcal{X}$ letting $(v{+}t)(x)=\min\{v(x){+}t,k_{x}{+}1\}$.

We restrict our attention to time-divergent (also called non-Zeno) behaviour. More precisely, we only consider strategies for the players that do not generate unrealisable executions, i.e., executions in which time does not advance beyond a certain point. We achieve this by restricting to TPTGs that satisfy the syntactic conditions for PTAs given in [45], derived from results on TAs [51, 53]. In addition, we require the following assumptions to ensure the correctness of the digital clocks semantics.

Assumption 1

For any TPTG $\mathsf{P}:$ (a) all invariants of ${\sf P}$ are bounded; (b) all clock constraints are closed and diagonal free; (c) all probabilities are rational.

Regarding Assumption 1(a), in fact bounded TAs are as expressive as standard TAs [9], and this result carries over to TPTGs.

To facilitate higher-level modelling, PTAs can be extended with parallel composition, discrete variables, urgent transitions and locations and resetting clocks to integer values [45]. We can extend TPTGs in a similar way, and will use these constructs in Section 5.

4 Correctness of the Digital Clocks Semantics

We now show that, under Assumption 1, optimal probabilistic and expected price reachability values agree under the digital and dense-time semantics. As for PTAs [45], by modifying the TPTG under study, we can reduce time-bounded probabilistic reachability properties to probabilistic reachability properties and both expected time-bounded cumulative price properties and expected time-instant price properties to expected reachability properties. In each case the modifications to the TPTG preserve Assumption 1, and therefore the digital clocks semantics can also be used to verify these classes of properties.

For the remainder of this section, we fix a TPTG $\mathsf{P}$, coalition of players $C$ and set of target locations $F\subseteq\mathit{L}$, and let $F_{\mathbb{T}}=\{(l,v)\in F{\times}\mathbb{T}^{\mathcal{X}}\mid v{\,\models\,}\mathit{inv}(l)\}$ for $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$. We have omitted the proofs that closely follow those for PTAs [38]. The missing definitions and proofs can be found in Appendix 0.A.

We first present results relating to the determinacy and existence of optimal strategies for the games ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ and a correspondence between the strategy profiles of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ and ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$.

Proposition 1

For any TPTG $\mathsf{P}$ satisfying Assumption 1, the games ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ are determined and have optimal strategies for both probabilistic and expected price reachability properties.

Proof

In the case of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$, the result follows from [23] and Assumption 1, i.e. since all clock constraints are closed. Considering ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$, the result follows from the fact that the game has a finite state space and is finitely branching [32].     \sqcap$$\sqcup

Proposition 2

For any strategy profile $\sigma^{\prime}$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$, there exists a strategy profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ such that $\mathbb{P}^{\sigma}(F_{\mathbb{R}})=\mathbb{P}^{\sigma^{\prime}}(F_{\mathbb{N}})$ and $\mathbb{E}^{\sigma}(F_{\mathbb{R}})=\mathbb{E}^{\sigma^{\prime}}(F_{\mathbb{N}})$.

Using the $\epsilon$-digitization approach of TAs [26], which has been extended to PTAs in [38], the following theorem follows, demonstrating the correctness of the digital clocks semantics for probabilistic reachability properties.

Theorem 4.1

For any TPTG $\mathsf{P}$ satisfying Assumption 1, coalition of players $C$ and set of locations $F\subseteq\mathit{L}:$ $\mathbb{P}^{C}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}}(F_{\mathbb{R}})=\mathbb{P}^{C}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}}(F_{\mathbb{N}})$.

For expected price reachability properties, we extend the approach of [38], by first showing that, for any fixed (dense-time) profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and $n\in\mathbb{N}$, there exist profiles of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ whose expected price of reaching the target locations $F$ within $n$ transitions that provide lower and upper bounds for that of $\sigma$.

For $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$, profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{T}}^{C}}$, and finite path $\pi\in\mathit{FPaths}^{\sigma}$ we inductively define the values $\langle\mathbb{E}^{\sigma}_{n}(\pi,F_{\mathbb{T}})\rangle_{n\in\mathbb{N}}$ which equal the expected price, under the profile $\sigma$, of reaching the target $F_{\mathbb{T}}$ after initially performing the path $\pi$ within $n$ steps. To ease presentation we only give the definition for deterministic profiles.

Definition 6

For $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$, strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{T}}^{C}}$ and finite path $\pi$ of the profile let $\mathbb{E}^{\sigma_{1},\sigma_{2}}_{0}(\pi,F_{\mathbb{T}})=0$ and for any $n\in\mathbb{N}$, if $\mathit{last}(\pi){=}(l,v)\in S_{i}$ for $1{\leqslant}i{\leqslant}2$, $\sigma_{i}(\pi){=}(t,a)$ and $\mu=P_{[\![{\mathsf{P}}]\!]_{\mathbb{T}}}((l,v),(t,a))$, then:

[TABLE]

We require the following properties of these expected price reachability properties. These then allow us to prove the correctness of the digital clocks semantics for expected price reachability properties (Theorem 4.2 below).

Lemma 1

For $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$ and profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{T}}^{C}}$, the sequence $\langle\mathbb{E}^{\sigma}_{n}(F_{\mathbb{T}})\rangle_{n\in\mathbb{N}}$ is non-decreasing and converges to $\mathbb{E}^{\sigma}(F_{\mathbb{T}})$, and, for any player 1 strategy $\sigma_{1}$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{T}}^{C}}$, the sequence of functions $\mathbb{E}^{\sigma_{1},\cdot}_{n}(F_{\mathbb{T}}):\Sigma^{2}\rightarrow\mathbb{R}$ converges uniformly. Furthermore, for any player 1 strategy $\sigma_{1}$, the sequence $\langle\inf\nolimits_{\sigma_{2}\in\Sigma^{2}}\mathbb{E}^{\sigma_{1},\sigma_{2}}_{n}(F_{\mathbb{T}})\rangle_{n\in\mathbb{N}}$ is non-decreasing and converges to $\inf\nolimits_{\sigma_{2}\in\Sigma^{2}}\mathbb{E}^{\sigma_{1},\sigma_{2}}(F_{\mathbb{T}})$, and the sequence of functions $\inf\nolimits_{\sigma_{2}\in\Sigma^{2}}\mathbb{E}^{\cdot,\sigma_{2}}_{n}(F_{\mathbb{T}}):\Sigma^{1}\rightarrow\mathbb{R}$ converges uniformly.

Proof

In each case, proving that the sequence is non-decreasing and converges follows from Definition 6. Uniform convergence follows from showing the set of strategies for players is compact and using the fact that the sequences are non-decreasing and converge pointwise [48, Theorem 7.13]. In the case when $\mathbb{T}{=}\mathbb{N}$, compactness follows from the fact the action set is finite, while for $\mathbb{T}{=}\mathbb{R}$ we must restrict to PTAs for which all invariants are bounded (Assumption 1) to ensure the action set is compact.     \sqcap$$\sqcup

Lemma 2

For any strategy profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and $n\in\mathbb{N}$, there exist strategy profiles $\sigma^{\mathit{lb}}$ and $\sigma^{\mathit{ub}}$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ such that: $\mathbb{E}^{\sigma^{\mathit{lb}}}_{n}(F_{\mathbb{N}})\;\leqslant\;\mathbb{E}^{\sigma}_{n}(F_{\mathbb{R}})\;\leqslant\;\mathbb{E}^{\sigma^{\mathit{ub}}}_{n}(F_{\mathbb{N}})$.

Theorem 4.2

For any TPTG $\mathsf{P}$ satisfying Assumption 1, coalition of players $C$ and set of locations $F\subseteq\mathit{L}:$ $\mathbb{E}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}}^{C}(F_{\mathbb{R}})=\mathbb{E}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}}^{C}(F_{\mathbb{N}})$.

Proof

Consider any $n\in\mathbb{N}$. Using Lemma 2 it follows that, for any profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}}$, there exist profiles $\sigma^{\mathit{lb}}{=}(\sigma_{1}^{\mathit{lb}},\sigma_{1}^{\mathit{lb}})$ and $\sigma^{\mathit{ub}}{=}(\sigma_{1}^{\mathit{ub}},\sigma_{1}^{\mathit{ub}})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ such that:

[TABLE]

On the other hand, using the construction in the proof of Proposition 2, for any profile $\sigma^{\prime}{=}(\sigma_{1}^{\prime},\sigma_{2}^{\prime})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}}$, there exists a profile $\sigma{=}(\sigma_{1},\sigma_{1})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ such that:

[TABLE]

Combining these results with Proposition 1 it follows that:

[TABLE]

Since $n\in\mathbb{N}$ was arbitrary, we have:

[TABLE]

and hence using Lemma 1 it follows that:

[TABLE]

The fact that the limit can move inside the $\sup$ and $\inf$ operators on both sides of the inequality follows from the uniform convergence results of Lemma 1.     \sqcap$$\sqcup

5 Case Studies

In this section, we apply our approach to two case studies, a security protocol and a scheduling problem, both of which have been previously modelled as PTAs [38]. In both case studies, by working with games we are able to give more realistic models that overcome the limitations of the earlier PTA models. We specify the finite-state TSG digital clocks semantic models of the case studies using the PRISM language and employ the PRISM-games tool [41] to perform the analysis. Using PRISM-games we are not only able to find optimal probabilistic and expected reachability values, but also synthesise optimal strategies for the players. PRISM files for the case studies are available from [54].

Non-repudiation protocol. Markowitch and Roggeman’s non-repudiation protocol for information transfer [44] is designed to allow an originator $O$ to transfer information to a recipient $R$ while guaranteeing non-repudiation, that is, neither $O$ nor $R$ can deny that they participated in the transfer.

Randomisation is fundamental to the protocol as, in the initialisation step, $O$ randomly selects a positive integer $N$ that is never revealed to $R$ during execution. Timing is also fundamental as, to prevent $R$ potentially gaining an advantage, if $O$ does not receive an acknowledgement within a specific timeout value (denoted $\mathit{AD}$), the protocol is stopped and $O$ states $R$ is trying to cheat. In previous PTA models of the protocol [42, 45] the originator $O$ had fixed behaviour, while the choices of a (malicious) recipient $R$ included varying the delay between receiving a message from $O$ and sending an acknowledgement. By modelling the protocol as a two-player game we can allow both $O$ and $R$ to make choices which can depend on the history, i.e., the previous behaviour of the parties. The game is naturally turn-based since, in each round, first $O$ sends a message after a delay of their choosing and, after receiving this message, $R$ can respond with an acknowledgement after a delay of their choosing.

We first consider an ‘honest’ version of the protocol where both $O$ and $R$ can choose delays for their messages but do follow the protocol (i.e., send messages and acknowledgements before timeouts occur). The component PTA models for $O$ and $R$ are presented in Fig. 2. In the PTA for $O$, the message delay is between $\mathit{md}{=}2$ and $\mathit{MD}{=}9$ time units, while the acknowledgement delay is at least $\mathit{ad}{=}1$ time units and $\mathit{AD}{=}5$ is the timeout value. In addition, the probabilistic choice of $N$ is made using a geometric distribution with parameter $p\in(0,1]$. The parallel composition of these two components then gives the TPTG model of the protocol by assigning control of locations to either $O$ or $R$, based on which party decides on the delay. There is a complication in the location where $O$ is waiting and $R$ is sending an acknowledgement, as the delay before sending the acknowledgement controlled by $R$, while if the timeout is reached $O$ should end the protocol. However, since $O$’s behaviour is deterministic in this location, we assign this location to be under the control of $R$, but add the constraints that an acknowledgement can only be sent before the timeout is reached. If $O$’s behaviour was not deterministic, then a turn-based model would not be sufficient and the protocol would need to be modelled as a concurrent game.

We also consider two ‘malicious’ versions of the protocol, one in which $R$ is allowed to guess which is the last message (malicious version 1) and a version further extended by giving $R$ additional power through a probabilistic decoder that can decode a message with probability $0.25$ before $O$ will timeout (malicious version 2). The TPTG models follow the same structure as that for the ‘honest’ version, requiring that, in the locations where $O$ is waiting for an acknowledgement, once the timeout has been reached the only possible behaviour is for the protocol to terminate and $O$ states $R$ is trying to cheat.

For the ‘honest’ version, Figures 3 and 4 present results when different coalitions try to maximise the probability the protocol terminates successfully by time $T$ when $p{=}0.01$ and $p{=}0.1$ and minimise expected time for successful termination as the parameter $p$ varies. More precisely, we consider the coalition of both players ($\langle\!\langle{O,R}\rangle\!\rangle$), a single player ($\langle\!\langle{O}\rangle\!\rangle$ or $\langle\!\langle{R}\rangle\!\rangle$) and the empty coalition ($\langle\!\langle{}\rangle\!\rangle$). Using a PTA model, only the first and last cases could be considered. As can be seen, both parties have some control over the time it takes for the protocol to complete and $O$ has greater power as it can delay messages longer than $R$ (if $R$ delays too long then $O$ will terminate the protocol stating $R$ is cheating).

In the case of the versions with a malicious recipient, in Figures 5 and 6 we have plotted the maximum probability the recipient gains information by time $T$ for versions 1 and 2 respectively. We have included the cases where $O$ works against $R$ ($\langle\!\langle{R}\rangle\!\rangle$) and where they collaborate ($\langle\!\langle{O,R}\rangle\!\rangle$). As we can see, although $O$ cannot reduce the probability of $R$ obtaining information, it can to some extent increase the time it takes $R$ to obtain this information.

Processor Task Scheduling. This case study is based on the task-graph scheduling problem from [12]. The task-graph is given in Fig. 7 and is for evaluating the expression $D{\times}(C{\times}(A{+}B)){+}((A{+}B){+}(C{\times}D))$ where each multiplication and addition is evaluated on one of two processors, $P_{1}$ and $P_{2}$. The time and energy required to perform these operations is different, with $P_{1}$ being faster than $P_{2}$ while consuming more energy as detailed below.

• •

Time and energy usage of $P_{1}$: $[0,2]$ picoseconds for addition, $[0,3]$ picoseconds multiplication, 10 Watts when idle and 90 Watts when active.

• •

Time and energy usage of $P_{2}$: $[0,5]$ picoseconds for addition, $[0,7]$ picoseconds multiplication, 20 Watts when idle and 30 Watts when active.

A (non-probabilistic) TA model is considered in [12], which is the parallel composition of a TA for each processor and for the scheduler. Previously, in [45], we extended this model by adding probabilistic behaviour to give a PTA. However, the execution time of the processors had to remain fixed since the non-determinism was under the control of the scheduler, and therefore the optimal scheduler would always choose the minimum execution time for each operation. By moving to a TPTG model, we can allow the execution times to be under the control of a separate player (the environment). We further extend the model by allowing the processors $P_{1}$ and $P_{2}$ to have at most $k_{1}$ and $k_{2}$ faults respectively. We assume that the probability of any fault causing a failure is $p$ and faults can happen at any time a processor is active, i.e., the time the faults occur is under the control of the environment. Again, we could not model this extension with a PTA, since the scheduler would then be in control of when the faults occurred, and therefore could decide that no faults would occur.

As explained in [12], an optimal schedule for a game model in which delays can vary does not yield a simple assignment of tasks to processors at specific times as presented in [45] for PTAs, but instead it is an assignment that also has as input when previous tasks were completed and on which processors.

In Fig. 8 we present both the original TA model for processor $P_{1}$, in which the execution time is non-deterministic, and the extended PTA, which allows $k_{1}$ faults and where the probability of a fault causing a failure equals $p$. The PTA includes an integer variable $\mathit{faults}$ and the missing enabling conditions equal $\mathtt{true}$. To specify the automaton for the scheduler and ensure that we can then build a turn-based game, we restrict the scheduler so that it decides what tasks to schedule initially and immediately after a task ends, then passes control to the environment, which decides the time for the next active task to end.

In Fig. 9 we have plotted both the optimal expected time and energy when there are different number of faults in each processor as the parameter $p$ (the probability of a fault causing a failure) varies. As would be expected, both the optimal expected time and energy consumption increases both as the number of faults increases and the probability that a fault causes a failure increases.

Considering the synthesised optimal schedulers for the expected time case, when $k_{1}{=}k_{2}{=}1$ and $p{=}1$, the optimal approach is to just use the faster processor $P_{1}$ and the expected time equals $18.0$. The optimal strategy for the environment, i.e., the choices that yield the worst-case expected time, against this scheduler is to delay all tasks as long as possible and cause a fault when a multiplication task is just about to complete on $P_{1}$ (recall $P_{2}$ is never used under the optimal scheduler). A multiplication is chosen as this takes longer (3 picoseconds) than an addition task (2 picoseconds). These choices can be seen through the fact that $18.0$ is the time for 4 multiplications and 3 additions to be performed on $P_{1}$, while the problem requires 3 multiplications and 3 additions. As soon as the probability of a fault causing a failure is less than 1, the optimal scheduler does use processor $P_{2}$ from the beginning by initially scheduling $\mathit{task}_{1}$ on process $P_{1}$ and $\mathit{task}_{2}$ on processor $P_{2}$ (which is also optimal when no faults can occur).

In the case of the expected energy consumption, the optimal scheduler uses both processes unless one has 2 or more faults than the other and there is only a small chance that a fault will cause a failure. For example, if $P_{1}$ has 3 faults and $P_{2}$ has 1 fault, then $P_{1}$ is only used by the optimal scheduler when the probability of a failure causing a fault is approximately $0.25$ or less.

6 Conclusions

We have introduced turn-based probabilistic timed games and shown that digital clocks are sufficient for analysing a large class of such games and performance properties. We have demonstrated the feasibility of the approach through two case studies. However, there are limitations of the method since, in particular, as for PTAs [38], the digital clocks semantics does not preserve stopwatch properties or general (nested) temporal logic specifications.

We are investigating extending the approach to concurrent probabilistic timed games. However, since such games are not determined for expected reachability properties [24], this is not straightforward. One direction is to find a class of games which are determined. If we are able to find such a class, then the extension of PRISM-games to concurrent stochastic games [36] could be used to verify this class. Work on finite-state concurrent stochastic games has recently been extended to the case when players have distinct objectives [37] and considering such objectives in the real-time case is also a direction of future research.

Another direction of future research is to formulate a zone-based approach for verifying probabilistic timed games. For the case of probabilistic reachability, this appears possible through the approach of [33] for PTAs. However, it is less clear that the techniques for expected time [29] and expected prices [35], and temporal logic specifications [40] for PTAs, can be extended to TPTGs. Finally, we mention that, although the PRISM language models used in Section 5 were built by hand, in future we plan to automate this procedure, extending the one already implemented in PRISM [34] for PTAs.

Acknowledgements. This work is partially supported by the EPSRC Programme Grant on Mobile Autonomy and the PRINCESS project, under the DARPA BRASS programme (contract FA8750-16-C-0045).

Appendix 0.A Proofs from Section 4

In this appendix we include the details omitted from Section 4 as they closely follow those for PTAs presented in [38]. As in Section 4, we fix a TPTG $\mathsf{P}$, coalition of players $C$ and target set of locations $F\in\mathit{L}$, and let $F_{\mathbb{T}}=\{(l,v)\in F{\times}\mathbb{T}^{\mathcal{X}}\mid v{\,\models\,}\mathit{inv}(l)\}$ be the target of game ${[\![{\mathsf{P}}]\!]_{\mathbb{T}}}$ for $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$.

We first prove Proposition 2, i.e. that for any strategy profile of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ there is a corresponding strategy profile of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$.

Proof (of Proposition 2)

Consider any strategy profile $\sigma^{\prime}{=}(\sigma_{1}^{\prime},\sigma_{2}^{\prime})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$. We can construction the strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ where the strategies $\sigma_{1}$ and $\sigma_{2}$ make the same choices as those of $\sigma_{1}^{\prime}$ and $\sigma_{2}^{\prime}$ respectively. The only difference is in the states reached as values of a clocks in ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}}$ are not bounded. It then follows that $\mathbb{P}^{\sigma}(F_{\mathbb{R}})=\mathbb{P}^{\sigma^{\prime}}(F_{\mathbb{N}})$ and $\mathbb{E}^{\sigma}(F_{\mathbb{R}})=\mathbb{E}^{\sigma^{\prime}}(F_{\mathbb{N}})$ as required.     \sqcap$$\sqcup

We now presenting definitions and results for PTAs [45] and TAs [25, 26] used in proving the correctness of the digital clocks semantics.

Definition 7

For any $t\in\mathbb{R}$ and $\varepsilon\in[0,1]$ let:

[TABLE]

Lemma 3

For any $t,t^{\prime}\in\mathbb{R}$, $c\in\mathbb{N}$ and $\sim\in\{\leqslant,=,\geqslant\}$, if $t-t^{\prime}\sim c$ then $[t]_{\varepsilon}-[t^{\prime}]_{\varepsilon}\sim c$ for all $\varepsilon\in[0,1]$.

Definition 8

For any infinite path $s_{0}\xrightarrow{t_{0},a_{0}}s_{1}\xrightarrow{t_{1},a_{1}}\cdots$ of ${[\![{{\sf P}}]\!]_{\mathbb{T}}}$, the accumulated duration up to the $(n{+}1)$th state of $\pi$ is defined by $\mathit{dur}(\pi,n)=\sum_{i=0}^{n-1}t_{i}$.

Lemma 4

For any path $\pi=(l_{0},v_{0})\xrightarrow{t_{0},a_{0}}(l_{1},v_{1})\xrightarrow{t_{1},a_{1}}\cdots$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$, $x\in{\mathcal{X}}$ and $i\in\mathbb{N}$, there exists $j\leqslant i$ such that $v_{i}(x)=\mathit{dur}(\pi,i)-\mathit{dur}(\pi,j)$.

Definition 9

For any (finite or infinite) path $\pi=(\bar{l},\mathbf{0})\xrightarrow{t_{0},a_{0}}(l_{1},v_{1})\xrightarrow{t_{1},a_{1}}\cdots$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$, its $\varepsilon$-digitization is the path

[TABLE]

of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ where for any $i\in\mathbb{N}$ and $x\in{\mathcal{X}}:$

• •

$[v_{i}]_{\varepsilon}(x)=\min([\mathit{dur}(\pi,i)]_{\varepsilon}-[\mathit{dur}(\pi,j)]_{\varepsilon},k_{x}+1)$ and $j\leqslant i$ such that $v_{i}(x)=\mathit{dur}(\pi,i)-\mathit{dur}(\pi,j)$ which exists by Lemma 4;

• •

$t_{i}^{\prime}=[\mathit{dur}(\pi,i{+}1)]_{\varepsilon}-[\mathit{dur}(\pi,i)]_{\varepsilon}$.

The correctness of this construction is dependent on the clock constraints appearing in $\mathsf{P}$ being closed and diagonal-free (Assumption 1).

We next extend the notion of digitization to strategy profiles of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$. Following [38], to achieve this we define the digitization of sets of paths, i.e. for a set of paths $\Pi$, we let $[\Pi]_{\varepsilon}\,\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\{[\pi]_{\varepsilon}\mid\pi\in\Pi\}$. When considering a strategy profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$, we assume the domain of the mapping $[\cdot]_{\varepsilon}$ is restricted to the sets of paths $\mathit{IPaths}^{\sigma}$ and $\mathit{FPaths}^{\sigma}$. Furthermore, for any set of finite paths $\Pi\subseteq\mathit{FPaths}^{\sigma}$ let:

[TABLE]

and for any finite path $\pi\in\mathit{FPaths}^{\sigma}$, $1{\leqslant}i{\leqslant}2$ and $(t,a)\in A(\mathit{last}(\pi))$ let:

[TABLE]

Definition 10

For any strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and $\varepsilon\in[0,1]$ its $\varepsilon$-digitization strategy profile $\sigma^{\varepsilon}{=}(\sigma_{1}^{\varepsilon},\sigma_{2}^{\varepsilon})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ is defined as follows. For any finite path $\pi$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ and $1{\leqslant}i{\leqslant}2$ such that $\mathit{last}(\pi)\in S_{i}:$

• •

if $[\pi]_{\varepsilon}^{-1}$ is non-empty, then for any $(t,a)\in A(\mathit{last}(\pi))$, then the probability of $\sigma_{i}^{\varepsilon}$ choosing $(t,a)$ after $\pi$ has been performed is given by

[TABLE]

• •

if $[\pi]_{\varepsilon}^{-1}$ is the empty set, then let $\sigma_{i}^{\varepsilon}$ choose an arbitrary element of $A(\mathit{last}(\pi))$.

We next show how probability measures of strategy profiles change under $\varepsilon$-digitization.

Proposition 3

For any strategy profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and $\varepsilon\in[0,1]$, we have ${\mathit{Prob}}^{\sigma^{\varepsilon}}(\Omega)={\mathit{Prob}}^{\sigma}([\Omega]_{\varepsilon}^{-1})$ for all elements $\Omega$ of the $\sigma$-algebra of the probability measure ${\mathit{Prob}}^{\sigma^{\varepsilon}}$.

Proof

Consider any strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and $\varepsilon\in[0,1]$. Using Definition 10 we can build the strategy profile $\sigma^{\varepsilon}{=}(\sigma^{\varepsilon}_{1},\sigma^{\varepsilon}_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$. Now, from the construction of ${\mathit{Prob}}^{\sigma^{\varepsilon}}$, see [31], it is sufficient to show that:

[TABLE]

which we prove by induction on the length of $\pi$. Therefore, consider any path $\pi\in\mathit{IPaths}^{\sigma^{\varepsilon}}$. If $|\pi|{=}0$, then $\pi{=}{\bar{s}}$ and ${\mathit{Prob}}^{\sigma^{\varepsilon}}(\pi)=1={\mathit{Prob}}^{\sigma}([\pi]_{\varepsilon}^{-1})$ as required.

Next, suppose $|\pi|{=}n{+}1$ and by induction the lemma holds for all paths of length $n$. Now, $\pi$ is of the form $\pi^{\prime}\xrightarrow{t,a}s^{\prime}$ for some path $\pi^{\prime}$ of length $n$, $(t,a)\in A(\mathit{last}(\pi^{\prime}))$ and $s^{\prime}\in S$. Now $\mathit{last}(\pi^{\prime})\in S_{i}$ for some $1{\leqslant}i{\leqslant}2$, and therefore by construction of ${\mathit{Prob}}^{\sigma^{\varepsilon}}$ supposing $\delta(\mathit{last}(\pi^{\prime}),(t,a))=\mu$:

[TABLE]

and hence (1) holds by induction.     \sqcap$$\sqcup

We are now in a position to prove Theorem 4.1, i.e.  $\mathbb{P}_{[\![{\mathsf{P}}]\!]_{\mathbb{R}}}^{C}(F_{\mathbb{R}})=\mathbb{P}_{[\![{\mathsf{P}}]\!]_{\mathbb{N}}}^{C}(F_{\mathbb{N}})$.

Proof (of Theorem 4.1)

Consider any TPTG $\mathsf{P}$ satisfying Assumption 1, coalition of players $C$ and set of locations $F\subseteq\mathit{L}$. From Definition 9, we have that:

[TABLE]

Now for any strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$, by definition of $\mathbb{P}^{\sigma}(F_{\mathbb{R}})$:

[TABLE]

for some strategy profile $\sigma^{\prime}{=}(\sigma_{1}^{\prime},\sigma_{2}^{\prime})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ using Proposition 3. Combining (3) with (2) it follows that:

[TABLE]

Since the player 2 strategy $\sigma_{2}$ was arbitrary it follows that:

[TABLE]

Following dual arguments and using Proposition 2 we have:

[TABLE]

and therefore:

[TABLE]

We can now apply similar arguments again to yield:

[TABLE]

as required.     \sqcap$$\sqcup

To give the proof of Lemma 2, we first require the following results from linear programming.

Definition 11

A matrix $\mathbf{A}$ is totally unimodular if each subdeterminant of $\mathbf{A}$ is [math], $+1$ or $-1$.

Theorem 0.A.1 ([50] Theorem 19.3)

Let $\mathbf{A}$ be a matrix with entries [math], $+1$ and $-1$. Then the following are equivalent:

$\mathbf{A}$* is totally unimodular;* 2. 2.

each collection of columns of $\mathbf{A}$ can be split into two parts so that the sum of the columns in one part minus the sum of the columns in the other part is a vector with entries only [math], $+1$ and $-1$.

Theorem 0.A.2 ([50] Corollary 19.1.a)

Let $\mathbf{A}$ be a totally unimodular matrix, and let $\mathbf{b}$ and $\mathbf{c}$ be integral vectors. Then both problems in the linear programming duality equation:

[TABLE]

have integral optimum solutions.

We also require a variant of Definition 6 which considers only action prices.

Definition 12

For $\mathbb{T}\in\{\mathbb{R},\mathbb{N}\}$, strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{T}}^{C}}$ and finite path $\pi$ of the profile let $\mathbb{A}^{\sigma_{1},\sigma_{2}}_{0}(\pi,F_{\mathbb{T}})=0$ and for any $n\in\mathbb{N}$, if $\mathit{last}(\pi){=}(l,v)\in S_{i}$ for $1{\leqslant}i{\leqslant}2$, $\sigma_{i}(\pi){=}(t,a)$ and $\mu=P_{[\![{\mathsf{P}}]\!]_{\mathbb{T}}}((l,v),(t,a))$, then:

[TABLE]

We are now in a position to prove Lemma 2, i.e. for any strategy profile $\sigma$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ and $n\in\mathbb{N}$, there exist strategy profiles $\sigma^{\mathit{lb}}$ and $\sigma^{\mathit{ub}}$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ such that:

[TABLE]

Proof (of Lemma 2)

Consider any strategy profile $\sigma{=}(\sigma_{1},\sigma_{2})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$. The first part of the proof involves constructing a set of constraints on the time steps of the strategy profiles that follow the same action choices as $\sigma$ up until the $n$th step. Using these constraints we then formulate a linear programming problem, whose objective is either to maximise or minimise the expected price of reaching a set of target states within $n$ steps. The result then follows from showing that there exist integer solutions which achieve the maximum and minimum values. Below, we consider only the construction of the strategy profile $\sigma^{\mathit{ub}}{=}(\sigma_{1}^{\mathit{ub}},\sigma_{2}^{\mathit{ub}})$ as the construction of the profile $\sigma_{1}^{\mathit{lb}}$ follows similarly.

We begin by constructing a set of linear constraints from which we can derive a set of strategy profiles that make the same choices as $\sigma_{1}$. More precisely, we consider any sequence of real values $\mathbf{t}=\langle t_{\pi}\rangle_{\pi\in\mathit{FPaths}^{\sigma}}$ which satisfy, for any $\pi\in\mathit{FPaths}^{\sigma}$, the following constraints:

• •

if $|\pi|=0$, then

[TABLE]

• •

if $|\pi|>0$, then

[TABLE]

Sequences of values which satisfy these constraints include letting $t_{\pi}$ equal $\mathit{dur}(\pi,|\pi|)$ or $[\mathit{dur}(\pi,|\pi|)]_{\varepsilon}$ for any $\varepsilon\in[0,1]$.

Now suppose that we fix a sequence of real values $\mathbf{t}$ which satisfy the above constraints. From these values we can construct the choices of a strategy profile $(\sigma_{1}^{\mathbf{t}},\sigma_{2}^{\mathbf{t}})$ which match the action choices of the profile $\sigma$, although the durations may differ. The set of finite paths of the profile $(\sigma_{1}^{\mathbf{t}},\sigma_{2}^{\mathbf{t}})$ when starting from the initial state is given by $\{[\pi]_{\mathbf{t}}\mid\pi\in\mathit{FPaths}^{\sigma_{1},\sigma_{2}}\}$, which we define inductively as follows:

• •

if $\pi=(\overline{l},\mathbf{0})$, then $[\pi]_{\mathbf{t}}=\pi$;

• •

if $\pi$ is of the form $\pi^{\prime}\xrightarrow{t,a}(l,v)$, then:

[TABLE]

where $t^{\prime}=t_{\pi}-t_{\pi^{\prime}}$ and for any clock $x$ we have $v^{\prime}(x)=t_{\pi}-t_{\pi^{(j)}}$ for $j\leqslant|\pi|$ such that $v(x)=\mathit{dur}(\pi,|\pi|)-\mathit{dur}(\pi,j)$, which exists by Lemma 4.

The construction all finite paths of the profile $(\sigma_{1}^{\mathbf{t}},\sigma_{2}^{\mathbf{t}})$ yields also the choices made by the profile and by construction the action choices match those of the profile $\sigma$ although the durations may differ. The fact that these choices are valid choices of ${[\![{\mathsf{P}}]\!]_{\mathbb{R}}^{C}}$ follows from Lemma 4, equations (4a)–(4d) and since we restrict attention to closed, diagonal-free probabilistic timed games (Assumption 1).

For any state $(l,v)\in S$, to simplify the presentation let ${r}_{L}(l,v)={r}_{L}(l)$. Now, from the construction of the choices of $(\sigma_{1}^{\mathbf{t}},\sigma_{2}^{\mathbf{t}})$ and Definition 6 and Definition 12, it follows that $\mathbb{E}^{\sigma_{1}^{\mathbf{t}},\sigma_{2}^{\mathbf{t}}}_{n}(F_{\mathbb{R}})$ equals:

[TABLE]

since the action choices of $\sigma$ and $(\sigma_{1}^{\mathbf{t}},\sigma_{2}^{\mathbf{t}})$ are the same.

Now suppose we fix some $n\in\mathbb{N}$ and consider the following linear programming problem over the variables $\langle t_{\pi}\rangle_{\pi\in\mathit{FPaths}^{\sigma}_{n}}$, where $\mathit{FPaths}^{\sigma}_{n}$ is subset of paths of $\mathit{FPaths}^{\sigma}$ with length at most $n$: maximise (5) such that the constraints of (4a)–(4d) are satisfied. From Assumption 1 we have that all probabilities are rational, and therefore we can scale the objective function such that it contains only integer values. Furthermore, from the construction of the constraints the corresponding matrix is totally unimodular (using Theorem 0.A.1 and the fact that, for any collection of columns of the constraint matrix, the sum of the columns is a vector with entries only [math], $+1$ and $-1$). Therefore, using Theorem 0.A.2, it follows that the maximum solution is achieved by an integer vector. More precisely, there exists a strategy profile $\sigma^{\mathit{ub}}{=}(\sigma_{1}^{\mathit{ub}},\sigma_{2}^{\mathit{ub}})$ of ${[\![{\mathsf{P}}]\!]_{\mathbb{N}}^{C}}$ such that $\mathbb{E}^{\sigma}_{n}(F_{\mathbb{R}})\leqslant\mathbb{E}^{\sigma^{\mathit{ub}}}_{n}(F_{\mathbb{N}})$ as required.     \sqcap$$\sqcup