Characterising Probabilistic Alternating Simulation for Concurrent Games

TL;DR

This paper introduces a new logical framework for characterising probabilistic alternating simulation in concurrent games, providing a sound and complete modal logic that captures the behavior of probabilistic game structures.

Contribution

It proposes a novel probabilistic distribution-based logic with fixpoints that fully characterises probabilistic alternating simulation, advancing theoretical understanding.

Findings

Sound and complete modal characterisation of probabilistic alternating simulation

A new logic based on probabilistic distributions for concurrent games

Extension with fixpoints captures a wide range of properties

Abstract

Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the behaviour of different probabilistic game structures. In this paper, we present a sound and complete modal characterisation of this simulation relation by proposing a new logic based on probabilistic distributions. The logic enables a player to enforce a property in the next state or distribution. Its extension with fixpoints, which also characterises the simulation relation, can express a lot of interesting properties in practical applications.

Equations

$$\phi ::=p\mid \neg p\mid \underset{i\in I}{\bigwedge }{\phi }_i\mid \underset{i\in I}{\bigvee }{\phi }_i\mid ⟨⟨\mathcal{I}⟩⟩\phi \mid \underset{j\in J}{⨁}{p}_j{\phi }_j\mid \underset{j\in J}{⨁}{\phi }_j$$

$$\nu X.(\mu Y.\mathsf{cashin}\vee ⟨⟨investor⟩⟩Y)\wedge ⟨⟨investor⟩⟩X).$$

$$\mu Z.(\mathsf{cashin}\wedge [\alpha ,\mathsf{profit}]\oplus [1-\alpha ,\top ])\vee ⟨⟨investor⟩⟩Z$$

Full text

1 Introduction

Simulation relations and bisimulation relations [21] are important research topics in concurrency theory. In the classical model of labelled transition systems (LTS), simulation and bisimulation have been proved useful for comparing the behaviour of concurrent systems. The modal characterisation problem has been studied both in classical and in probabilistic systems, i.e., the Hennessy-Milner logic (HML) [11] that characterises image-finite LTS, and various modal logics have been proposed to characterise strong and weak probabilistic (bi)simulation in the model of probabilistic automata [22, 9, 12]. To study multi-player games, the concurrent game structure (GS) [1] is a model that defines a system that evolves while interacting with outside players. As a player’s behaviour is not fully specified within a system, GS are often also known as open systems. Alternating simulation (A-simulation) is defined in GS focusing on players ability to enforce temporal properties specified in alternating-time temporal logic (ATL) [1], and A-simulation is shown to be sound and complete to a fragment of ATL [2].

In this paper, we work on the model of probabilistic game structure (PGS) which has probabilistic transitions. PGS also allows probabilistic (or mixed) choices of players. In this setting, we assume all players have complete information about system states. The simulation relation in PGS, called probabilistic alternating simulation (PA-simulation), has been shown to preserve a fragment of probabilistic alternating-time temporal logic (PATL) under mixed strategies [30]. Given the classical results of modal characterisations for (non-probabilistic) LTS, probabilistic automata, as well as for (non-probabilistic) game structures, we investigate if similar correspondence exists for processes and modal logics in the domain of concurrent games with probabilistic transitions and mixed strategies. We find that such a correspondence still holds by adapting a modal logic with nondeterministic distributions extended from the work of [9]. As a by-product, we extend that modal logic with fixpoint operators and study its expressiveness power. Notably, similar to the fixpoint logics in [18, 27], the least fixpoint modality in our logic only expresses finite reachability, a property in line with the original $\mu$-calculus [15], which somehow in the probabilistic setting may not be powerful enough to express certain reachability properties that require infinite accumulation of moves in a play.

Contributions. This paper studies modal characterisation of the probabilistic alternation simulation relation in probabilistic concurrent game structures, which defines a novel modal logic based on probabilistic distributions. This new logic expresses a player’s power to enforce a property in the next state or distribution. The logic also incorporates both probabilistic and nondeterminstic features that need to be considered during the two-player interplay. The second contribution is the introduction of a fixpoint logic, which also characterises the simulation relation, extended from that modal logic. The expressive power of the logic has been illustrated by examples.

2 Preliminaries

A discrete probabilistic distribution $\Delta$ over a set $S$ is a function of type $S\rightarrow[0,1]$, where $\sum_{s\in S}\Delta(s)=1$. We write $\mathcal{D}(S)$ for the set of all such distributions, ranged over by symbols $\Delta,\Theta,\dots$. Given a set $T\subseteq S$, $\Delta(T)=\sum_{s\in T}\Delta(s)$, i.e., the probability for the given set $T$. Given an index set $I$, a list of distributions $\langle\Delta_{i}\rangle_{i\in I}$ and a list of values $\langle p_{i}\rangle_{i\in I}$ where $p_{i}\in[0,1]$ for all $i\in I$ and $\sum_{i\in I}p_{i}=1$, we have that $\sum_{i\in I}p_{i}\Delta_{i}$ is also a distribution. If $|I|=2$ we may also write $\Delta_{1}\oplus_{\alpha}\Delta_{2}$ for the distribution $p_{1}\Delta_{1}+p_{2}\Delta_{2}$ where $p_{1}=\alpha$ and $p_{2}=1-\alpha$. For $s\in S$, $\widetilde{s}$ represents a point (or Dirac) distribution satisfying $\widetilde{s}(s)=1$ and $\widetilde{s}(t)=0$ for all $t\neq s$. Given $\Delta\in\mathcal{D}(S)$, we define $\lceil\Delta\rceil$ as the set $\{s\in S\mid\Delta(s)>0\}$, which is the support of $\Delta$.

We work on a model called probabilistic (concurrent) game structure (PGS) with two players ${\cal I}$ and ${\cal{I\!I}}$ (though we believe our results can be straightforwardly extended to handle a finite set of players as in the standard concurrent game structures [1]). Each player has complete information about the PGS at any time during a play. Let Prop be a finite set of propositions.

Definition 2.1**.**

A probabilistic game structure (PGS) $\mathcal{G}$ is a tuple $\langle S,s_{0},L,\texttt{Act},$, where

• •

$S$* is a finite set of states, with $s_{0}$ the initial state;*

• •

$L:S\rightarrow 2^{\texttt{Prop}}$* is the labelling function which assigns to each state $s\in S$ a set of propositions true in $s$;*

• •

$\texttt{Act}=\texttt{Act}_{\cal I}\times\texttt{Act}_{\cal{I\!I}}$* is a finite set of joint actions, where $\texttt{Act}_{\cal I}$ and $\texttt{Act}_{\cal{I\!I}}$ are, respectively, the sets of actions for players ${\cal I}$ and ${\cal{I\!I}}$;*

• •

is a transition function.

If in state $s$ player ${\cal I}$ performs action $a_{1}$ and player ${\cal{I\!I}}$ performs action $a_{2}$, then is the distribution for the next states. During each step the players choose their next moves simultaneously.

Example 2.5**.**

Figure 1 presents the PGS of two players repeatedly playing the rock-paper-scissors game.111A similar example was used in [16]. A concurrent stochastic structure (CSG), as defined in [16], in a PGS, in the sense that all the probability distributions involved in the CSG are point distributions. It has three states $s_{0}$, $s_{1}$, and $s_{2}$, with $s_{0}$ being the initial state. Each state is labelled with an atomic proposition indicating the result of a round of the game (which payer wins or there is a draw). For instance, in state $s_{1}$ player ${\cal I}$ wins the game. Actions of the players are $r$ (representing playing rock), $p$ (representing playing paper), $s$ (representing playing scissors). The joint actions $\langle a_{1},a_{2}\rangle$ with $a_{1},a_{2}\in\{r,p,s\}$ are depicted along with the transitions. The function describes the transitions from state $s$ and state $s^{\prime}$ as shown in Figure 1. The winning states $s_{1}$ and $s_{2}$ are absorbing, i.e., all actions from there make self-transitions, and the game effectively terminates there.

We define a mixed action of player $i$ as a function from states to distributions on $\texttt{Act}_{i}$, ranged over by $\pi,\pi_{1},\sigma\dots$, and write $\Pi_{i}$ for the set of mixed actions from player $i$. In particular, $\widetilde{a}$ is a deterministic mixed action which always chooses $a$ with probability $1$ in all states.

Example 2.7**.**

In the rock-paper-scissors game (see Figure 1), the mixed action with probability $\frac{1}{3}$ for each of the actions ($r$, $p$ and $s$) is known as the optimal strategy for both players.

We generalise the transition function by $\widetilde{}$ to handle mixed actions. Given $\pi_{1}\in\Pi_{\cal I}$ and $\pi_{2}\in\Pi_{\cal{I\!I}}$, for all $s,t\in S$, we have $\widetilde{}(s,\langle\pi_{1},\pi_{2}\rangle)(t)=\sum_{a_{1}\in\texttt{Act}_{\cal I},a_{2}\in\texttt{Act}_{\cal{I\!I}}}\pi_{1}(s)(a_{1})\cdot\pi_{2}(s)(a_{2})\cdot$. We further extend the function $\widetilde{}$ to handle transitions from distributions to distributions. Formally, given a distribution $\Delta$, $\pi_{1}\in\Pi_{\cal I}$ and $\pi_{2}\in\Pi_{\cal{I\!I}}$, for all $s\in S$, we have $\widetilde{}(\Delta,\langle\pi_{1},\pi_{2}\rangle)(s)=\sum_{t\in\lceil\Delta\rceil}\Delta(t)\cdot\widetilde{}(t,\langle\pi_{1},\pi_{2}\rangle)(s)$. For better readability, sometimes we write $\Delta\xrightarrow{\pi_{1},\pi_{2}}\Theta$ if $\Theta=\widetilde{}(\Delta,\langle\pi_{1},\pi_{2}\rangle)$.

Let $\leq\ \subseteq S\times S$ be a partial order, define $\leq_{Sm}\subseteq\mathcal{P}(S)\times\mathcal{P}(S)$, by $P\leq_{Sm}Q$ if for all $t\in Q$ there exists $s\in P$ such that $s\leq t$. In the literature this definition is known as the ‘Smyth order’ [26, 14] regarding ‘$\leq$’.

Relations in probabilistic systems usually require a notion of lifting [13], which extends the relations to the domain of distributions.222In a probabilistic system without explicit user interactions, state $s$ is simulated by state $t$ if for every $s\stackrel{{\scriptstyle a}}{{\rightarrow}}\Delta_{1}$ there exists $t\stackrel{{\scriptstyle a}}{{\rightarrow}}\Delta_{2}$ such that $\Delta_{1}$ is simulated by $\Delta_{2}$. Let $S$, $T$ be two sets and $\mathcal{R}\subseteq S\times T$ be a relation, then $\overline{\mathcal{R}}\subseteq\mathcal{D}(S)\times\mathcal{D}(T)$ is a lifted relation defined by $\Delta\,\overline{\mathcal{R}}\,\Theta$ if there exists a weight function $w:S\times T\rightarrow[0,1]$ such that

• •

$\sum_{t\in T}w(s,t)=\Delta(s)$ for all $s\in S$,

• •

$\sum_{s\in S}w(s,t)=\Theta(t)$ for all $t\in T$,

• •

$s\mathcal{R}\,t$ for all $s\in S$ and $t\in T$ with $w(s,t)>0$.

The intuition behind the lifting is that each state in the support of one distribution may correspond to a number of states in the support of the other distribution, and vice versa. In the following section, we extend the notion of alternating simulation [2] to a probabilistic setting in the way of lifting. The next example is taken from [24] which shows how to lift a relation.

Example 2.16**.**

*In Figure 2, we have two sets of states $S=\{s_{1},s_{2}\}$ and $T=\{t_{1},t_{2},t_{3}\}$, and a relation $\mathcal{R}=\{(s_{1},t_{1}),(s_{1},t_{2}),(s_{2},t_{2}),(s_{2},t_{3})\}$. Suppose $\Delta(s_{1})=\Delta(s_{2})=\frac{1}{2}$ and $\Theta(t_{1})=\Theta(t_{2})=\Theta(t_{3})=\frac{1}{3}$, we may establish $\Delta\,\overline{\mathcal{R}}\,\Theta$. To check this, we define a weight function $w$ by: $w(s_{1},t_{1})=\frac{1}{3}$, $w(s_{1},t_{2})=w(s_{2},t_{2})=\frac{1}{6}$, and $w(s_{2},t_{3})=\frac{1}{3}$. The dotted lines in the graph indicate the allocation of weights that is required to relate $\Delta$ to $\Theta$ via $\overline{\mathcal{R}}$. *

We present some properties of lifted relations. First we show that, by combining distributions that are lift-related with the same weight on both sides, we get the resulting distributions lift-related.

Lemma 2.17**.**

Let $\mathcal{R}\subseteq S\times S^{\prime}$ and $\langle p_{i}\rangle_{i\in I}$ be a list of values satisfying $\sum_{i\in I}p_{i}=1$, and $\Delta_{i}\,\overline{\mathcal{R}}\,\Delta^{\prime}_{i}$ for $\Delta_{i}\in\mathcal{D}(S)$ and $\Delta_{i}^{\prime}\in\mathcal{D}(S^{\prime})$ for all $i$, then $\sum_{i\in I}p_{i}\Delta_{i}\,\overline{\mathcal{R}}\,\sum_{i\in I}p_{i}\Delta^{\prime}_{i}$.

The following lemma states that, given two related distributions, if we split a distribution on one side, then there exists a split on the other side to get a one-to-one matching with respect to the lifted relation.

Lemma 2.18**.**

Let $\Delta\in\mathcal{D}(S)$, $\Delta^{\prime}\in\mathcal{D}(S^{\prime})$, $\mathcal{R}\subseteq S\times S^{\prime}$, $\langle p_{i}\rangle_{i\in I}$ be a list of values satisfying $\sum_{i\in I}p_{i}=1$. If $\Delta\,\overline{\mathcal{R}}\,\Delta^{\prime}$, then

for all lists of distributions $\langle\Delta_{i}\rangle_{i\in I}$ with $\Delta_{i}\in\mathcal{D}(S)$ for all $i\in I$, satisfying $\Delta=\sum_{i\in I}p_{i}\Delta_{i}$, there exists $\langle\Delta_{i}^{\prime}\rangle_{i\in I}$ with $\Delta_{i}^{\prime}\in\mathcal{D}(S^{\prime})$ such that $\Delta^{\prime}=\sum_{i\in I}p_{i}\Delta_{i}^{\prime}$ and $\Delta_{i}\,\overline{\mathcal{R}}\,\Delta_{i}^{\prime}$ for all $i\in I$; 2. 2.

for all lists of distributions $\langle\Delta_{i}^{\prime}\rangle_{i\in I}$ with $\Delta_{i}^{\prime}\in\mathcal{D}(S^{\prime})$ for all $i\in I$, satisfying $\Delta^{\prime}=\sum_{i\in I}p_{i}\Delta_{i}^{\prime}$, there exists $\langle\Delta_{i}\rangle_{i\in I}$ with $\Delta_{i}\in\mathcal{D}(S)$ such that $\Delta=\sum_{i\in I}p_{i}\Delta_{i}$, and $\Delta_{i}\,\overline{\mathcal{R}}\,\Delta_{i}^{\prime}$ for all $i\in I$.

3 Probabilistic Alternating Simulation

In concurrency models, simulation is used to relate states with respect to their behaviours. For example, in a labelled transition system (LTS) $\langle S,A,\rightarrow\rangle$, where $S$ is a set of states, $A$ is a set of actions and $\rightarrow\ \subseteq S\times A\times S$ is the transition relation, we say state $s$ is simulated by state $t$, written $s\leq t$, if for every $s\stackrel{{\scriptstyle a}}{{\rightarrow}}s^{\prime}$ there exists $t\stackrel{{\scriptstyle a}}{{\rightarrow}}t^{\prime}$ such that $s^{\prime}\leq t^{\prime}$. In this coinductive definition, state $t$ is able to simulate state $s$ by performing the same action $a$, with their destination states still related. Simulation is a useful tool in abstraction and refinement based verification, as informally, in the above case, $t$ contains at least as much behaviour as $s$ does. If the relation ‘$\leq$’ is symmetric, then it is also a bisimulation.

In two-player non-probabilistic game structures (GS), alternating simulation (A-simulation) is used to describe a player’s ability to enforce certain temporal requirements (regardless of the other player’s behaviours) [2]. In this paper we only focus on the ability of player ${\cal I}$ in a two-player game. Since in a game structure a transition requires the participation of both parties, fixing player ${\cal I}$’s input leaves a set of possible next states depending on player ${\cal{I\!I}}$’s inputs. A-simulation is defined in the model of non-probabilistic game structures $\langle S,s_{0},\texttt{Act},L,$, which has a set of states $S$ with $s_{0}\in S$ the initial state, $\texttt{Act}=\texttt{Act}_{\cal I}\times\texttt{Act}_{\cal{I\!I}}$ the set of actions from players ${\cal I}$ and ${\cal{I\!I}}$, $L$ the labelling function and the transition function. An A-simulation $\leq^{A}\subseteq S\times S$ is defined as follows. Let $s,t\in S$, $s$ is A-simulated by $t$, i.e., $s\leq^{A}t$, if

• •

$L(s)=L(t)$, and

• •

for all $a\in\texttt{Act}_{\cal I}$ there exists $a^{\prime}\in\texttt{Act}_{\cal I}$ such that , where is the “curried” transition function defined by $\{t\in S\mid\exists b\in\texttt{Act}_{\cal{I\!I}}:$.

Intuitively, on state $t$ action $a^{\prime}$ enforces a more restrictive set than action $a$ enforces on state $s$, as shown by the Smyth-ordered relation $\leq^{A}_{Sm}$: for every $b^{\prime}\in\texttt{Act}_{\cal{I\!I}}$ there exists $b\in\texttt{Act}_{\cal{I\!I}}$ such that .

Zhang and Pang extend A-simulation to probabilistic alternating simulation (PA-simulation) in PGS [30]. Their definition requires lifting of the simulation relation to derive a relation on distributions of states.

Definition 3.9**.**

Given a PGS $\langle S,s_{0},L,\texttt{Act},$, a probabilistic alternating simulation (PA-simulation) is a relation $\sqsubseteq\ \subseteq S\times S$ such that $s\sqsubseteq t$ if

• •

$L(s)=L(t)$, and

• •

for all $\pi_{1}\in\Pi_{\cal I}$, there exists $\pi_{2}\in\Pi_{\cal I}$, such that $\widetilde{}(s,\pi_{1})\mathrel{\overline{\sqsubseteq}}_{Sm}\widetilde{}(t,\pi_{2})$, where $\widetilde{}(s,\pi)=\{\Delta\in\mathcal{D}(S)\mid\exists\pi^{\prime}\in\Pi_{\cal{I\!I}}:\widetilde{}(s,\langle\pi,\pi^{\prime}\rangle)=\Delta\}$.

If state $s$ PA-simulates state $t$ and $t$ PA-simulates $s$, we say $s$ and $t$ are PA-simulation equivalent, which is written $s\simeq t$.

4 A Modal Logic for Probabilistic GS

In the literature different modal logics have been introduced to characterise process semantics at different levels. Hennessy-Milner logic (HML) [11] provides a classical example that has been proved to be equivalent to bisimulation semantics in image-finite LTS. In other words, two states (or processes) satisfy the same set of HML formulas iff they are bisimilar. For a more comprehensive survey we refer to [28].

In this section we propose a modal logic for PGS that characterises a player’s abilitiy to enforce temporal properties. We define a new logic $\mathcal{L}^{\oplus}$ in the spirit of the logic of Deng et al. [8, 9]. The syntax of the logic $\mathcal{L}^{\oplus}$ is presented below.

[TABLE]

In particular, $p$ is an atomic formula that belongs to the set Prop. Formula $\bigwedge_{i\in I}\varphi_{i}$ produces a conjunction, and $\bigvee_{i\in I}\varphi_{i}$ produces a disjunction, both via an index set $I$. We then derive $\top=\bigwedge_{i\in\emptyset}\varphi_{i}$ is a formula that is true everywhere, and $\bot=\bigvee_{i\in\emptyset}\varphi_{i}$ is a formula false everywhere. $\langle\!\langle{\cal I}\rangle\!\rangle\varphi$ specifies player ${\cal I}$’s ability to enforce $\varphi$ in the next step. The probabilistic summation operator $\bigoplus_{j\in J}p_{j}\varphi_{j}$ explicitly specifies that a distribution satisfying such a formula should be split with pre-defined weights, each part with weight $p_{j}$ satisfying sub-formula $\varphi_{j}$. For a summation formula with index $J$, we may explicitly write down each component coupled by its weight, such as in the way of $[p_{1},\varphi_{1}]\oplus[p_{2},\varphi_{2}]\oplus\ldots\oplus[p_{|J|},\varphi_{|J|}]$. The operator $\bigoplus_{j\in J}\varphi_{j}$ allows arbitrary linear interpolation among formulas $\varphi_{j}$. We only allow negation of formulas on the propositional level. We use $\mathcal{L}^{\oplus}$ to denote the set of modal formulas defined by the above syntax.

The semantics of $\mathcal{L}^{\oplus}$ is presented as follows. The interpretation of each formula is defined as a set of distributions of states in a finite PGS $\mathcal{G}=\langle S,s_{0},L,\texttt{Act},$.

• •

$\llbracket p\rrbracket=\{\Delta\in\mathcal{D}(S)\mid\forall s\in\lceil\Delta\rceil:p\in L(s)\}$;

• •

$\llbracket\neg p\rrbracket=\{\Delta\in\mathcal{D}(S)\mid\forall s\in\lceil\Delta\rceil:p\not\in L(s)\}$;

• •

$\llbracket\bigwedge_{i\in I}\varphi_{i}\rrbracket=\bigcap_{i\in I}\llbracket\varphi_{i}\rrbracket$; $\llbracket\bigvee_{i\in I}\varphi_{i}\rrbracket=\bigcup_{i\in I}\llbracket\varphi_{i}\rrbracket$;

• •

$\llbracket\langle\!\langle{\cal I}\rangle\!\rangle\varphi\rrbracket=\{\Delta\in\mathcal{D}(S)\mid\exists\pi_{1}\in\Pi_{\cal I}:\forall\pi_{2}\in\Pi_{\cal{I\!I}}:\Delta\xrightarrow{\pi_{1},\pi_{2}}\Theta\mbox{ implies }\Theta\in\llbracket\varphi\rrbracket\}$;

• •

$\llbracket\bigoplus_{j\in J}p_{j}\varphi_{j}\rrbracket=\{\Delta\in\mathcal{D}(S)\mid\Delta=\sum_{j\in J}p_{j}\Delta_{j}\wedge\forall j\in J:\Delta_{j}\in\llbracket\varphi_{j}\rrbracket\}$;

• •

$\llbracket\bigoplus_{j\in J}\varphi_{j}\rrbracket=\{\Delta\in\mathcal{D}(S)\mid\exists\{p_{j}\}_{j\in J}:\sum_{j\in J}p_{j}=1\wedge\Delta=\sum_{j\in J}p_{j}\Delta_{j}\wedge\forall j\in J:\Delta_{j}\in\llbracket\varphi_{j}\rrbracket\}$;

Note here we say a distribution $\Delta$ satisfies a propositional formula if the formula holds in every state in the support of $\Delta$. The rest of the semantics is self-explained.

Remark. The probabilistic modal logic proposed by Parma and Segala [22] and Hermanns et al. [12] uses a fragment operator $[\varphi]_{\alpha}$, such that a distribution $\Delta\models[\varphi]_{\alpha}$ iff there exists $\Delta_{1},\Delta_{2}\in\mathcal{D}(S)$ such that $\Delta=\Delta_{1}\oplus_{\alpha}\Delta_{2}$ and $\Delta_{1}\models\varphi$. Informally, it states that a fragment of $\Delta$ with weight at least $\alpha$ satisfies $\varphi$. Note that the summation operator of $\mathcal{L}^{\oplus}$ can be used to encode the fragment operator $[\varphi]_{\alpha}$, in the way that $\Delta\models[\varphi]_{\alpha}$ iff $\Delta\models[\alpha,\varphi]\oplus[1-\alpha,\top]$. Therefore, a straightforward adaptation of the logic by Parma and Segala [22] and Hermanns et al. [12] does not yield a more expressive logic than $\mathcal{L}^{\oplus}$.

The semantics of $\bigoplus_{j\in J}\varphi_{j}$ allows arbitrary linear interpolation among formulas $\varphi_{j}$. Similar to the way treating probabilistic summations, one may write down $\bigoplus_{j\in J}\varphi_{j}$ by $[\varphi_{1}]\oplus[\varphi_{2}]\oplus\ldots\oplus[\varphi_{|J|}]$. The following lemma is straightforward.

Lemma 4.2**.**

Let $\varphi=\bigoplus_{j\in J}p_{j}\varphi_{j}$ and $\varphi^{\prime}=\bigoplus_{j\in J}\varphi_{j}$, and $\Delta\in\mathcal{D}(S)$. We have $\Delta\models\varphi$ implies $\Delta\models\varphi^{\prime}$.

Similar to most of the literature, given a PGS $\mathcal{G}$, we define preorders on the set of states in $\mathcal{G}$ with respect to satisfaction of the modal logic $\mathcal{L}^{\oplus}$.

Definition 4.3**.**

Given states $s,t\in S$, $s\sqsubseteq_{\mathcal{L}^{\oplus}}t$ if for all $\varphi\in\mathcal{L}^{\oplus}$, $s\models\varphi$ implies $t\models\varphi$. If $s\sqsubseteq_{\mathcal{L}^{\oplus}}t$ and $t\sqsubseteq_{\mathcal{L}^{\oplus}}s$, we write $s\simeq_{\mathcal{L}^{\oplus}}t$.

Now we state the first main result of the paper, and we leave its proof in the following two subsections.

Theorem 4.4**.**

Let $\mathcal{G}=\langle S,s_{0},L,\texttt{Act},$ be a PGS, then for all $s,t\in S$, $s\sqsubseteq t$ iff $s\sqsubseteq_{\mathcal{L}^{\oplus}}t$.

Proof 4.6**.**

By combining Theorem 4.25 and Theorem 4.40 and by treating $s$ and $t$ as point distributions $\widetilde{s}$ and $\widetilde{t}$.

Corollary 4.7**.**

Let $\mathcal{G}=\langle S,s_{0},L,\texttt{Act},$ be a PGS, then for all $s,t\in S$, $s\simeq t$ iff $s\simeq_{\mathcal{L}^{\oplus}}t$.

4.1 A Soundness Proof

Since the notion of PA-simulation given in Definition 3.9 is defined as a relation on states, in the following we show that the lifted PA-simulation is also a simulation on distributions over the states, which is used as a stepping stone to our soundness result. Similar to the way of treating distributions, we also allow linear combination of mixed actions.

Definition 4.9**.**

Given a list of mixed actions $\langle\pi_{i}\rangle_{i\in I}$ (of player ${\cal I}$), and $\langle p_{i}\rangle_{i\in I}$ satisfying $\sum_{i\in I}p_{i}=1$, $\sum_{i\in I}p_{i}\pi_{i}$ is a mixed action defined by $\left(\sum_{i\in I}p_{i}\pi_{i}\right)(s)(a)=\sum_{i\in I}p_{i}\cdot\left(\pi_{i}(s)(a)\right)$ for all $s\in S$ and $a\in\texttt{Act}_{\cal I}$.

Lemma 4.10**.**

Let $s\in S$, $\pi\in\Pi_{\cal I}$ and $\sigma=\sum_{i\in I}p_{i}\sigma_{i}\in\Pi_{\cal{I\!I}}$, then $\widetilde{}(s,\langle\pi,\sigma\rangle)=\sum_{i\in I}p_{i}\cdot\widetilde{}(s,\langle\pi,\sigma_{i}\rangle)$.

Lemma 4.13**.**

Let $s\in S$, $\pi=\sum_{i\in I}p_{i}\pi_{i}\in\Pi_{\cal I}$ and $\sigma\in\Pi_{\cal{I\!I}}$, then $\widetilde{}(s,\langle\pi,\sigma\rangle)=\sum_{i\in I}p_{i}\cdot\widetilde{}(s,\langle\pi_{i},\sigma\rangle$.

Lemma 4.10 and Lemma 4.13 show that we can distribute the distributions over actions out of a transition operator.

Lemma 4.16**.**

Let $\Delta,\Theta\in\mathcal{D}(S)$ with $\Delta=\sum_{i\in I}p_{i}\Delta_{i}$ and $\Theta=\sum_{i\in I}p_{i}\Theta_{i}$, $\pi_{1},\pi_{2}\in\Pi_{\cal I}$ and $\sigma_{1},\sigma_{2}\in\Pi_{\cal{I\!I}}$. If $\widetilde{}(\Delta_{i},\langle\pi_{1},\sigma_{1}\rangle)\ \overline{\sqsubseteq}\ \widetilde{}(\Theta_{i},\langle\pi_{2},\sigma_{2}\rangle)$ for all $i\in I$, then $\widetilde{}(\Delta,\langle\pi_{1},\sigma_{1}\rangle)\ \overline{\sqsubseteq}\ \widetilde{}(\Theta,\langle\pi_{2},\sigma_{2}\rangle)$.

Lemma 4.16 allows to merge the simulation by component distributions on both sides of the relation. The next auxiliary lemma states that given a PA-simulation on states, the lifted PA-simulation on distributions of states can be treated as a simulation via mixed actions of player ${\cal I}$ and player ${\cal{I\!I}}$.

Lemma 4.21**.**

Let $\mathcal{G}=\langle S,s_{0},\mathcal{L},\texttt{Act},$ be a PGS, and $\sqsubseteq$ be a PA-simulation relation for $\mathcal{G}$. Given $\Delta\overline{\sqsubseteq}\Theta$, for all player ${\cal I}$ mixed actions $\pi_{1}$, there exists a player ${\cal I}$ mixed action $\pi_{2}$, such that $\widetilde{}(\Delta,\pi_{1})\overline{\sqsubseteq}_{Sm}\widetilde{}(\Theta,\pi_{2})$.

This can be proved by splitting distributions on both sides, and then merge related components to form distributions on both sides of the lifted relation, applying previous lemmas.

Theorem 4.25**.**

Given $\varphi\in\mathcal{L}^{\oplus}$ and $\Delta\overline{\sqsubseteq}\Theta$, then $\Delta\models\varphi$ implies $\Theta\models\varphi$.

The theorem can be proved by structural induction on $\varphi$. The base cases when $\varphi=p$ and $\neg p$ are straightforward. For the Induction step, we only show the case of $\langle\!\langle{\cal I}\rangle\!\rangle\psi$, as the other cases are straightforward. If $\varphi=\langle\!\langle{\cal I}\rangle\!\rangle\psi$, then there exists a player ${\cal I}$ mixed actions $\pi_{1}$ such that for all player ${\cal{I\!I}}$ mixed actions $\sigma_{1}$, $\Delta\xrightarrow{\pi_{1},\sigma_{1}}\Delta^{\prime}$ and $\Delta^{\prime}\models\psi$. By Lemma 4.21, there exists a player ${\cal I}$ mixed action $\pi_{2}$ such that $\widetilde{}(\Delta,\pi_{1})\,\overline{\sqsubseteq}_{Sm}\widetilde{}(\Theta,\pi_{2})$. Therefore, for all player ${\cal{I\!I}}$ mixed actions $\sigma_{2}$ there exists a player ${\cal{I\!I}}$ strategy $\sigma_{1}^{\prime}$, such that $\Delta\xrightarrow{\pi_{1},\sigma_{1}^{\prime}}\Delta^{\prime\prime}$, $\Theta\xrightarrow{\pi_{2},\sigma_{2}}\Theta^{\prime}$, and $\Delta^{\prime\prime}\overline{\sqsubseteq}\Theta^{\prime}$. Since $\Delta^{\prime\prime}\models\psi$, by I.H., $\Theta^{\prime}\models\psi$. This shows that $\pi_{2}$ is the player ${\cal I}$ mixed action for $\Theta\models\langle\!\langle{\cal I}\rangle\!\rangle\psi$.

4.2 A Completeness Proof

The completeness is proved by approximating the relations $\sqsubseteq$ and $\sqsubseteq_{\mathcal{L}^{\oplus}}$. For PA-simulation we construct relations $\sqsubseteq^{n}$ for $n\in\mathbb{N}$, where $n$ denotes the numbers of steps that are required to check for a state to simulate another. (Intuitively, the more steps to check, the harder for a pair of states to satisfy the relation.) Similarly we define $\sqsubseteq^{\mathcal{L}}_{n}$, restricting to formulas in $\mathcal{L}^{\oplus}$ with size up to $n$. Then we prove that the relation $\sqsubseteq^{\mathcal{L}}_{n}$ is contained in $\sqsubseteq^{n}$ for all $n\in\mathbb{N}$.

Definition 4.28**.**

Let $\mathcal{L}^{\oplus}_{0}$ be the set of formulas constructed by using only $p$, $\neg p$ and $\bigwedge_{i\in I}\varphi_{i}$. For $n\in\mathbb{N}$, a formula $\varphi\in\mathcal{L}^{\oplus}_{n+1}$ if either $\varphi\in\mathcal{L}^{\oplus}_{n}$ or $\varphi$ is a conjunction of formulas of the form $\langle\!\langle{\cal I}\rangle\!\rangle\bigoplus_{i\in I}\sum_{j\in J}p_{j}\varphi_{i,j}$, where each $\varphi_{i,j}\in\mathcal{L}^{\oplus}_{n}$.

Intuitively, formulas in $\mathcal{L}^{\oplus}_{n}$ require $n$ steps of transitions (for player ${\cal I}$) to enforce. Given states $s,t\in S$, we write $s\sqsubseteq^{\mathcal{L}}_{n}t$, if for all $\varphi\in\mathcal{L}^{\oplus}_{n}$, $\widetilde{s}\models\varphi$ implies $\widetilde{t}\models\varphi$. Similarly we define approximating relations for PA-simulation.

Definition 4.29**.**

Given $s,t\in S$, $s\sqsubseteq_{0}t$ if $L(s)=L(t)$. For $n\in\mathbb{N}$, $s\sqsubseteq_{n+1}t$ if $s\sqsubseteq_{n}t$, and for all player ${\cal I}$ mixed actions $\pi_{1}$ there exists a player ${\cal I}$ mixed action $\pi_{2}$, such that $\widetilde{}(s,\pi_{1})\ (\overline{\sqsubseteq}_{n})_{Sm}\widetilde{}(t,\pi_{2})$.

Before starting the completeness proof, we define formulas that characterise properties of the game states. Let $s\in S$, the [math]-characteristic formula for $s$ is $\phi_{s}^{0}=\bigwedge\{p\mid p\in L(s)\}\wedge\bigwedge\{\neg q\mid q\in\texttt{Prop}\setminus L(s)\}$. Plainly, the level [math]-characterisation considers only propositional formulas. For a distribution, we specify the characteristic formulas for the states in its support proportional to weights. The [math]-characteristic formula $\phi^{0}_{\Delta}$ for distribution $\Delta$ is $\sum_{t\in\lceil\Delta\rceil}\Delta(t)\cdot\phi_{t}^{0}$. Given all $n$-characteristic formulas defined, the ($n+1$)-characteristic formula $\phi_{s}^{n+1}$ for state $s$ is $\bigwedge_{\pi\in\mathcal{D}(\texttt{Act}_{\cal I})}\langle\!\langle{\cal I}\rangle\!\rangle\bigoplus_{\texttt{Act}_{\cal{I\!I}}}\phi^{n}_{\Delta_{\pi,b}}$, where $\widetilde{s}\xrightarrow{\pi,\widetilde{b}}\Delta_{\pi,b}$. Similarly, an $n$-characteristic formula $\phi^{n+1}_{\Delta}$ for distribution $\Delta$ is $\sum_{t\in\lceil\Delta\rceil}\Delta(t)\cdot\phi_{t}^{n+1}$.

Obviously every state or distribution satisfies its own characteristic formula, and the following lemma can be proved straightforwardly by induction on $n\in\mathbb{N}$.

Lemma 4.32**.**

For all $\Delta\in\mathcal{D}(S)$, $\Delta\models\phi^{n}_{\Delta}$ for all $n\in\mathbb{N}$.

Lemma 4.33**.**

For all states $s,t\in S$ and $n\in\mathbb{N}$, $s\sqsubseteq^{\mathcal{L}}_{n}t$ implies $s\sqsubseteq_{n}t$.

Proof 4.34**.**

For each $n\in\mathbb{N}$, we have $\widetilde{s}\models\phi^{n}_{s}$ by Lemma 4.32. Let $s\sqsubseteq^{\mathcal{L}}_{n}t$, then $\widetilde{t}\models\phi^{n}_{s}$. We proceed by induction on the level of approximation $n$ to show that $s\sqsubseteq_{n}t$.

First we show that the state-based relation can be naturally carried over to distributions. Suppose for all $s,t\in S$, $s\sqsubseteq^{\mathcal{L}}_{n}t$ implies $\widetilde{t}\models\phi^{n}_{s}$. Given two distributions $\Delta,\Theta\in\mathcal{D}(S)$ and let $\Delta\ \overline{\sqsubseteq}^{\mathcal{L}}_{n}\ \Theta$. Then there exists a weight function $w$, such that $\Delta=\sum_{s\in\lceil\Delta\rceil,t\in\lceil\Theta\rceil:w(s,t)>0}w(s,t)\cdot\widetilde{s}$, and $\Theta=\sum_{s\in\lceil\Delta\rceil,t\in\lceil\Theta\rceil:w(s,t)>0}w(s,t)\cdot\widetilde{t}$, and $s\sqsubseteq^{\mathcal{L}}_{n}t$ for all $w(s,t)>0$. Since $\phi^{n}_{\Delta}$ can be written as $\sum_{s\in\lceil\Delta\rceil,t\in\lceil\Theta\rceil:w(s,t)>0}w(s,t)\cdot\phi^{n}_{s}$, we must have $\Theta\models\phi^{n}_{\Delta}$ as well.

Base case:* Trivial.*

Induction step:* Let $\widetilde{t}\models\phi^{n+1}_{s}$, where $\phi^{n+1}_{s}=\bigwedge_{\pi\in\mathcal{D}(\texttt{Act}_{\cal I})}\langle\!\langle{\cal I}\rangle\!\rangle\bigoplus_{\texttt{Act}_{\cal{I\!I}}}\phi^{n}_{\Delta_{\pi,b}}$. Then for each $\pi\in\mathcal{D}(\texttt{Act}_{\cal I})$, $\widetilde{t}\models\langle\!\langle{\cal I}\rangle\!\rangle\bigoplus_{b\in\texttt{Act}_{\cal{I\!I}}}\phi^{n}_{\Delta_{\pi,b}}$. By definition there exists a player ${\cal I}$ mixed action $\pi^{\prime}$, such that for every player ${\cal{I\!I}}$ mixed action $\sigma$, we have $\widetilde{t}\xrightarrow{\pi^{\prime},\sigma}\Theta$ and $\Theta\models\bigoplus_{b\in\texttt{Act}_{\cal{I\!I}}}\phi^{n}_{\Delta_{\pi,b}}$. We need to show that $\widetilde{}(s,\pi)\mathrel{(\overline{\sqsubseteq}^{\mathcal{L}}_{n})}_{Sm}\widetilde{}(t,\pi^{\prime})$.*

*It suffices to check each $b\in\texttt{Act}_{\cal{I\!I}}$ from $t$ can be followed by a player ${\cal{I\!I}}$ mixed action from $s$ to establish such a simulation. Let $b^{\prime}$ be a player ${\cal{I\!I}}$ action, and $\widetilde{t}\xrightarrow{\pi^{\prime},\widetilde{b^{\prime}}}\Theta$. Since $\Theta\models\bigoplus_{b\in\texttt{Act}_{\cal{I\!I}}}\phi^{n}_{\Delta_{\pi,b}}$, there exists a list of probability values $\langle p_{c}\rangle_{c\in\texttt{Act}_{\cal{I\!I}}}$, such that $\Theta\models\sum_{c\in\texttt{Act}_{\cal{I\!I}}}p_{c}\phi^{n}_{\Delta_{\pi,c}}$. Then by definition, we have $\Theta=\sum_{c\in\texttt{Act}_{\cal{I\!I}}}p_{c}\cdot\Theta_{c}$, $\sum_{c\in\texttt{Act}_{\cal{I\!I}}}p_{c}=1$ and $\Theta_{c}\models\phi^{n}_{\Delta_{\pi,c}}$ for all $c\in\texttt{Act}_{\cal{I\!I}}$. In state $s$, we define a player ${\cal{I\!I}}$ mixed action $\sigma$ satisfying $\sigma(s)(c)=p_{c}$ for all $c\in\texttt{Act}_{\cal{I\!I}}$. Then by Lemma 4.10, we have $\widetilde{}(s,\langle\pi,\sigma\rangle)=\sum_{c\in\texttt{Act}_{\cal{I\!I}}}p_{c}\cdot$ for all $c\in\texttt{Act}_{\cal{I\!I}}$. By Lemma 2.17, it suffices to show for all $c\in\texttt{Act}_{\cal{I\!I}}$. Since $\Theta_{c}\models\phi^{n}_{\Delta_{\pi,c}}$, we have $\Delta_{\pi,c}\overline{\sqsubseteq}^{n}\Theta_{c}$ by I.H.. *

Intuitively, by fixing a mixed strategy from player ${\cal I}$, a transition in the PGS is bounded by deterministic actions from player ${\cal{I\!I}}$, as mimicked in the structure of the characteristic formulas. The way of showing satisfaction of a characteristic formula thus mimic the PA-simulation in the proof of Lemma 4.33.

Theorem 4.40**.**

For all $s,t\in S$, $s\sqsubseteq^{\mathcal{L}}t$ implies $s\sqsubseteq t$.

Proof 4.41**.**

In a finite state PGS (i.e., the space $S\times S$ is finite) there exists $n\in\mathbb{N}$ such that $\sqsubseteq\ =\ \sqsubseteq^{n}$. Since $\sqsubseteq^{\mathcal{L}}\ \subseteq\ \sqsubseteq^{\mathcal{L}}_{n}$ for all $n$, and $\sqsubseteq^{\mathcal{L}}_{n}\ \subseteq\ \sqsubseteq_{n}$ by Lemma 4.33, we have $\sqsubseteq^{\mathcal{L}}\ \subseteq\ \sqsubseteq^{n}\ =\ \sqsubseteq$.

5 Probabilistic Alternating-time Mu-Calculus

Modal logics of finite modality depth are not enough to express temporal requirements such as “something bad never happens”. In this section, we extend the logic $\mathcal{L}^{\oplus}$ into a Probabilistic Alternating-time $\mu$-calculus (PAMu), by adding variables and fixpoint operators.

[TABLE]

Let the environment $\rho:\mathcal{V}\rightarrow\mathcal{P}(\mathcal{D}(S))$ be a mapping from variables in $\mathcal{V}$ to sets of distributions on states, and the semantics of the fixpoint operators of PAMu are defined in the standard way.

• •

$\llbracket p\rrbracket_{\rho}=\{\Delta\in\mathcal{D}(S)\mid\forall s\in\lceil\Delta\rceil:p\in L(s)\}$;

• •

$\llbracket\neg p\rrbracket_{\rho}=\{\Delta\in\mathcal{D}(S)\mid\forall s\in\lceil\Delta\rceil:p\not\in L(s)\}$;

• •

$\llbracket\bigwedge_{i\in I}\varphi_{i}\rrbracket_{\rho}=\bigcap_{i\in I}\llbracket\varphi_{i}\rrbracket_{\rho}$; $\llbracket\bigvee_{i\in I}\varphi_{i}\rrbracket=\bigcup_{i\in I}\llbracket\varphi_{i}\rrbracket_{\rho}$;

• •

$\llbracket\langle\!\langle{\cal I}\rangle\!\rangle\varphi\rrbracket_{\rho}=\{\Delta\in\mathcal{D}(S)\mid\exists\pi_{1}\in\Pi_{\cal I}:\forall\pi_{2}\in\Pi_{\cal{I\!I}}:\Delta\xrightarrow{\pi_{1},\pi_{2}}\Theta\mbox{ implies }\Theta\in\llbracket\varphi\rrbracket_{\rho}\}$;

• •

$\llbracket\bigoplus_{j\in J}p_{j}\varphi_{j}\rrbracket_{\rho}=\{\Delta\in\mathcal{D}(S)\mid\Delta=\sum_{j\in J}p_{j}\Delta_{j}\wedge\forall j\in J:\Delta_{j}\in\llbracket\varphi_{j}\rrbracket_{\rho}\}$;

• •

$\llbracket\bigoplus_{j\in J}\varphi_{j}\rrbracket_{\rho}=\{\Delta\in\mathcal{D}(S)\mid\exists\{p_{j}\}_{j\in J}:\sum_{j\in J}p_{j}=1\wedge\Delta=\sum_{j\in J}p_{j}\Delta_{j}\wedge\forall j\in J:\Delta_{j}\in\llbracket\varphi_{j}\rrbracket_{\rho}\}$;

• •

$\llbracket Z\rrbracket_{\rho}=\rho(Z)$;

• •

$\llbracket\mu Z.\varphi\rrbracket_{\rho}=\bigcap\{D\subseteq\mathcal{D}(S)\mid\llbracket\varphi\rrbracket_{\rho}[Z\mapsto D]\subseteq D\}$;

• •

$\llbracket\nu Z.\varphi\rrbracket_{\rho}=\bigcup\{D\subseteq\mathcal{D}(S)\mid D\subseteq\llbracket\varphi\rrbracket_{\rho}[Z\mapsto D]\}$.

The set of closed PAMu formulas are the formulas with all variables bounded, which form the set $\mathcal{L}^{\mu}$, and we can safely drop the environment $\rho$ for those formulas.

Example 5.1**.**

For the rock-paper-scissors game in Figure 1, the property describing that player ${\cal I}$ has a strategy to eventually win the game once can be expressed as $\mu Z.{\sf win}_{{\cal I}}\vee\langle\!\langle{\cal I}\rangle\!\rangle Z$. This property does not hold. However, player ${\cal I}$ has a strategy to eventually win the game with probability almost $\frac{1}{2}$, i.e., the system satisfies $\mu Z.([\frac{1}{2}-\epsilon,{\sf win}_{{\cal I}}]\oplus[\frac{1}{2}+\epsilon,\top])\vee\langle\!\langle{\cal I}\rangle\!\rangle Z$ for arbitrarily small $\epsilon>0$. We explain the reason why players can only enforce $\epsilon$-optimal strategies in later part of the section.

The logic characterisation of PA-Simulation can be extended to PAMu.

Theorem 5.2**.**

Given $\Delta,\Theta\in\mathcal{D}(S)$, $\Delta\overline{\sqsubseteq}\Theta$ iff $\{\varphi\in\mathcal{L}^{\mu}\mid\Delta\models\varphi\}\subseteq\{\varphi\in\mathcal{L}^{\mu}\mid\Theta\models\varphi\}$.

Since $\mathcal{L}^{\oplus}$ is syntactically a sublogic of $\mathcal{L}^{\mu}$, we only need to show the soundness of PA-simulation to the logic $\mathcal{L}^{\mu}$. We apply the classical approach of approximants for Modal Mu-Calculus [3]. Given formulas $\mu Z.\varphi$ and $\nu Z.\phi$, we define the following.

[TABLE]

Next we show approximants are semantically equivalent to the fixpoint formulas.

Lemma 5.3**.**

(1) $\llbracket\mu^{\omega}Z.\varphi\rrbracket=\llbracket\mu Z.\varphi\rrbracket$; (2) $\llbracket\nu^{\omega}Z.\phi\rrbracket=\llbracket\nu Z.\phi\rrbracket$.

We briefly sketch a proof of Lemma 5.3(1), and the proof for the other part of the lemma is similar. To show $\llbracket\mu^{\omega}Z.\varphi\rrbracket\subseteq\llbracket\mu Z.\varphi\rrbracket$, we initially have $\llbracket\mu^{0}Z.\varphi\rrbracket=\emptyset\subseteq\llbracket\mu Z.\varphi\rrbracket$, then by the monotonicity of $\varphi$, given $\llbracket\mu^{i}Z.\varphi\rrbracket\subseteq\llbracket\mu Z.\varphi\rrbracket$, we prove $\llbracket\mu^{i+1}Z.\varphi\rrbracket\subseteq\llbracket\mu Z.\varphi\rrbracket$ by applying $\varphi$ on both sides of $\subseteq$. Therefore, $\llbracket\mu^{i}Z.\varphi\rrbracket\subseteq\llbracket\mu Z.\varphi\rrbracket$ for all $i\in\mathbb{N}$, thus $\llbracket\bigvee_{i\in\mathbb{N}}\mu^{i}Z.\varphi\rrbracket\subseteq\llbracket\mu Z.\varphi\rrbracket$. To show $\llbracket\mu Z.\varphi\rrbracket\subseteq\llbracket\mu^{\omega}Z.\varphi\rrbracket$, it is straightforward to see that $\mu^{\omega}Z.\varphi$ is a prefixpoint, therefore it contains $\mu Z.\varphi$, the intersection of all prefixpoints.

From Lemma 5.3, and by the soundness of PA-simulation to $\mathcal{L}^{\oplus}$ (Theorem 4.25), we get the the soundness of PA-simulation to the logic $\mathcal{L}^{\mu}$, as required.

Expressiveness of PAMu. There exist game-based extensions of probabilistic temporal logics, such as the logic PAMC [27] that extends the Alternating-time Mu-Calculus [1], and PATL [5] that extends PCTL [10]. The semantics of both logics are sets of states, rather than sets of distributions. It has also been shown in [27] that PAMC and PATL are incomparable on probabilistic game structures, based on a result showing that PCTL and P$\mu$TL are incomparable on Markov chains [18]. Here we make a short comparison between PAMu and those logics.

Distribution formulas of PAMu cannot be expressed by state-based logics. For example, the formula $\langle\!\langle{\cal I}\rangle\!\rangle[\frac{1}{2},p]\oplus[\frac{1}{2},q]$, expressing that player ${\cal I}$ has a strategy to enforce in the next move a distribution which has half of its weight satisfying $p$ and the other half satisfying $q$, cannot be expressed by PATL or PAMC. As the latter two logics have probability values bundled with strategy modalities, a formula such as $\langle\!\langle{\cal I}\rangle\!\rangle^{\geq\frac{1}{2}}p\wedge\langle\!\langle{\cal I}\rangle\!\rangle^{\geq\frac{1}{2}}q$ denotes that player ${\cal I}$ has a strategy to enforce $p$ with at least probability $\frac{1}{2}$ in the next step and player ${\cal I}$ also has a possibly different strategy to enforce $q$ with at least probability $\frac{1}{2}$ in the next step. However, the resulting states (or distributions) that satisfy $p$ and $q$ may overlap.

The PATL formula $\langle\!\langle{\cal I}\rangle\!\rangle^{\geq 1}\Diamond p$ is not expressible by PAMu. Given the PGS in Figure 3 where player ${\cal I}$ has action set $\{a\}$ and player ${\cal{I\!I}}$ has action set $\emptyset$. Then it is straightforward to see both $s_{0}$ and $s_{1}$ satisfies $\langle\!\langle{\cal I}\rangle\!\rangle^{\geq 1}\Diamond p$. The closest formula in PAMu is $\mu Z.p\vee\langle\!\langle{\cal I}\rangle\!\rangle Z$, but $s_{0}\not\models\mu Z.p\vee\langle\!\langle{\cal I}\rangle\!\rangle Z$. More precisely, $s_{0}\models\mu Z.([\alpha,p]\oplus[1-\alpha,\top])\vee\langle\!\langle{\cal I}\rangle\!\rangle Z$ for all $0\leq\alpha<1$. Intuitively, the semantics of the least fixpoint operator in PAMu only track finite number of probabilistic transitions, as starting from $s_{0}$, player ${\cal I}$ can only reach distributions that satisfy $p$ with probability strictly less than $1$ with finite number of steps.333Intuitively, $\widetilde{s_{0}}\stackrel{{\scriptstyle a}}{{\rightarrow}}[\frac{1}{2},s_{0}]\oplus[\frac{1}{2},s_{1}]\stackrel{{\scriptstyle a}}{{\rightarrow}}[\frac{1}{4},s_{0}]\oplus[\frac{3}{4},s_{1}]\stackrel{{\scriptstyle a}}{{\rightarrow}}\ldots\stackrel{{\scriptstyle a}}{{\rightarrow}}[\frac{1}{2^{i}},s_{0}]\oplus[1-\frac{1}{2^{i}},s_{1}]\ldots$. We shall see that in finite number of transitions one never reaches $\widetilde{s_{1}}$ from $\widetilde{s_{0}}$ with strict probability $1$. However, such a restriction may be alleviated in practice, as implemented in PRISM-game [16], $\epsilon$-optimal strategies are synthesized for unbounded reachability properties. PAMC formulas that contain the $\llbracket{\cal I}\rrbracket^{\bowtie\alpha}$ modalities do not seem expressible in PAMu. For instance, the PAMC formula $\llbracket{\cal I}\rrbracket^{\geq\alpha}\varphi$ 444$\llbracket{\cal I}\rrbracket^{\geq\alpha}\varphi$ can be interpreted as for all player ${\cal I}$ strategies $\pi$, there exists player ${\cal{I\!I}}$ strategy $\sigma$, such that the combined effect of $\pi$ and $\sigma$ enforces $\varphi$ with probability at least $\alpha$. is semantically equivalent to $\neg\langle\!\langle{\cal I}\rangle\!\rangle^{<\alpha}\varphi$, which is not expressible by PAMu as negation is only allowed at the propositional level in PAMu. Nevertheless, the focus of PAMu is more on logic characterisation than expressiveness.

Example 5.4**.**

The authors of [16] proposed a CSG variant of a futures market investor model [20], which studies the interactions between an investor and a stock market. The investor and the market take their decisions simultaneously in the CSG model, and the authors show that this does not give any additional benefits to the investor by analysing his maximum expected value over a fixed period of time.555 For details of the model, we refer to [20] and the website https://www.prismmodelchecker.org. We take this example to show the expressiveness of PAMu. For instance, the property “it is always possible for the investor to cash in” can be specified with two nested fixpoints as

[TABLE]

Another interesting property is to check whether the investor has a strategy to ensure a good chance for him to make a profit. This can be formulated in PAMu with $\frac{1}{2}<\alpha\leq 1$, as

[TABLE]

6 Related Work

Segala and Lynch [25] introduce a probabilistic simulation relation which preserves probabilistic computation tree logic (PCTL) formulas without negation and existential quantification. Segala introduces the notion of probabilistic forward simulation, which relates states to probability distributions over states and is sound and complete for trace distribution precongruence [23, 19]. Parma and Segala [22] use a probabilistic extension of the Hennessy-Milner logic which allows countable conjunction and admits a new operator $[\phi]_{p}$ – a distribution satisfies $[\phi]_{p}$ if the probability on the set of states satisfying $\phi$ is at least $p$, with a sound and complete logic characterisation. Hermanns et al. [12] further extend this result for image-infinite probabilistic automata. Deng et al. [8, 9] introduce a few probabilistic operators to derive a probabilistic modal mu-calculus (pMu). A fragment of pMu is proved to characterise (strong) probabilistic simulation in finite-state probabilistic automata.

Alur, Henzinger and Kupferman [1] define alternating-time temporal logic (ATL) to generalise CTL for game structures by requiring each path quantifier to be parameterised by a set of agents. GS are more general than LTS, in the sense that they allow both collaborative and adversarial behaviours of individual agents in a system, and ATL can be used to express properties like “a set of agents can enforce a specific outcome of the system”. The alternating simulation, which is a natural game-theoretic interpretation of the classical simulation in (deterministic) multi-player games, is introduced in [2]. Logic characterisation of this relation concentrates on a subset of ATL⋆ formulas where negations are only allowed at propositional level and all path quantifiers are parameterised by a predefined set of agents.

Game structures deal well with systems in which the players execute a pure strategy, i.e., a strategy in which the moves are chosen deterministically. However, mixed strategies, which are formed by combining pure strategies, are necessary for a player to achieve optimal rewards [29]. Zhang and Pang [30] extend the notion of game structures to probabilistic game structures (PGS) and introduce notions of simulation that are sound for a fragment of probabilistic alternating-time temporal logic (PATL), a probabilistic extension of ATL.

Fixpoint logics for sets of states in Markov chains and PGS have been studied more recently in [18, 27], and a short comparison is given in Section 5.

Metric-based simulation on game structures have been studied by de Alfaro et al [7] regarding the probability of winning games whose goals are expressed in quantitative $\mu$-calculus (qMu) [20]. Two states are equivalent if the players can win the same games with the same probability from both states, and similarity among states can thus be measured. Algorithmic verification complexities are further studied for MDP and turn-based games [4].

More recently, algorithmic verification of turn-based and concurrent games have been implemented as an extension of PRISM [17, 16]. The properties can be specified as state formulas, path formulas and reward formulas. The verification procedure requires solving matrix games for concurrent game structures, and it applies value iteration algorithms to approach the goal (similar to [6, 7]). For unbounded properties, the synthesised strategy is memoryless (but only $\epsilon$-optimal strategies). Finite-memory strategies are synthesised for bounded properties.

7 Conclusions and Future Work

In this work, we have presented sound and complete modal characterisations of PA-simulation for concurrent games by introducing two new logics $\mathcal{L}^{\oplus}$ and PAMu (with fixpoints). Both logics incorporate nondeterministic and probabilisitic features and express the ability of the players to enforce a property in current state. In the future, we aim to study verification complexities for these two logics.