Admissibility in Concurrent Games

TL;DR

This paper investigates the concept of admissibility for randomized strategies in concurrent games, proving their existence, characterizing them, and developing methods for assume-admissible synthesis in omega-regular objectives.

Contribution

It introduces the notion of admissibility in concurrent games, proves their existence, characterizes them, and provides a synthesis method for omega-regular objectives.

Findings

Admissible strategies always exist in concurrent games.

A precise characterization of admissible strategies is provided.

Method for assume-admissible synthesis in omega-regular objectives is developed.

Abstract

In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays `as well as possible', because there is no other strategy that dominates it, i.e., that wins (almost surely) against a super set of adversarial strategies. We prove that admissible strategies always exist in concurrent games, and we characterise them precisely. Then, when the objectives of the players are omega-regular, we show how to perform assume-admissible synthesis, i.e., how to compute admissible strategies that win (almost surely) under the hypothesis that the other players play admissible

Equations

$${\delta }_r(s,(a,\gamma ))(s^{\prime })$$

$$=\sum _{c\in \text{Supp}(\gamma )}\gamma (c){\delta }_r(s,(b,c))(s^{\prime })$$

$$={\delta }_r(s,(b,\gamma ))(s^{\prime }).$$

$${\delta }_r(s,(a,\gamma ))(S_1)$$

$$=\sum _{c\mid h\delta (s,a,c)\in {\text{Val}}_{p,1}^{\star }}\gamma (c){\delta }_r(s,(a,c))(\delta (s,a,c))$$

$$=\sum _{c\mid h\delta (s,b,c)\in {\text{Val}}_{p,1}^{\star }}\gamma (c){\delta }_r(s,(b,c))(\delta (s,b,c))$$

$$=\sum _{s^{\prime }\mid h{s}^{\prime }\in {\text{Val}}_{p,1}^{\star }}{\delta }_r(s,(b,\gamma ))(s^{\prime })$$

$$={\delta }_r(s,(b,\gamma ))(S_1).$$

$${\delta }_r(s,(\alpha ,\gamma ))(s^{\prime })$$

$$=\sum _{a\in \text{Supp}(\alpha )}{\delta }_r(s,(b,\gamma ))(s^{\prime })\alpha (a)$$

$$={\delta }_r(s,(b,\gamma ))(s^{\prime })\sum _{a\in \text{Supp}(\alpha )}\alpha (a)$$

$$={\delta }_r(s,(b,\gamma ))(s^{\prime }).$$

$${\delta }_r(s,(\alpha ,\gamma ))(s^{\prime })$$

$${\delta }_r(s,(\beta ,\gamma ))(s^{\prime })$$

$$=\sum _{b\in \text{Supp}(\beta )}{\delta }_r(s,(\alpha ,\gamma ))(s^{\prime })\beta (b)$$

$$={\delta }_r(s,(\alpha ,\gamma ))(s^{\prime })\sum _{b\in \text{Supp}(\beta )}\beta (b)$$

$$={\delta }_r(s,(\alpha ,\gamma ))(s^{\prime }).$$

$${\delta }_r(s,(\alpha ,\gamma ))(S_1)$$

$$=\sum _{a\in \text{Supp}(\alpha )}\left(\alpha (a)\sum _{s^{\prime }\mid h{s}^{\prime }\in {\text{Val}}_{p,1}^{\star }}{\delta }_r(s,(a,\gamma ))(s^{\prime })\right)$$

$$=\sum _{a\in \text{Supp}(\alpha )}\left(\alpha (a)\sum _{s^{\prime }\mid h{s}^{\prime }\in {\text{Val}}_{p,1}^{\star }}{\delta }_r(s,(b,\gamma ))(s^{\prime })\right)$$

$$=\left(\sum _{s^{\prime }\mid h{s}^{\prime }\in {\text{Val}}_{p,1}^{\star }}{\delta }_r(s,(b,\gamma ))(s^{\prime })\right)\left(\sum _{a\in \text{Supp}(\alpha )}\alpha (a)\right)$$

$$=\sum _{s^{\prime }\mid h{s}^{\prime }\in {\text{Val}}_{p,1}^{\star }}{\delta }_r(s,(b,\gamma ))(s^{\prime }).$$

$${\delta }_r(s,(\alpha ,\gamma ))(S_1)$$

$${\delta }_r(s,(\beta ,\gamma ))(S_1)$$

$$=\sum _{b\in \text{Supp}(\beta )}\left(\beta (b)\sum _{s^{\prime }\mid h{s}^{\prime }\in {\text{Val}}_{p,1}^{\star }}{\delta }_r(s,(b,\gamma ))(s^{\prime })\right)$$

$$=\sum _{b\in \text{Supp}(\beta )}\beta (b){\delta }_r(s,(\alpha ,\gamma ))(S_1)$$

$$={\delta }_r(s,(\alpha ,\gamma ))(S_1)\sum _{b\in \text{Supp}(\beta )}\beta (b)$$

$$={\delta }_r(s,(\alpha ,\gamma ))(S_1)$$

$$\forall h\in {\text{Hist}}_0(\sigma )={\text{Hist}}_0({\sigma }^{\prime }),{\mathbb{P}}_{(\sigma ,\tau )}(\text{Cyl}(h))={\mathbb{P}}_{({\sigma }^{\prime },\tau )}(\text{Cyl}(h)).$$

$${\mathbb{P}}_{(\sigma ,\tau )}(\text{Cyl}(h^{\prime }{s}^{\prime }))$$

$$={\mathbb{P}}_{({\sigma }^{\prime },\tau )}(\text{Cyl}(h^{\prime })){\delta }_r(s,({\sigma }^{\prime }(h^{\prime }),\tau (h^{\prime })))(s^{\prime })$$

$$={\mathbb{P}}_{(\sigma ,\tau )}(\text{Cyl}(h^{\prime }{s}^{\prime }))$$

$$\Phi (p)=\left(\square {\text{Val}}_{p,0}^{\star }\cap \Phi (p)\right)⨄\left(◊{\text{Val}}_{p,1}^{\star }\cap \Phi (p)\right).$$

$${\mathbb{P}}_{({\sigma }^{\prime \prime },\tau )}(◊{\text{Val}}_{p,1}^{\star })=\sum _{h\in {\text{Hist}}_0({\sigma }^{\prime \prime })}{\mathbb{P}}_{({\sigma }^{\prime \prime },\tau )}(\text{Cyl}(h)){\delta }_r(s,({\sigma }^{\prime \prime }(h),\tau (h)))({\text{Val}}_{p,1}^{\star }).$$

$${\text{AfterHelpMove}}_p^{\star }$$

$$\square {\text{Val}}_{i,0}^{\star }\wedge \neg \Phi (i)\wedge ◊\square \neg {\text{AfterHelpMove}}_p^{\star }.$$

$$\neg \Phi (q)\cap \text{Cyl}(h)=(\neg \Phi (q)\cap \{\mathfrak{o}(\rho )\})\cup \bigcup _{k\ge |h|}\bigcup _{s^{\prime }}\left(\neg \Phi (q)\cap \text{Cyl}(\mathfrak{o}({\rho }_{\le k})s^{\prime })\right)$$

Full text

1 Introduction

In a concurrent $n$-player game played on a graph, all $n$ players independently and simultaneously choose moves at each round of the game, and those $n$ choices determine the next state of the game [13]. Concurrent games generalise turn-based games and it is well-known that, while deterministic strategies are sufficient in the turn-based case, randomised strategies are necessary for winning with probability one even for reachability objectives. Intuitively, randomisation is necessary because in concurrent games, in each round, players have no information about the concurrent choice of moves made by the other players. Randomisation allows for some probability of choosing a good move while not knowing the choice of the other players. As a consequence, there are two classical semantics that are considered to analyse these games qualitatively: winning with certainty (sure semantics in the terminology of [13]), and winning with probability one (almost sure semantics in the terminology of [13]). We consider both semantics here.

Previous papers on concurrent games are mostly concerned with two-player zero-sum games, i.e. two players that have fully antagonistic objectives. In this paper, we consider the more general setting of $n$-player non zero-sum concurrent games in which each player has its own objective. The notion of winning strategy is not sufficient to study non zero-sum games and other solution concepts have been proposed. One such concept is the notion of admissible strategy [1].

For a player with objective $\Phi$, a strategy $\sigma$ is said to be dominated by a strategy $\sigma^{\prime}$ if $\sigma^{\prime}$ does as well as $\sigma$ with respect to $\Phi$ against all the strategies of the other players and strictly better for some of them. A strategy $\sigma$ is admissible for a player if it is not dominated by any other of his strategies. Clearly, playing a strategy which is not admissible is sub-optimal and a rational player should only play admissible strategies. While recent works have studied the notion of admissibility for $n$-player non zero-sum game graphs [4, 14, 9, 7, 6], they are all concerned with the special case of turn-based games and this work is the first to consider the more general concurrent games.

Throughout the paper, we consider the running example in Figure 2. This is a concurrent game played by two players. Player $1$’s objective is to reach $\mathsf{Trg}$, while Player $2$ wants to reach $s_{2}$. Edges are labelled by pairs of moves of both players which activate that transition (where $-$ means ‘any move’). It is easy to see that no player can enforce its objective with or without randomisation, so, there is no winning strategy in this game for either player. This is because moving from $s_{0}$ to $s_{1}$ and from $s_{1}$ to $s_{2}$ requires the cooperation of both players. Moreover, the transitions from $s_{2}$ behave as in the classical ‘matching pennies’ game: player $1$ must chose between $f$ and $f^{\prime}$; player $2$ between $g$ and $g^{\prime}$; and the target is reached only when the choices ‘match’. So, randomisation is needed to make sure $\mathsf{Trg}$ is reached with probability one, from $s_{2}$. In the paper, we will describe the dominated and admissible strategies of this game.

Technical contributions

First, we study the notion of admissible strategies for both the sure and almost sure semantics of concurrent games. We show in Theorem 1 that in both semantics admissible strategies always exist. The situation is thus similar to the turn-based case [4, 9]. Nevertheless, the techniques used in this simpler case do not generalise easily to the concurrent case and we need substantially more involved technical tools here. To obtain our universal existence result, we introduce two weaker solution concepts: locally admissible moves and strongly cooperative optimal strategies. While cooperative optimal strategies were already introduced in [6] and shown equivalent to admissible strategies in the turn based setting, there are strictly weaker than admissible strategies in the concurrent setting (both for the sure and the almost sure semantics), and they need to be combined with the notion of locally admissible moves to fully characterise admissible strategies. In the special case of safety objectives, we can show that admissible strategies are exactly those that always play locally admissible moves. This situation is depicted in Figure 1.

Second, we build on our characterisation of admissible strategies based on the notions of locally admissible moves and strongly cooperative optimal strategies to obtain algorithms to solve the assume admissible synthesis problem for concurrent games. In the assume admissible synthesis problem, we ask whether a given player has an admissible strategy that is winning against all admissible strategies of the other players. So this rule relaxes the classical synthesis rule by asking for a strategy that is winning against the admissible strategies of the other players only and not against all of them. This is reasonable as in a multi-player game, each player has his own objective which is generally not the complement of the objectives of the other players. The assume-admissible rule makes the hypothesis that players are rational, hence they play admissible strategies and it is sufficient to win against those strategies. Our algorithm is applicable to all $\omega$-regular objectives and it is based on a reduction to a zero-sum two-player game in the sure semantics. While this reduction shares intuitions with the reduction that we proposed in [7] to solve the same problem in the turn-based case, our reduction here is based on games with imperfect information [17]. In contrast, in the turn-based case, games of perfect information are sufficient. The correctness and completeness of our reduction are proved in Theorem 2.

Related works

Concurrent reachability games were studied in [13] and algorithms to solve more general omega-regular objectives were given in [10]. The games studied there are two-player and zero-sum only. We rely on the algorithms defined in [10] to compute states from which players have almost surely winning strategies for their objectives when all the other players play adversely. States where a player has a (deterministic) strategy to surely win against all other players can be computed by a reduction to more classical turn-based game graphs [2]. Nash equilibria have been studied in concurrent games [5], but without randomised strategies. None of those papers consider the notion of admissibility.

We use the notion of admissibility to obtain synthesis algorithms for systems composed of several sub-systems starting from non zero-sum specifications. There have been a few other proposals in the literature that are based on refinements of the notion of Nash equilibrium (and not on admissibility), most notably: assume-guarantee synthesis [11] and rational synthesis [15, 16]. Those works assume the simpler setting of turn-based games and so they do not deal with randomised strategies. In the context of infinite games played on graphs, one well known limitation of Nash equilibria is the existence of non-credible threats, admissibility does not suffer from this problem.

In [12], Damm and Finkbeiner use the notion of dominant strategy to provide a compositional semi-algorithm for the (undecidable) distributed synthesis problem. So while we use the notion of admissible strategy, they use a notion of dominant strategy. The notion of dominant strategy is strictly stronger: every dominant strategy is admissible but an admissible strategy is not necessary dominant. Also, in multiplayer games with omega-regular objectives with complete information (as considered here), admissible strategies are always guaranteed to exist [4] while it is not the case for dominant strategies.

2 Preliminaries

Concurrent games played on graphs

Let $P=\{1,2,\ldots n\}$ be a set of players. A concurrent game played on a finite graph by the players in $P$ is a tuple $\mathcal{G}=(S,\Sigma,s_{\mathsf{init}},(\Sigma_{p})_{p\in P},\delta)$ where,

(i) $S$is a finite set of states; and $s_{\mathsf{init}}\in S$ the initial state;

(ii) $\Sigma$is a finite set of actions;

(iii) For all $p\in P$, $\Sigma_{p}:S\to 2^{\Sigma}\setminus\{\emptyset\}$ is a action assignment that assigns, to all states $s\in S$, the set of actions available to player $p$ from state $s$.

(iv) $\delta:S\times\Sigma\times\ldots\times\Sigma\rightarrow S$is the transition function.

We write $\Sigma(s)=\Sigma_{1}(s)\times\ldots\times\Sigma_{n}(s)$ for all $s\in S$. It is often convenient to consider a player $p$ separately and see the set of all other players $P\setminus\{p\}$ as a single player denoted $-p$. Hence, the set of actions of $-p$ in state $s$ is: $\Sigma_{-p}(s)=_{\mathrm{def}}\prod_{q\in P\setminus\{p\}}\Sigma_{q}(s)$. We assume that $\Sigma_{i}(s)\cap\Sigma_{j}(s)=\emptyset$ for all $s\in S$ and $i\neq j$. We denote by $\mathrm{Succ}(s,a)=\{\delta(s,a,b)\mid b\in\Sigma_{-p}(s)\}$ the set of possible successors of the state $s\in S$ when player $p$ performs action $a\in\Sigma_{p}(s)$. A particular case of concurrent games are the turn-based games. A game $\mathcal{G}=(S,\Sigma,s_{\mathsf{init}},(\Sigma_{p})_{p\in P},\delta)$ is turn-based iff for all states $s\in S$, there is a unique player $p$ s.t. the successors of $s$ depend only on $p$’s choice of action, i.e., $\mathrm{Succ}(s,a)$ contains exactly one state for all $a\in\Sigma_{p}(s)$.

A history is a finite path $h=s_{1}s_{2}\ldots s_{k}\in S^{*}$ s.t.

(i) $k\in\mathbb{N}$;

(ii) $s_{1}=s_{\mathsf{init}}$; and

(iii) for every $2\leq i\leq k$, there exists $(a_{1},\ldots,a_{n})\in\Sigma^{|P|}$ with $s_{i}=\delta(s_{i-1},a_{1},\ldots,a_{n})$.

The length $|h|$ of a history $h=s_{1}s_{2}\ldots s_{k}$ is its number of states $k$; for every $1\leq i\leq k$, we denote by $h_{i}$ the state $s_{i}$ and by $h_{\leq i}$ the history $s_{1}s_{2}\ldots s_{i}$. We denote by $\mathrm{last}(h)$ the last state of $h$, that is, $\mathrm{last}(h)=h_{|h|}$. A run is defined similarly as a history except that its length is infinite. For a run $\rho=s_{1}s_{2}\ldots\in S^{\omega}$ and $i\in\mathbb{N}$, we also write $\rho_{\leq i}=s_{1}s_{2}\ldots s_{i}$ and $\rho_{i}=s_{i}$. Let $\texttt{Hist}(\mathcal{G})$ (resp. $\texttt{Runs}(\mathcal{G})$) denote the set of histories (resp. runs) of $\mathcal{G}$. The game is played from the initial state $s_{\mathsf{init}}$ for an infinite number of rounds, producing a run. At each round $i\geq 0$, with current state $s_{i}$, all players $p$ select simultaneously a action $a^{i}_{p}\in\Sigma_{p}(s_{i})$, and the state $\delta(s_{i},a^{i}_{1},\ldots,a^{i}_{n})$ is appended to the current history. The selection of the action by a player is done according to strategies defined below.

Randomised moves and strategies

Given a finite set $A$, a probability distribution on $A$, is a function $\alpha:A\to[0,1]$ such that $\sum_{a\in A}\alpha(a)=1$; and we let $\textrm{Supp}(\alpha)=\{a\mid\alpha(a)>0\}$ be the support of $\alpha$. We denote by $\alpha(B)=\sum_{a\in B}\alpha(a)$ the probability of a given set $B$ according to $\alpha$. The set of probability distributions on $A$ is denoted by $\mathcal{D}(A)$. A randomised move of player $p$ in state $s$ is a probability distribution on $\Sigma_{p}(s)$, that is, an element of $\mathcal{D}(\Sigma_{p}(s))$. A randomised move that assigns probability $1$ to an action and [math] to the others is called a Dirac move. We will henceforth denote randomised moves as sums of actions weighted by their respective probabilities. For instance $0.5f+0.5g$ denotes the randomised move that assigns probability $0.5$ to $f$ and $g$ (and [math] to all other actions). In particular, we denote by $b$ a Dirac move that assigns probability $1$ to action $b$.

Given a state $s$ and a tuple $\bm{\beta}=(\beta_{p})_{p\in P}\in\prod_{p\in P}\mathcal{D}(\Sigma_{p}(s))$ of randomised moves from $s$, one per player, we let $\delta_{r}(s,\bm{\beta})\in\mathcal{D}(S)$ be the probability distribution on states s.t. for all $s^{\prime}\in S$: $\delta_{r}(s,\bm{\beta})(s^{\prime})=\sum_{\bm{a}\mid\delta(s,\bm{a})=s^{\prime}}\bm{\beta}(\bm{a})$, where $\bm{\beta}(a_{1},\ldots,a_{n})=\prod_{i=1}^{n}\beta_{i}(a_{i})$. Intuitively, $\delta_{r}(s,\bm{\beta})(s^{\prime})$ is the probability to reach $s^{\prime}$ from $s$ when the players play according to $\bm{\beta}$.

A strategy for player $p$ is a function $\sigma$ from histories to randomised moves (of player $p$) such that, for all $h\in\texttt{Hist}(\mathcal{G})$: $\sigma(h)\in\mathcal{D}(\Sigma_{p}(\mathrm{last}(h)))$. A strategy is called Dirac at history $h$, if $\sigma(h)$ is a Dirac move; it is called Dirac if it is Dirac in all histories. We denote by $\Gamma_{p}(\mathcal{G})$ the set of player-$p$ strategies in the game, and by $\Gamma^{{\it det}}_{p}(\mathcal{G})$ the set of player-$p$ strategies that only use Dirac moves (those strategies are also called deterministic); we might omit $\mathcal{G}$ if it is clear from context. A strategy profile ${\bm{\sigma}}$ for a subset $A\subseteq P$ of players is a tuple $({\bm{\sigma}}_{p})_{p\in A}$ with ${\bm{\sigma}}_{p}\in\Gamma_{p}$ for all $p\in A$. When the set of players $A$ is omitted, we assume $A=P$. Let ${\bm{\sigma}}=({\bm{\sigma}}_{p})_{p\in P}$ be a strategy profile. Then, for all players $p$, we let ${\bm{\sigma}}_{-p}$ denote the restriction of ${\bm{\sigma}}$ to $P\setminus\{p\}$ (hence, ${\bm{\sigma}}_{-p}$ can be regarded as a strategy of player $-p$ that returns, for all histories $h$, a randomised move from $\prod_{p\in P\setminus\{p\}}\mathcal{D}(\Sigma_{p}(s))\subseteq\mathcal{D}(\Sigma_{-p}(\mathrm{last}(h)))$). We sometimes denote ${\bm{\sigma}}$ by the pair $({\bm{\sigma}}_{p},{\bm{\sigma}}_{-p})$. Given a history $h$, we let $({\bm{\sigma}}_{p})_{p\in A}(h)=({\bm{\sigma}}_{p}(h))_{p\in A}$.

Let $h$ be a history and let $\rho$ be a history or a run. Then, we write $h\subseteq_{\mathsf{pref}}\rho$ iff $h$ is a prefix of $\rho$, i.e., $\rho_{\leq|h|}=h$. Consider two strategies $\sigma$ and $\sigma^{\prime}$ for player $p$, and a history $h$. We denote by $\sigma\langle h\leftarrow\sigma^{\prime}\rangle$ the strategy that follows strategy $\sigma$ and shifts to $\sigma^{\prime}$ as soon as $h$ has been played. Formally, $\sigma\langle h\leftarrow\sigma^{\prime}\rangle$ is the strategy s.t., for all histories $h^{\prime}$: $\sigma\langle h\leftarrow\sigma^{\prime}\rangle(h^{\prime})=\sigma^{\prime}(h^{\prime})$ if $h\subseteq_{\mathsf{pref}}h^{\prime}$; and $\sigma\langle h\leftarrow\sigma^{\prime}\rangle(h^{\prime})=\sigma(h^{\prime})$ otherwise.

Probability measure and outcome of a profile

Given a history $h$, we let $\textrm{Cyl}(h)=\{\rho\mid h\subseteq_{\mathsf{pref}}\rho\}$ be the cylinder of $h$. To each strategy profile ${\bm{\sigma}}$, we associate a probability measure $\mathbb{P}_{{\bm{\sigma}}}$ on certain sets of runs. First, for a history $h$, we define $\mathbb{P}_{\bm{\sigma}}(\textrm{Cyl}(h))$ inductively on the length of $h$: $\mathbb{P}_{\bm{\sigma}}(\textrm{Cyl}(s_{\mathsf{init}}))=1$, and $\mathbb{P}_{{\bm{\sigma}}}(\textrm{Cyl}(h^{\prime}s^{\prime}))=\mathbb{P}_{{\bm{\sigma}}}(\textrm{Cyl}(h^{\prime}))\cdot\delta_{r}(\mathrm{last}(h^{\prime}),{\bm{\sigma}}(h^{\prime}))(s^{\prime})$when $|h|>1$ and $h=h^{\prime}s^{\prime}$. Based on this definition, we can extend the definition of $\mathbb{P}_{\bm{\sigma}}$ to any Borel set of runs on cylinders. In particular, the function $\mathbb{P}_{\bm{\sigma}}$ is well-defined for all $\omega$-regular sets of runs, that we will consider in this paper [18]. We extend the Hist notation and let $\texttt{Hist}({\bm{\sigma}})$ be the set of histories $h$ such that $\mathbb{P}_{{\bm{\sigma}}}(\textrm{Cyl}(h))>0$. Given a profile ${\bm{\sigma}}$ we denote by $\texttt{Outcome}({\bm{\sigma}})$ the set of runs $\rho$ s.t. all prefixes $h$ of $\rho$ belong to $\texttt{Hist}({\bm{\sigma}})$. In particular, $\mathbb{P}_{{\bm{\sigma}}}(\texttt{Outcome}({\bm{\sigma}}))=1$. Note that when ${\bm{\sigma}}$ is composed of Dirac strategies then $\texttt{Outcome}({\bm{\sigma}})$ is a singleton. The outcome (set of histories) of a strategy $\sigma\in\Gamma_{p}$, denoted by $\texttt{Outcome}(\sigma)$ ($\texttt{Hist}(\sigma)$), is the union of outcomes (set of histories, respectively) of profile ${\bm{\sigma}}$ s.t. ${\bm{\sigma}}_{p}=\sigma$.

Winning conditions

To determine the gain of all players in the game $\mathcal{G}$, we define winning conditions that can be interpreted with two kinds of semantics denoted by the symbols S for the sure semantics or and A for the almost sure semantics. A winning condition $\Phi$ is a subset of $\texttt{Runs}(\mathcal{G})$ called winning runs. From now on, we assume that concurrent games are equipped with a function $\Phi$, called the winning condition, and mapping all players $p\in P$ to a winning condition $\Phi(p)$. A profile ${\bm{\sigma}}$ is A-winning for $\Phi(p)$ if $\mathbb{P}_{{\bm{\sigma}}}(\Phi)=1$ which we write $\mathcal{G},{\bm{\sigma}}\models^{\texttt{A}}\Phi(p)$. A profile ${\bm{\sigma}}$ is S-winning for $\Phi(p)$ if $\texttt{Outcome}(\mathcal{G},{\bm{\sigma}})\subseteq\Phi(p)$ which we write $\mathcal{G},{\bm{\sigma}}\models^{\texttt{S}}\Phi(p)$. Note that when ${\bm{\sigma}}$ is Dirac, the two semantics coincide: $\mathcal{G},{\bm{\sigma}}\models^{\texttt{S}}\Phi(p)$ iff $\mathcal{G},{\bm{\sigma}}\models^{\texttt{A}}\Phi(p)$. The profile ${\bm{\sigma}}$ is A-winning from $h$ if $h\in\texttt{Hist}(\mathcal{G},{\bm{\sigma}})$ and $\mathbb{P}_{{\bm{\sigma}}}(\Phi(p)\mid\textrm{Cyl}(h))=\mathbb{P}_{{\bm{\sigma}}}(\Phi(p)\cap\textrm{Cyl}(h))/\mathbb{P}_{{\bm{\sigma}}}(\textrm{Cyl}(h))=1$ which we denote $\mathcal{G},{\bm{\sigma}}\models^{\texttt{A}}_{h}\Phi(p)$. The profile ${\bm{\sigma}}$ is winning for the sure semantics from $h$ if $\{\rho\in\texttt{Outcome}(\mathcal{G},{\bm{\sigma}})\mid h\subseteq_{\mathsf{pref}}\rho\}\subseteq\Phi(p)$, which we denote $\mathcal{G},{\bm{\sigma}}\models^{\texttt{S}}_{h}\Phi(p)$. We often omit $\mathcal{G}$ in notations when clear from the context. Most of our definitions and results hold for both semantics and we often state them using the symbol $\star\in\{\texttt{S},\texttt{A}\}$ as in the following definition. Given a semantics $\star\in\{\texttt{S},\texttt{A}\}$, a strategy $\sigma$ for player $p$ (from a history $h$) is called $\star$-winning for player $p$ if for every $\tau\in\Gamma_{-p}$, the profile $(\sigma,\tau)$ is $\star$-winning for player $p$ (from $h$). Note that a strategy $\sigma$ for player $p$ is S-winning iff $\texttt{Outcome}(\sigma)\subseteq\Phi(p)$. We often describe winning conditions using standard linear temporal operators $\Box$ and $\Diamond$; e.g. $\Box\Diamond S$ means the set of runs that visit infinitely often $S$. See [3] for a formal definition.

A winning condition $\Phi(p)$ is prefix-independent if for all $s_{1}s_{2}\ldots\in\Phi(p)$, and all $i\geq 1$: $s_{i}s_{i+1}\ldots\in\Phi(p)$. When $\Phi(p)$ contains all runs that do not visit some designated set $\mathsf{Bad}_{p}\subseteq S$ of states, we say that $\Phi(p)$ is a safety condition. A safety game is a game whose winning condition $\Phi$ is such that $\Phi(p)$ is a safety condition for all players $p$. Without loss of generality, we assume that safety games are so-called simple safety games: a safety game $(S,\Sigma,s_{\mathsf{init}},(\Sigma_{p})_{p\in P},\delta)$ is simple iff for all players $p$, for all $s\in S$: $s\in\mathsf{Bad}_{p}$ implies that no $s^{\prime}\not\in\mathsf{Bad}_{p}$ is reachable from $s$. That is, once the safety condition is violated, then it remains violated forever at all future histories.

We note the following property of winning strategies.

Lemma 1**.**

Given $\star\in\{\texttt{S},\texttt{A}\}$, ${\bm{\sigma}}\models^{\star}\Phi(p)$ iff ${\bm{\sigma}}\models^{\star}_{h}\Phi(p)$ for every $h\in\texttt{Hist}({\bm{\sigma}})$.

Proof.

The only non-trivial implication is: if ${\bm{\sigma}}\models^{\texttt{A}}\Phi(p)$ then ${\bm{\sigma}}\models^{\texttt{A}}_{h}\Phi(p)$ for every $h\in\texttt{Hist}({\bm{\sigma}})$ which we show by contraposition. Assume there exists $h\in\texttt{Hist}({\bm{\sigma}})$ such that ${\bm{\sigma}}\not\models^{\texttt{A}}_{h}\Phi(p)$. This means that $\mathbb{P}_{{\bm{\sigma}}}(\textrm{Cyl}(h))>0$ and $\mathbb{P}_{{\bm{\sigma}}}(\Phi(p)\cap\textrm{Cyl}(h))/\mathbb{P}_{{\bm{\sigma}}}(\textrm{Cyl}(h))<1$. It follows that ${\bm{\sigma}}\not\models^{\texttt{A}}_{h}\Phi(p)$. ∎

Example 1**.**

*Let us consider three player-$1$ strategies in Fig. 2.

(i) $\sigma_{1}$is any strategy that plays $a$ in $s_{0}$;

(ii) $\sigma_{2}$is any strategy that plays $b$ in $s_{0}$, $d$ in $s_{1}$ and $f$ in $s_{2}$; and

(iii) $\sigma_{3}$is any strategy that plays $b$ in $s_{0}$, $d$ in $s_{1}$, and $0.5f+0.5g$ in $s_{2}$.

Clearly, $\sigma_{1}$ never allows one to reach $\mathsf{Trg}$ while some runs respecting $\sigma_{2}$ and $\sigma_{3}$ do (remember that there is no $\star$-winning strategy in this game). We will see later that the best choice of player $1$ (among $\sigma_{2}$, $\sigma_{3}$) depends on the semantics we consider. In the almost-sure semantics, $\sigma_{3}$ is ‘better’ for player $1$, because $\sigma_{3}$ is an A-winning strategy from all histories ending in $s_{2}$, while $\sigma_{2}$ is not. On the other hand, in the sure semantics, playing $\sigma_{2}$ is ’better’ for player $1$ than $\sigma_{3}$. Indeed, for all player-$2$ strategies $\tau$, either $\texttt{Outcome}(\sigma_{3},\tau)$ contains only runs that do not reach $s_{2}$, or $\texttt{Outcome}(\sigma_{3},\tau)$ contains at least a run that reaches $s_{2}$, but, in this case, it also contains a run of the form $hs_{2}^{\omega}$ (because, intuitively, player $1$ plays both $f$ and $g$ from $s_{2}$). So, $\sigma_{3}$ is not winning against any $\tau$, while $\sigma_{2}$ wins at least against a player $2$ strategy that plays $b^{\prime}$ in $s_{0}$, $d^{\prime}$ in $s_{1}$ and $f^{\prime}$ in $s_{2}$. We formalise these intuitions in the next section.*

3 Admissibility

In this section, we define the central notion of the paper: admissibility [4, 8]. Intuitively, a strategy is admissible when it plays ‘as well as possible’. Hence the definition of admissible strategies is based on a notion of domination between strategies: a strategy $\sigma^{\prime}$ dominates another strategy $\sigma$ when $\sigma^{\prime}$ wins every time $\sigma$ does. Obviously, players have no interest in playing dominated strategies, hence admissible strategies are those that are not dominated. Apart from these (classical) definitions, we characterise admissible strategies as those that satisfy two weaker notions: they must be both strongly cooperative optimal and play only locally-admissible moves. Finally, we discuss important characteristics of admissible strategies that will enable us to perform assume-admissible synthesis (see Section 4).

In this section, we fix a game $\mathcal{G}$, a player $p$, and, following our previous conventions, we denote by $\Gamma_{-p}$ the set $\{{\bm{\sigma}}_{-p}\mid{\bm{\sigma}}\in\Gamma\}$.

Admissible strategies

We first recall the classical notion of admissible strategy [4, 1]. Given two strategies $\sigma,\sigma^{\prime}\in\Gamma_{p}$, we say that $\sigma$ is $\star$-weakly dominated by $\sigma^{\prime}$, denoted $\sigma\preccurlyeq^{\star}\sigma^{\prime}$, if for all $\tau\in\Gamma_{-p}$: $(\sigma,\tau)\models^{\star}\Phi(p)$ implies $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. This indeed captures the idea that $\sigma^{\prime}$ is not worse that $\sigma$, because it wins (for $p$) every time $\sigma$ does. Note that $\preccurlyeq^{\star}$ is not anti-symmetric, hence we note $\sigma\approx^{\star}\sigma^{\prime}$ when $\sigma$ and $\sigma^{\prime}$ are equivalent, i.e. $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ and $\sigma^{\prime}\preccurlyeq^{\star}\sigma$. In other words $\sigma\approx^{\star}\sigma^{\prime}$ iff for every $\tau\in\Gamma_{-p}$, $(\sigma,\tau)\models^{\star}\Phi(p)\Leftrightarrow(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. When $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ but $\sigma^{\prime}\not\preccurlyeq^{\star}\sigma$ we say that $\sigma$ is $\star$-dominated by $\sigma^{\prime}$, and we write $\sigma\prec^{\star}\sigma^{\prime}$. Observe that $\sigma\prec^{\star}\sigma^{\prime}$ holds if and only if $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ and there exists at least one $\tau\in\Gamma_{-p}$, such that $(\sigma,\tau)\not\models^{\star}\Phi(p)$ and $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. That is, $\sigma^{\prime}$ is now strictly better than $\sigma$. Then, a strategy $\sigma$ is $\star$-admissible iff there is no strategy $\sigma^{\prime}$ s.t. $\sigma\prec^{\star}\sigma^{\prime}$, i.e., $\sigma$ is $\star$-admissible iff it is not $\star$-dominated.

Example 2**.**

Let us continue our running example, by formalising the intuitions we have sketched in Example 1. Since $\sigma_{1}$ does not allow to reach the target, while some runs respecting $\sigma_{2}$ and $\sigma_{3}$ do, we have: $\sigma_{1}\prec^{\star}\sigma_{2}$ and $\sigma_{1}\prec^{\star}\sigma_{3}$. Moreover, $\sigma_{2}\prec^{\texttt{A}}\sigma_{3}$ because $\sigma_{3}$ is A-winning from any history that ends in $s_{2}$ while $\sigma_{2}$ is not because it does not A-win against a player $2$ strategy that would always play $g^{\prime}$ in $s_{2}$ (and both strategies behave the same way in $s_{0}$ and $s_{1}$). On the other hand, $\sigma_{3}\prec^{\texttt{S}}\sigma_{2}$. In fact, $\texttt{Outcome}(\sigma_{2})\subsetneq\texttt{Outcome}(\sigma_{3})$, so, for all $\tau\in\Gamma_{2}$, whenever $(\sigma_{3},\tau)\models^{\texttt{S}}\Phi(1)$, all runs of $\texttt{Outcome}(\sigma_{3})$ reach $\mathsf{Trg}$, and we also have $(\sigma_{2},\tau)\models^{\texttt{S}}\Phi(1)$. Moreover, for the strategy $\tau\in\Gamma_{2}$ that plays $f^{\prime}$ at $s_{2}$, profile $(\sigma_{2},\tau)$ is S-winning but not $(\sigma_{3},\tau)$. We will see later that $\sigma_{3}$ is A-admissible and $\sigma_{2}$ is S-admissible.

Values of histories

Before we discuss strongly cooperative optimal and locally admissible strategies, we associate values to histories. Let $h$ be a history, and $\sigma$ be a strategy of player $p$. Then, the value of $h$ w.r.t. $\sigma$ for semantics $\star\in\{\texttt{S},\texttt{A}\}$ is defined as follows. $\chi_{\sigma}^{\star}(h)=1$ if $\sigma$ is $\star$-winning from $h$; $\chi_{\sigma}^{\star}(h)=0$ if there are $\tau\in\Gamma_{-p}$ and $\tau^{\prime}\in\Gamma_{-p}$ s.t. $(\sigma,\tau)\models^{\star}_{h}\Phi(p)$, and $(\sigma,\tau^{\prime})\not\models^{\star}_{h}\Phi(p)$; and $-1$ otherwise.

Value $\chi_{\sigma}^{\star}(h)=1$ corresponds to the case where $\sigma$ is $\star$-winning for player $p$ from $h$ (thus, against all possible strategies in $\Gamma_{-p}$). When $\chi_{\sigma}^{\star}(h)=0$, $\sigma$ is not $\star$-winning from $h$ (because of $\tau^{\prime}$ in the definition), but the other players can still help $p$ to reach his objective (by playing some $\tau$ s.t. $(\sigma,\tau)\models^{\star}_{h}\Phi(p)$, which exists by definition). Last, $\chi_{\sigma}^{\star}(h)=-1$ when there is no hope for $p$ to $\star$-win, even with the collaboration of the other players. In this case, there is no $\tau$ s.t. $(\sigma,\tau)\models^{\star}_{h}\Phi(p)$. Hence, having $\chi_{\sigma}^{\star}(h)=-1$ is stronger than saying that $\sigma$ is not winning—when $\sigma$ is not winning, we could have $\chi_{\sigma}^{\star}(h)=0$ as well.

We define the value of a history $h$ for player $p$ as the best value he can achieve with his different strategies: $\chi_{p}^{\star}(h)=\max_{\sigma\in\Gamma_{p}}\chi_{\sigma}^{\star}(h)$. Last, for $v\in\{-1,0,1\}$, let $\texttt{Val}^{\star}_{p,v}$ be the set of histories $h$ s.t. $\chi_{p}^{\star}(h)=v$.

Strongly cooperative optimal strategies

We are now ready to define strongly cooperative optimal (SCO) strategies. Recall that, in the classical setting of turn-based games, admissible strategies are exactly the SCO strategies [8]. We will see that this condition is still necessary but not sufficient in the concurrent setting.

A strategy $\sigma$ of Player $p$ is $\star$-SCO at $h$ iff $\chi_{\sigma}^{\star}(h)=\chi_{p}^{\star}(h)$; and $\sigma$ is $\star$-SCO iff it is $\star$-SCO at all $h\in\texttt{Hist}(\sigma)$. Intuitively, when $\sigma$ is a $\star$-SCO strategy of Player $p$, the following should hold:

(i) if $p$ has a $\star$-winning strategy from $h$ (i.e. $\chi_{p}^{\star}(h)=1$), then, $\sigma$ should be $\star$-winning (i.e. $\chi_{\sigma}^{\star}(h)=1$); and

(ii) otherwise if $p$ has no $\star$-winning strategy from $h$ but still has the opportunity to $\star$-win with the help of other players (hence $\chi_{p}^{\star}(h)=0$), then, $\sigma$ should enable the other players to help $p$ fulfil his objective (i.e. $\chi_{\sigma}^{\star}(h)=0$).

Observe that when $\chi_{p}^{\star}(h)=-1$, no continuation of $h$ is $\star$-winning for $p$, so $\chi_{\sigma}^{\star}(h)=-1$ for all strategies $\sigma$.

Example 3**.**

Consider again the example in Figure 2. For the almost-sure semantics, we have \texttt{Val}^{\texttt{A}}_{p,1}=\big{\{}h\mid\mathrm{last}(h)\in\{s_{2},\mathsf{Trg}\}\big{\}}, and \texttt{Val}^{\texttt{A}}_{p,0}=\big{\{}h\mid\mathrm{last}(h)\in\{s_{0},s_{1}\}\big{\}}. For the sure semantics, we have: $\texttt{Val}^{\texttt{S}}_{1,1}=\{h\mid\mathrm{last}(h)=\mathsf{Trg}\}$, and $\texttt{Val}^{\texttt{S}}_{1,0}=\{h\mid\mathrm{last}(h)\neq\mathsf{Trg}\}$. Let us Consider again the three strategies $\sigma_{1}$, $\sigma_{2}$ and $\sigma_{3}$ from Example 1. We see that $\sigma_{2}$ is S-SCO but it is not A-SCO because, for all profiles $h$ ending in $s_{2}$: $\chi_{\sigma_{2}}^{\texttt{A}}(h)=0$ while $h\in\texttt{Val}^{\texttt{A}}_{1,1}$. On the other hand, $\sigma_{3}$ is A-SCO; but it is not S-SCO. Indeed, one can check that, for all strategies $\tau\in\Gamma_{2}$: if $\texttt{Outcome}(\sigma_{3},\tau)$ contains a run reaching $\mathsf{Trg}$, then it also contains a run that cycles in $s_{2}$. So, for all such strategies $\tau$, $\texttt{Outcome}(\sigma_{3},\tau)\not\models^{\texttt{S}}\Phi(1)$, hence $\chi_{\sigma_{3}}^{\texttt{S}}(h)=-1$ for all histories that end in $s_{2}$; while $\chi_{p}^{\texttt{S}}(h)=0$ since $\chi_{\sigma^{\prime}}^{\texttt{S}}(h)=0$ for all Dirac strategies $\sigma^{\prime}$.

*Next, let us build a strategy $\sigma_{3}^{\prime}$ that is A-dominated by $\sigma_{3}$ (hence, not A-admissible), but A-SCO. We let $\sigma_{3}^{\prime}$ play as $\sigma_{3}$ except that $\sigma_{3}^{\prime}$ plays $c$ the first time $s_{1}$ is visited (hence ensuring that the self-loop on $s_{1}$ will be taken after the first visit to $s_{1}$). Now, $\sigma_{3}$ is A-dominated by $\sigma_{3}^{\prime}$, because

(i) $\sigma_{3}$A-wins every time $\sigma_{3}^{\prime}$ does; but

(ii) $\sigma_{3}^{\prime}$does not A-win against the player $2$ strategy $\tau$ that plays $d^{\prime}$ only when $s_{1}$ is visited for the first time, while $\sigma_{3}$ A-wins against $\tau$.

However, $\sigma_{3}^{\prime}$ is SCO because playing $c$ keeps the value of the history equal to $0=\chi_{1}^{\texttt{A}}(h)$ (intuitively, playing $c$ once does not prevent the other players from helping in the future). As similar example can be built in the S semantics. Thus, there are $\star$-SCO strategies which are not admissible, so, being $\star$-SCO is not a sufficient criterion for admissibility.*

Locally admissible moves and strategies

Let us now discuss another criterion for admissibility, which is more local in the sense that it is based on a domination between moves available to each player after a given history. Let $h$ be a history, and let $\alpha$ and $\alpha^{\prime}$ be two randomised moves in $\mathcal{D}(\Sigma_{p})$. We say that $\alpha$ is $\star$-weakly dominated at $h$ by $\alpha^{\prime}$ (denoted $\alpha\leqslant^{\star}_{h}\alpha^{\prime}$) iff for all $\sigma\in\Gamma_{p}$ such that $h\in\texttt{Hist}(\sigma)$ and $\sigma(h)=\alpha$, there exists $\sigma^{\prime}\in\Gamma_{p}$ s.t. $\sigma^{\prime}(h)=\alpha^{\prime}$ and $\sigma\preccurlyeq^{\star}\sigma^{\prime}$. Observe that the relation $\leqslant^{\star}_{h}$ is not anti-symmetric. We let $\simeq^{\star}_{h}$ be the equivalence relation s.t. $\alpha\simeq^{\star}_{h}\beta$ iff $\alpha\leqslant^{\star}_{h}\beta$ and $\beta\leqslant^{\star}_{h}\alpha$. When $\alpha\leqslant^{\star}_{h}\alpha^{\prime}$ but $\alpha^{\prime}\not\leqslant^{\star}_{h}\alpha$ we say that $\alpha$ is $\star$-dominated at $h$ by $\alpha^{\prime}$ and denote this by $\alpha<^{\star}_{h}\alpha^{\prime}$. When a randomised move $\alpha$ is not $\star$-dominated at $h$, we say that $\alpha$ is $\star$-admissible at $h$. This allows us to define a more local notion of dominated strategy: a strategy $\sigma$ of player $p$ is $\star$-locally-admissible (LA) if $\sigma(h)$ is a $\star$-admissible move at $h$, for all histories $h$.

Example 4**.**

Consider the Dirac move $f$ and the non-Dirac move $0.5f+0.5g$ played from $s_{2}$ in the example in Figure 2. One can check that $0.5f+0.5g<^{\texttt{S}}_{s_{2}}f$. Indeed, consider a strategy $\sigma$ s.t. $\sigma(h)=0.5f+0.5g$ for some $h$ with $\mathrm{last}(h)=s_{2}$. Then, playing $\sigma(h)$ from $h$ will never allow Player 1 to reach $\mathsf{Trg}$ surely at the next step, whatever Player 2 plays; while playing, for instance, $f$ (Dirac move) ensures player 1 to reach $\mathsf{Trg}$ surely at the next step, against a Player-2 strategy that plays $f^{\prime}$. Thus, $\sigma_{2}$ is S-LA but $\sigma_{3}$ is not.

On the other hand, after every randomised move played in state $s_{2}$, the updated state is $s_{2}$ or $s_{3}$ from which A-winning strategies exist, thus $f\simeq^{\texttt{A}}_{h}g\simeq^{\texttt{A}}_{h}\lambda f+(1-\lambda)g$ for all $\lambda\in[0,1]$ and all histories $h$ s.t. $\mathrm{last}(h)=s_{2}$ (so, in particular, $\lambda f+(1-\lambda)g\leqslant^{\texttt{A}}_{h}f$ and $\lambda f+(1-\lambda)g\leqslant^{\texttt{A}}_{h}g$). It follows that both $\sigma_{2}$ and $\sigma_{3}$ are A-LA. However, in the long run, player 1 needs to play $\lambda f+(1-\lambda)g$, with $\lambda\in(0,1)$, infinitely often in order to A-win. In fact, $\sigma_{3}$ is A-winning from $s_{2}$ while $\sigma_{2}$ is not. Thus, there are $\star$-LA strategies which are not admissible, so being $\star$-LA is not a sufficient criterion for $\star$-admissibility.

We close this section by several lemmata that allow us to better characterise the notion of LA strategies. First, we observe that, while randomisation might be necessary for winning in certain concurrent games (for example, in Figure 2, no Dirac move allows player 1 to reach $\mathsf{Trg}$ surely from $s_{2}$, while playing repeatedly $f$ and $g$ with equal probability ensures to reach $\mathsf{Trg}$ with probability 1) randomisation is useless when a player wants to play only locally admissible moves. This is shown by the next Lemma (point (i)), saying that, if a randomised move $\alpha$ plays some action $a$ with some positive probability, then $\alpha$ is dominated by the Dirac move $a$. However, this does not immediately allow us to characterise admissible moves: some Dirac moves could be dominated (hence non-admissible), and some non-Dirac moves could be admissible too. Points (ii) and (iii) elucidate this: among Dirac moves, the non-dominated ones are admissible, and a non-Dirac move is admissible iff all the Dirac moves that occur in its support are admissible and equivalent to each other.

Lemma 2**.**

For all histories $h$ and all randomised moves $\alpha$:

1. (i)

For all $a\in\textrm{Supp}(\alpha)$: $\alpha\leqslant^{\star}_{h}a$; 2. (ii)

Dirac moves that are not $\star$-dominated at $h$ by another Dirac move are admissible; 3. (iii)

*A move $\alpha$ is $\star$-LA at $h$ iff, for all $a\in\textrm{Supp}(\alpha)$: *

(1) $a$*is $\star$-LA at $h$; and * (2) $a\simeq^{\star}_{h}b$*for all $b\in\textrm{Supp}(\alpha)$. * **

Proof.

Proof of (i): Take a strategy $\sigma\in\Gamma_{p}$ such that $h\in\texttt{Hist}(\sigma)$ and $\sigma(h)=\alpha$. Define $\sigma^{\prime}$ the strategy that plays as $\sigma$ except in $h$ where it plays $a$ instead of $\alpha$. One show that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$. Consider any $\tau\in\Gamma_{-p}$ such that $(\sigma,\tau)\models^{\texttt{A}}_{h}\Phi(p)$. This means that $\mathbb{P}_{(\sigma,\tau)}(\Phi(p)\mid\textrm{Cyl}(h))=1$, so, in particular $\mathbb{P}_{(\sigma,\tau)}(\Phi(p)\mid\textrm{Cyl}(h\delta(s,a,\tau(h))))=1$, for all $a\in\textrm{Supp}(\alpha)$. Since $\sigma$ and $\sigma^{\prime}$ are identical in all other histories, including those extending $h\delta(s,a,\tau(h))$, we deduce that $(\sigma^{\prime},\tau)\models^{\texttt{A}}_{h}\Phi(p)$. The proof for the sure semantics is similar.

Proof of (ii): If a Dirac move $a$ is $\star$-dominated at $h$ by a move $\alpha^{\prime}$ then by (i) it is $\star$-dominated at $h$ by a Dirac move $a^{\prime}\in\textrm{Supp}(\alpha^{\prime})$. This shows (ii) by contraposition.

Proof of (iii): Assume $\alpha$ is a $\star$-LA move at $h$. By (i), for every $a\in\textrm{Supp}(\alpha)$, $\alpha\leqslant^{\star}_{h}a$ and $\alpha\not<^{\star}_{h}a$ (because $\alpha$ is a $\star$-LA move at $h$) so $\alpha\simeq^{\star}_{h}a$. Hence all the elements of $\textrm{Supp}(\alpha)$ are equivalent and $\star$-LA at $h$.

Assume now that $\forall a\in\textrm{Supp}(\alpha)$, $a$ is $\star$-LA at $h$ and $\forall b\in\textrm{Supp}(\alpha)$, $a\simeq^{\star}_{h}b$. We take $a\in\textrm{Supp}(\alpha)$. By Lemma 2 it holds that $\alpha\leqslant^{\star}_{\sigma}a$; so it remains to show that $a\leqslant^{\star}_{h}\alpha$. Let $\sigma$ be such that $\sigma(h)=a$. We construct a strategy $\sigma^{\prime}$ such that $\sigma^{\prime}(h)=\alpha$ and $\sigma\preccurlyeq^{\star}\sigma^{\prime}$. For every $b\simeq^{\star}_{h}a$, there exists a strategy $\sigma_{b}$ such that $\sigma_{b}(h)=b$ and $\sigma\preccurlyeq^{\star}\sigma_{b}$. We construct $\sigma^{\prime}$ as follows. We start with $\sigma^{\prime}=\sigma$, we set $\sigma^{\prime}(h)=\alpha$, for every $b\in\textrm{Supp}(\alpha)$ and for every $s^{\prime}\in\mathrm{Succ}(s,b)$, we do $\sigma^{\prime}\leftarrow\sigma^{\prime}\langle hs^{\prime}\leftarrow\sigma_{b}\rangle$. This shows that $a\leqslant^{\star}_{h}\alpha$. We conclude that $\alpha$ is $\star$-LA at $h$. ∎

Example 5**.**

As we have seen in Example 4, $0.5f+0.5g<^{\texttt{S}}_{s_{2}}f$. Note that a strategy $\sigma^{\prime}$ s.t. $\sigma^{\prime}(h)=0.5f+0.5g$ for all $h$ with $\mathrm{last}(h)=s_{2}$ has value $\chi_{\sigma^{\prime}}^{\texttt{S}}(h)=-1$, while $\chi_{1}^{\texttt{S}}(h)=0$.

This example seems to suggest that the local dominance of two moves coincide with the natural order on the values of histories that are obtained when playing those moves (in other words $x<^{\star}_{h}y$ would hold iff the value of the history obtained by playing $x$ is smaller than or equal to the value obtained by playing $y$). This is not true for histories of value [math]: we have seen that $a$ and $b$ are $\leqslant^{\star}_{h}$-incomparable, yet playing $a$ or $b$ from $s_{0}$ yields a history with value [math] in all cases (even when $s_{1}$ is reached). The next Lemma gives a precise characterisation of the dominance relation between Dirac moves in terms of values:

Lemma 3**.**

For all players $p$, histories $h$ with $\mathrm{last}(h)=s$ and Dirac moves $a,b\in\Sigma_{p}(s)$: $a\leqslant^{\star}_{h}b$ if, and only if the following conditions hold for every $c\in\Sigma_{-p}(s)$ where we write $s_{(a,c)}=\delta(s,(a,c))$ and $s_{(b,c)}=\delta(s,(b,c))$:

1. (i)

$\chi_{p}^{\star}(hs_{(a,c)})\leq\chi_{p}^{\star}(hs_{(b,c)})$; 2. (ii)

if $\chi_{p}^{\star}(hs_{(a,c)})=\chi_{p}^{\star}(hs_{(b,c)})=0$ then $s_{(a,c)}=s_{(b,c)}$.

Proof.

Direction $a\leqslant^{\star}_{h}b\Rightarrow$(i)$\wedge$(ii): Assume that $a\leqslant^{\star}_{h}b$. Let $\sigma\in\Gamma_{p}$ such that $h\in\texttt{Hist}(\sigma)$ and $\sigma(h)=a$ and strategy $\sigma^{\prime}\in\Gamma_{p}$ such that $\sigma^{\prime}(h)=b$ and $\sigma\preccurlyeq^{\star}\sigma^{\prime}$.

Proof of (i): We take $c\in\Sigma_{p}(s)$, and show that $\chi_{p}^{\star}(hs_{(a,c)})\leq\chi_{p}^{\star}(hs_{(b,c)})$. For every $\tau\in\Gamma_{-p}$, if $(\sigma,\tau)\models^{\star}\Phi(p)$ then $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. In particular, if $(\sigma,\tau)\models^{\star}_{hs_{(a,c)}}\Phi(p)$ then $(\sigma^{\prime},\tau)\models^{\star}_{hs_{(b,c)}}\Phi(p)$. We deduce that $\sigma^{\prime}$ is winning from $hs_{(b,c)}$ if $\sigma$ is winning from $hs_{(a,c)}$. As $\sigma$ is arbitrary this shows that $\chi_{p}^{\star}(hs_{(a,c)})=1\Rightarrow\chi_{p}^{\star}(hs_{(b,c)})=1$. Dually if $\chi_{p}^{\star}(hs_{(b,c)})=-1$ then $\sigma^{\prime}$ is losing from $hs_{(b,c)}$ and so is $\sigma$ from $hs_{(a,c)}$. This shows the implication $\chi_{p}^{\star}(hs_{(b,c)})=-1\Rightarrow\chi_{p}^{\star}(hs_{(a,c)})=-1$. These two implications yield $\chi_{p}^{\star}(hs_{(a,c)})\leq\chi_{p}^{\star}(hs_{(b,c)})$.

Proof of (ii): We show the contrapositive, consider $c$ such that $s_{(a,c)}\neq s_{(b,c)}$ and show that $\chi_{p}^{\star}(hs_{(a,c)})$ and $\chi_{p}^{\star}(hs_{(b,c)})$ cannot be both equal to [math]. For this purpose we assume that $\chi_{p}^{\star}(hs_{(a,c)})=0$ and show that $\chi_{p}^{\star}(hs_{(b,c)})=1$. Since $\sigma$ is chosen arbitrary we take it such that $\chi_{\sigma}^{\star}(hs_{(a,c)})=\chi_{p}^{\star}(hs_{(a,c)})=0$. In particular there exists $\tau\in\Gamma_{-p}$ such that $(\sigma,\tau)\models^{\star}_{hs_{(a,c)}}\Phi(p)$. Let $\tau^{\prime}$ be an arbitrary player $-p$ strategy. By $\sigma\preccurlyeq^{\star}\sigma^{\prime}$, we have $(\sigma,\tau^{\prime})\models^{\star}\Phi(p)$ implies $(\sigma^{\prime},\tau^{\prime})\models^{\star}\Phi(p)$. Since $\tau^{\prime}\langle hs_{(a,c)}\leftarrow\tau\rangle$ and $\tau^{\prime}$ are equal on histories incomparable to $hs_{(a,c)}$, it then holds that $(\sigma^{\prime},\tau^{\prime})\models^{\star}_{hs_{(b,c)}}\Phi(p)$ for every arbitrary profile $\tau^{\prime}$. We have shown that $\sigma^{\prime}$ is winning from $hs_{(b,c)}$ and hence that $\chi_{p}^{\star}(hs_{(b,c)})=1$ as claimed.

Direction (i)$\wedge$(ii) $\Rightarrow a\leqslant^{\star}_{h}b$: We assume that (i) and (ii) hold and show that $a\leqslant^{\star}_{h}b$. Let $\sigma$ be such that $h\in\texttt{Hist}(\sigma)$ and $\sigma(h)=a$. We define $\sigma^{\prime}$ such that $\sigma^{\prime}(h)=b$ and $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ in several steps. We start with $\sigma^{\prime}=\sigma$. We set $\sigma^{\prime}(h)=b$. For every $s^{\prime}\in\mathrm{Succ}(s,b)\setminus\mathrm{Succ}(s,a)$ we take a strategy $\sigma_{s^{\prime}}$ such that $\chi_{\sigma_{s^{\prime}}}^{\star}(hs^{\prime})=\chi_{p}^{\star}(hs^{\prime}){}$ and update $\sigma^{\prime}$ to $\sigma^{\prime}\langle hs^{\prime}\leftarrow\sigma_{s^{\prime}}\rangle$. For every $s^{\prime}\in\mathrm{Succ}(s,b)\cap\mathrm{Succ}(s,a)$ such that $\chi_{\sigma}^{\star}(hs^{\prime})<\chi_{p}^{\star}(hs^{\prime})$ we do the same operation. Note that for all states $s^{\prime}\in\mathrm{Succ}(s,b)\cap\mathrm{Succ}(s,a)$ such that $\chi_{\sigma}^{\star}(hs^{\prime})=\chi_{p}^{\star}(hs^{\prime})$ the strategies $\sigma^{\prime}$ and $\sigma$ coincide from $hs^{\prime}$. Now we show that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$. We take an arbitrary $\tau\in\Gamma_{-p}$ such that $(\sigma,\tau)\models^{\star}\Phi(p)$ and show that $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. Assume that $h\in\texttt{Hist}(\sigma,\tau)$, otherwise $(\sigma,\tau)$ and $(\sigma^{\prime},\tau)$ behave exactly the same. Let $\gamma=\tau(h)$. We show that $(\sigma^{\prime},\tau)\models^{\star}_{h}\Phi(p)$. This is equivalent to show that $(\sigma^{\prime},\tau)\models^{\star}_{hs_{(b,c)}}\Phi(p)$ for every $c\in\textrm{Supp}(\gamma)$. Let $c\in\textrm{Supp}(\gamma)$. If $s_{(b,c)}=s_{(a,c)}$ and $\chi_{\sigma}^{\star}(hs_{(b,c)})=\chi_{p}^{\star}(hs_{(b,c)})$ then $\sigma$ and $\sigma^{\prime}$ play the same from $hs_{(a,c)}=hs_{(b,c)}$ and so $(\sigma^{\prime},\tau)\models^{\star}_{hs_{(b,c)}}\Phi(p)$. If $s_{(b,c)}\neq s_{(a,c)}$ then by (ii) and (i), either $\chi_{p}^{\star}(hs_{(b,c)})=\chi_{p}^{\star}(hs_{(a,c)})=-1$, or $\chi_{p}^{\star}(hs_{(b,c)})=\chi_{p}^{\star}(hs_{(a,c)})=1$, or $\chi_{p}^{\star}(hs_{(b,c)})>\chi_{p}^{\star}(hs_{(a,c)})$. The first case is not possible since $\tau$ witnesses that $\chi_{p}^{\star}(hs_{(a,c)})>0$. In the second case, by construction, we have $\chi_{\sigma^{\prime}}^{\star}(hs_{(b,c)})=1$, thus $(\sigma^{\prime},\tau)\models^{\star}_{hs_{(b,c)}}\Phi(p)$. Assume the third case, which means $\chi_{p}^{\star}(hs_{(b,c)})>\chi_{p}^{\star}(hs_{(a,c)})$. Then $\chi_{\sigma^{\prime}}^{\star}(hs_{(b,c)})=\chi_{p}^{\star}(hs_{(b,c)})>\chi_{p}^{\star}(hs_{(a,c)})\geq 0$ (the first equality is due to the construction of $\sigma^{\prime}$, the last inequality is due to the fact that $(\sigma,\tau)\models^{\star}_{hs_{(a,c)}}\Phi(p)$). We deduce that $\sigma^{\prime}$ is winning from $hs_{(b,c)}$ and hence that $(\sigma^{\prime},\tau)\models^{\star}_{hs_{(b,c)}}\Phi(p)$. This concludes the proof of $(\sigma^{\prime},\tau)\models^{\star}_{h}\Phi(p)$. As $\sigma^{\prime}$ agrees with $\sigma$ on histories for which $h$ is not a prefix, this implies that $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. ∎

Now, we turn our attention to randomised moves in general, and show, again, how the notion of $\star$-LA equivalence between $\star$-LA moves relates to values of histories. Let $h$ be a history ending in $s$, and assume that player 1 has the choice between two randomised moves $\alpha$ and $\beta$ which are $\star$-LA and equivalent ($\alpha\simeq^{\star}_{h}\beta$). Then, the probability of ending up in some state $s^{\prime}$ will be the same by playing $\alpha$ or $\beta$, provided $hs^{\prime}$ has value [math] (for player $p$). A similar property exists for histories of value $1$: the probability of producing a history of value $1$ is the same under $\alpha$ and $\beta$:

Lemma 4**.**

Let $h$ be a history s.t. $\mathrm{last}(h)=s$, and let $\alpha$ and $\beta$ be two randomised moves in $\mathcal{D}(\Sigma_{p}(s))$ s.t. $\alpha\simeq^{\star}_{h}\beta$. Then, for all $\gamma\in\mathcal{D}(\Sigma_{-p}(s))$:

1. (i)

$\delta_{r}(s,(\alpha,\gamma))(s^{\prime})=\delta_{r}(s,(\beta,\gamma))(s^{\prime})$* for all $s^{\prime}$ s.t. $hs^{\prime}\in\texttt{Val}^{\star}_{p,0}$; and* 2. (ii)

$\delta_{r}(s,(\alpha,\gamma))(S_{1})=\delta_{r}(s,(\beta,\gamma))(S_{1})$, with $S_{1}=\{s^{\prime}\mid hs^{\prime}\in\texttt{Val}^{\star}_{p,1}\}$.

Proof.

We first prove the properties for Dirac moves $\alpha=a$ and $\beta=b$ such that $a\simeq^{\star}_{h}b$. By Lemma 3, $\chi^{p}_{h\delta(s,a,c)}=\chi^{p}_{h\delta(s,b,c)}$ for every $c\in\Sigma_{-p}(s)$ and if this value is [math] it further holds that: $\delta(s,a,c)=\delta(s,b,c)$. Then for every $s^{\prime}$ such that $\chi^{p}_{hs^{\prime}}=0$, for every $c\in\textrm{Supp}(\gamma)$, it holds that $\delta_{r}(s,(a,c))(s^{\prime})=\delta_{r}(s,(b,c))(s^{\prime})$. Thus (i) holds when $\alpha=a$ and $\beta=b$ are Dirac moves:

[TABLE]

Next, we know that, for all Dirac moves $c\in\Sigma_{-p}(s)$, $\delta_{r}(s,(a,c))(\delta(s,a,c))=\delta_{r}(s,(b,c))(\delta(s,b,c))=1$, by definition of Dirac moves. We use this to establish point (ii), again when $\alpha=a$ and $\beta=b$ are Dirac moves:

[TABLE]

Notice that the third inequality follows from $a\simeq^{\star}_{h}b$ and Lemma 3, since we have $\{c\mid h\delta(s,a,c)\in\texttt{Val}^{\star}_{p,1}\}=\{c\mid h\delta(s,b,c)\in\texttt{Val}^{\star}_{p,1}\}$.

To finish the proof, we establish both properties for general randomised moves $\alpha$ and $\beta$. We know that $\alpha$’s and $\beta$’s supports are equivalent Dirac moves by Lemma 2. We start by selecting some $b\in\textrm{Supp}(\beta)$, in order to reuse the results above. We have:

[TABLE]

So, summing up:

[TABLE]

However:

[TABLE]

Therefore establishing (i).

Finally, we proceed similarly for $S_{1}$. Again, we start by fixing $b\in\textrm{Supp}(\beta)$. We have:

[TABLE]

So, summing up:

[TABLE]

However,

[TABLE]

Therefore establishing (ii). ∎

Characterisation and existence of admissible

strategies

Equipped with our previous results, we can now establish the main results of this section. First, we show that $\star$-admissible strategies are exactly those that are both $\star$-LA and $\star$-SCO (Theorem 1$(i)$). Then, we show that admissible strategies always exist in concurrent games (Theorem 1$(ii)$).

To establish Theorem 1, we need an ancillary lemma, which relates the notions of $\star$-admissibility and the notions of $\star$-LA. To this end, we draw a link between (global) equivalence of strategies (in terms of $\approx^{\star}$) and the local equivalence of moves (in terms of $\simeq^{\star}_{h}$). For all player $p$ strategies $\sigma$ and all $v\in\{-1,0,1\}$, let us define $\texttt{Hist}_{v}(\sigma)$ as $\texttt{Hist}(\sigma)\cap\texttt{Val}^{\star}_{p,v}$, i.e., the set of histories of $\sigma$ that have value $v$. Then:

Lemma 5**.**

*Let $\sigma$ and $\sigma^{\prime}$ be two player $p$ strategies s.t.:

(i) $\sigma$is $\star$-LA; and

(ii) for all histories $h$: $\chi_{p}^{\star}(h)=1$ implies that $\sigma$ and $\sigma^{\prime}$ are $\star$-winning from $h$.

Then, the following conditions are equivalent:*

1. (1)

$\sigma(h)\simeq^{\star}_{h}\sigma^{\prime}(h)$* for all $h\in\texttt{Hist}(\sigma)\cap\texttt{Hist}(\sigma^{\prime})$;* 2. (2)

$\texttt{Hist}_{0}(\sigma)=\texttt{Hist}_{0}(\sigma^{\prime})$* and $\sigma(h)\simeq^{\star}_{h}\sigma^{\prime}(h)$ for all $h\in\texttt{Hist}_{0}(\sigma)$;* 3. (3)

$\sigma\approx^{\star}\sigma^{\prime}$**

Proof.

Proof of $(\ref{it1:equivstrat})\Rightarrow(\ref{it2:equivstrat})$ : By induction and application of Lemma 4.

Proof of $(\ref{it2:equivstrat})\Rightarrow(\ref{it3:equivstrat})$ We assume that $\forall h\in\texttt{Hist}_{0}(\sigma)=\texttt{Hist}_{0}(\sigma^{\prime})$, $\sigma(h)\simeq^{\texttt{A}}_{h}\sigma^{\prime}(h)$ and show that $\sigma\approx^{\texttt{A}}{}\sigma^{\prime}$.

It suffices to take an arbitrary $\tau\in\Gamma_{-p}$ and show that $\mathbb{P}_{(\sigma,\tau)}(\Phi(p))=1$ iff $\mathbb{P}_{(\sigma^{\prime},\tau)}(\Phi(p))=1$. We first show that:

[TABLE]

This can be shown by induction using Lemma 4 where the base case is $\mathbb{P}_{(\sigma,\tau)}(\textrm{Cyl}(s_{\mathsf{init}}))=1=\mathbb{P}_{(\sigma^{\prime},\tau)}(\textrm{Cyl}(s_{\mathsf{init}}))$ and the induction step is that $\mathbb{P}_{(\sigma,\tau)}(\textrm{Cyl}(h))=\mathbb{P}_{(\sigma^{\prime},\tau)}(\textrm{Cyl}(h))$ implies:

[TABLE]

We decompose the set of runs as $\Box\texttt{Val}^{\star}_{p,0}\biguplus\Diamond\texttt{Val}^{\star}_{p,1}\biguplus\Diamond\texttt{Val}^{\star}_{p,-1}$. When intersecting with $\Phi(p)$, the last set in the union becomes empty and we have:

[TABLE]

Hence for $\sigma^{\prime\prime}\in\{\sigma,\sigma^{\prime}\}$, $\mathbb{P}_{(\sigma^{\prime\prime},\tau)}(\Phi(p))=\mathbb{P}_{(\sigma^{\prime\prime},\tau)}(\Box\texttt{Val}^{\star}_{p,0}\cap\Phi(p))+\mathbb{P}_{(\sigma^{\prime\prime},\tau)}(\Diamond\texttt{Val}^{\star}_{p,1})$ where we used that $\Diamond\texttt{Val}^{\star}_{p,1}$ implies $\Phi(p)$ almost surely because $\sigma^{\prime\prime}$ is winning from histories of value $1$.

Hence it suffices to show that $\mathbb{P}_{(\sigma,\tau)}(\Box\texttt{Val}^{\star}_{p,0}\cap\Phi(p))=\mathbb{P}_{(\sigma^{\prime},\tau)}(\Box\texttt{Val}^{\star}_{p,0}\cap\Phi(p))$ and $\mathbb{P}_{(\sigma,\tau)}(\Diamond\texttt{Val}^{\star}_{p,1})=\mathbb{P}_{(\sigma^{\prime},\tau)}(\Diamond\texttt{Val}^{\star}_{p,1})$. The former equality is due to (3). To prove the latter equality, we write for $\sigma^{\prime\prime}\in\{\sigma,\sigma^{\prime}\}$,

[TABLE]

This equality traduces the decomposition of the even $\texttt{Val}^{\star}_{p,1}$ into the disjoint events parametrised by the history $h$ of value [math] just before entering $\texttt{Val}^{\star}_{p,1}$. Using (4), Lemma 4 and (3) we deduce that $\mathbb{P}_{(\sigma,\tau)}(\Diamond\texttt{Val}^{\star}_{p,1})=\mathbb{P}_{(\sigma^{\prime},\tau)}(\Diamond\texttt{Val}^{\star}_{p,1})$, ending the proof.

**Proof of $(\ref{it3:equivstrat})\Rightarrow(\ref{it1:equivstrat})$: **Straightforward. ∎

Theorem 1** **(Characterisation and existence of admissible

strategies).

The following holds for all strategies $\sigma$ in a concurrent game with semantics $\star\in\{\texttt{S},\texttt{A}\}$:

1. (i)

$\sigma$* is $\star$-admissible iff $\sigma$ is $\star$-LA and $\star$-SCO; in the special case of simple safety objectives, if $\sigma$ is $\star$-LA then $\sigma$ is $\star$-admissible.* 2. (ii)

there is a $\star$-admissible strategy $\sigma^{\prime}$ such that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$.

In particular, point (ii) implies that admissible strategies always exist in concurrent games.

Proof of Theorem 1.

We start with the proof of point (i).

”$\sigma$ is $\star$-admissible” implies ”$\sigma$ is $\star$-SCO”: We show the contrapositive. Let $\sigma$ be a strategy that is not $\star$-SCO, and let us show that $\sigma$ is not $\star$-admissible. Since $\sigma$ is not $\star$-SCO, there is, by definition of $\star$-SCO, a history $h$ s.t. $\chi_{\sigma}^{\star}(h)\neq\chi_{p}^{\star}(h)$. Recall that $\chi_{p}^{\star}(h)=\max_{\sigma^{\prime}}\chi_{\sigma^{\prime}}^{\star}(h)$. Hence, $\chi_{\sigma}^{\star}(h)\neq\chi_{p}^{\star}(h)$ implies that $\chi_{p}^{\star}(h){\mathcal{G}}{\sigma}<\chi_{p}^{\star}(h)$ and that there exists a strategy $\sigma^{\prime}$ s.t. $\chi_{\sigma}^{\star}(h)=\chi_{p}^{\star}(h)$. Consider the strategy $\overline{\sigma}=\sigma\langle h\leftarrow\sigma^{\prime}\rangle$ that plays like $\sigma$ and switches to $\sigma^{\prime}$ after history $h$. We claim that $\sigma\prec^{\star}\overline{\sigma}$. Observe that, by construction: $\chi_{\sigma}^{\star}(h)<\chi_{\overline{\sigma}}^{\star}(h)$. Note also that $\chi_{=}^{h}(\sigma)-1$ is not possible, because this means that all continuations of $h$ are losing for $p$, so it is not possible to have $\overline{\sigma}$ with $\chi_{\sigma}^{\star}(h)<\chi_{\overline{\sigma}}^{\star}(h)$. So we have necessarily $\chi_{=}^{h}(\sigma)0$ and $\chi_{=}^{h}(\overline{\sigma})1$. This means that $\overline{\sigma}$ is winning from $h$ (against all possible strategies of $-p$), while, by definition of $\chi_{\sigma}^{\star}(h)=0$, $\sigma$ is, from $h$, losing for $p$ against at least one strategy of $-p$. Hence, $\sigma\prec^{\star}\overline{\sigma}$ and $\sigma$ is not $\star$-admissible.

”$\sigma$ is $\star$-admissible” implies ”$\sigma$ is $\star$-LA”: We show the contrapositive: we assume that $\sigma$ is not $\star$-LA and show that $\sigma$ is not $\star$-admissible. There exists a history $h\in\texttt{Hist}(\sigma)$ such that $\sigma(h)$ is $\star$-dominated at $h$ by an $\star$-LA move $b$ that can be chosen Dirac by virtue of Lemma 2 (i). There exists $a\in\textrm{Supp}(\sigma(h))$ such that $a<^{\star}_{h}b$ (otherwise all the moves of the support of $\textrm{Supp}(\sigma(h))$ would be equivalent to the $\star$-LA move $b$ and so would be $\alpha$ by Lemma 2 (ii)). We already saw in the proof of Lemma 2 (i), that $\sigma\preccurlyeq^{\star}\sigma_{a}$ where $\sigma_{a}$ is the strategy that plays like $\sigma$ everywhere except in $h$ where it plays $a$ instead of $\alpha$. Then it suffices to show that $\sigma_{a}$ is $\star$-dominated. Using Lemma 3 and notation therein with $a\leqslant^{\star}_{h}b$, we know that for every $c\in\Sigma_{-p}(s)$, $\chi_{p}^{\star}(hs_{(a,c)})\leq\chi_{p}^{\star}(hs_{(b,c)})$ and if $\chi_{p}^{\star}(hs_{(a,c)})=\chi_{p}^{\star}(hs_{(b,c)})=0$ then $s_{(a,c)}=s_{(b,c)}$. Here we can reuse the end of the proof of Lemma 3 to find a strategy $\sigma^{\prime}$ such that $\sigma_{a}\preccurlyeq^{\star}\sigma^{\prime}$ and that satisfies the further properties that it is $\star$-SCO at $hs_{(b,c)}$ for every $c\in\Sigma_{-p}(s)$, and it plays as $h$ in every proper prefix of $h$. It remains to show that there exists a profile $\tau\in\Gamma_{-p}$ such that $(\sigma_{a},\tau)\not\models^{\star}\Phi(p)$ and $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. Using Lemma 3, this time with $\sigma_{a}(h)\not\leqslant^{\star}_{h}a$ we get the existence of a Dirac move $c\in\Sigma_{-p}(s)$ such that $\chi_{p}^{\star}(hs_{(a,c)})<\chi_{p}^{\star}(hs_{(b,c)})$. We define $\tau\in\Gamma_{-p}$ such that $h\in\texttt{Hist}(\sigma_{a},\tau)$, $\tau(h)=c$ and a further property depending on cases described as follows. If $\chi^{p}_{hs_{a}}=-1$ then $\chi^{p}_{hs_{b}}\geq 0$ and we further require that $(\sigma^{\prime},\tau)\models^{\star}_{hs_{b}}\Phi(p)$. If $\chi^{p}_{hs_{a}}=0$ then $\chi^{p}_{hs_{b}}=1$ and we further require that $(\sigma_{a},\tau)\not\models^{\star}_{hs_{a}}\Phi(p)$. In both cases it holds that $(\sigma^{\prime},\tau)\models^{\star}_{hs_{b}}\Phi(p)$ and $(\sigma_{a},\tau)\not\models^{\star}_{hs_{a}}\Phi(p)$. So $(\sigma_{a},\tau)\not\models^{\star}\Phi(p)$ and $(\sigma^{\prime},\tau)\models^{\star}\Phi(p)$. We conclude that $\sigma$ is not $\star$-LA because $\sigma\preccurlyeq^{\star}\sigma_{a}\prec^{\star}\sigma^{\prime}$.

”$\sigma$ is $\star$-SCO and $\star$-LA” implies ”$\sigma$ is $\star$-admissible”: Let $\sigma$ be a strategy that is both $\star$-LA and $\star$-SCO. We show that for every $\sigma^{\prime}$ such that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ implies $\sigma\approx^{\star}\sigma^{\prime}$; which is a way of proving that $\sigma$ is $\star$-Admissible. Let $\sigma^{\prime}\in\Gamma_{p}$ such that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$. We can assume without loss of generality that $\sigma^{\prime}$ is winning from histories of value $1$ (otherwise it suffices to change $\sigma^{\prime}$ so that when a history of value $1$ it switches to a winning strategy from that history). $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ we deduce that $\sigma(h)\leqslant^{\star}_{h}\sigma^{\prime}(h)$ for every $h\in\texttt{Hist}(\sigma)\cap\texttt{Hist}(\sigma^{\prime})$, then $\sigma(h)\simeq_{h}\sigma^{\prime}(h)$ because $\sigma(h)$ is $\star$-LA at $h$. We can apply Lemma 5, and deduce that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$ as required.

In simple safety games: ”$\sigma$ is $\star$-LA” implies ”$\sigma$ is $\star$-admissible”: To establish this case, we prove that, in simple safety games, ”$\sigma$ is $\star$-LA” implies ”$\sigma$ is $\star$-SCO”. This implies that all $\star$-LA strategies are also $\star$-SCO, hence admissible. First, observe that, in the case of simple safety games, the two semantics A and S coincide. Indeed, a winning strategy for the S semantics is also winning for the almost sure semantics. On the other hand, a winning strategy for the almost sure semantics ensures that no prefix generated by the strategy reaches the bad states (otherwise, this prefix would have non-negative measure, and the probability of winning would be $<1$). Hence, a winning strategy for the almost sure semantics is also winning for the sure semantics. So, we can restrict ourselves to the sure semantics in the arguments that follow.

From $\sigma$, we build a new Dirac $\star$-LA strategy $\sigma^{\prime}$, s.t., for all histories $h$, $\sigma^{\prime}(h)$ is an arbitrarily chosen action from $\textrm{Supp}(\sigma(h))$. By Lemma 2, point (iii), $\sigma^{\prime}$ is also $\star$-LA. We claim that $\sigma^{\prime}$ is value-preserving i.e., for all histories $h$: $\chi_{p}^{\texttt{S}}(h)\leq\chi_{p}^{\texttt{S}}(hs)$, for all $s\in\mathrm{Succ}(\mathrm{last}(h),\sigma^{\prime}(h))$ (assuming $\sigma$, and hence $\sigma^{\prime}$, are player $p$ strategies). In other words, by playing $\sigma^{\prime}$, player $p$ never decreases the value of the histories he visits. This value preserving property holds by Lemma 3.

Moreover, since the objective is a simple safety one, it is easy to see that when $\sigma^{\prime}$ is S-winning, then $\sigma$ is S-winning too. So $\sigma^{\prime}$ is dominated by $\sigma$ and it is sufficient to prove that $\sigma^{\prime}$ is admissible to show that $\sigma$ is admissible too.

So, when states of value $1$ are entered, $\sigma^{\prime}$ ensures that they are never left, and $\sigma^{\prime}$ is thus winning from states of value $1$. On the other hand, when a history of value [math] is entered, $\sigma^{\prime}$ will also ensure that only histories of value [math] or $1$ are visited. In both cases, the $\sigma^{\prime}$ is winning because we are considering a safety objective. In particular, if we stay in histories of value [math] forever, the strategy is winning because the bad states are never visited (otherwise, the value of the history would drop to $-1$).

We conclude that $\sigma^{\prime}$ is $\star$-SCO. Since it is also $\star$-LA, $\sigma^{\prime}$ is admissible. Hence, $\sigma$ is admissible too.

Now, we move to the proof of point (ii).

Let $\sigma$ be a strategy for player $p$, we build an admissible strategy that weakly dominates $\sigma$. This proof is similar to the proof of a similar result for SCO strategies in turn based games ([6, Lemma 7]). The strategy $\sigma^{\prime}$ is built dynamically along runs. It plays a winning strategy as soon as the current history begins to be of value $1$. When the history begins to be of value $-1$, there is nothing more to do, the strategy can play arbitrarily. Consider now, runs in which the value is always [math]. The strategy $\sigma^{\prime}$ keeps in memory a wished strategy $\sigma_{h}$ for himself and a wished strategy $\tau_{h}$ of player $-p$ such that $(\sigma_{h},\tau_{h})\models^{\star}_{h}\Phi(p)$. The strategies $\sigma_{h}$ and $\tau_{h}$ are inductively defined as follows. At the beginning, $h=s_{\mathsf{init}}$, $\sigma_{h}$ and $\tau_{h}$ are chosen such that $(\sigma_{h},\tau_{h})\models^{\star}_{h}\Phi(p)$ and such that $\sigma_{h}$ is $h$-admissible. Here and below if $\sigma$ satisfies these properties then the choice $\sigma_{h}=\sigma$ is made by default, otherwise another strategy $\sigma_{h}$ is chosen (and it dominates $\sigma$). After history $h$, $\sigma^{\prime}$ plays $\sigma_{h}(h)$. If after some history $h$ the continuation $hs^{\prime}$ chosen is not in $\texttt{Hist}(\sigma_{h},\tau_{h})$ (this is the case only if player $-p$ plays something else than $\tau_{h}(h)$), then $\sigma_{hs^{\prime}}$ and $\tau_{hs^{\prime}}$ are chosen such that $\sigma_{hs^{\prime}}$ is $hs^{\prime}$-admissible and $(\sigma_{hs^{\prime}},\tau_{hs^{\prime}})\models^{\star}_{hs^{\prime}}\Phi(p)$. Otherwise, if the wished profile is followed then the wished strategy for player $-p$ is left unchanged ($\tau_{hs^{\prime}}=\tau_{h}$); the wished strategy for player $p$ is left unchanged ($\sigma_{hs^{\prime}}=\sigma_{h}$) if $\sigma_{h}$ is $hs^{\prime}$-admissible and otherwise $\sigma_{hs^{\prime}}$ is defined as a strategy that plays an admissible moves in $hs^{\prime}$ and that dominates $\sigma_{h}$. The constructed strategy is $\star$-LA. It is also $\star$-SCO because from every history $h$ of value [math], $(\sigma^{\prime},\tau_{h})\models^{\star}_{h}\Phi(p)$ and from every history of value $1$, $\sigma^{\prime}$ is winning. $\sigma^{\prime}$ plays as $\sigma$ by default or a strategy that dominates $\sigma$. At the end $\sigma^{\prime}$ is an admissible strategy that weakly dominates $\sigma$. ∎

Example 6**.**

We consider again the example in Figure 2, and consider strategies $\sigma_{2}$ and $\sigma_{3}$ as defined in Example 1. Remember that these two strategies do their best to reach $s_{2}$, and that, from $s_{2}$, $\sigma_{2}$ plays deterministically $f$, while $\sigma_{3}$ plays $f$ and $g$ with equal probabilities. From Example 3, we know that $\sigma_{2}$ is S-SCO but not A-SCO; while $\sigma_{3}$ is A-SCO but not S-SCO. Indeed, we have already argued in Example 2 that $\sigma_{2}$ is not A-admissible, and that $\sigma_{3}$ is not S-admissible. However, from Example 4, we know that $\sigma_{2}$ is S-LA and that $\sigma_{3}$ is A-LA. So, by Theorem 1, $\sigma_{2}$ is S-admissible and $\sigma_{3}$ is A-admissible as expected.

Finally, we close the section by a finer characterisation of $\star$-admissible strategies. We show that:

(i) in the sure semantics, there is always an S-admissible strategy that plays Dirac moves only; and

(ii) in the almost-sure semantics, there is always an A-admissible strategy that plays Dirac moves only in histories of values [math] or $-1$.

The difference between the two semantics should not be surprising, as we know already that randomisation is sometimes needed to win (i.e., from histories of value $1$) in the almost sure semantics:

Proposition 1**.**

For all player $p$ strategies $\sigma$ in a concurrent game with $\star\in\{\texttt{S},\texttt{A}\}$:

1. (i)

If $\sigma$ is A-admissible then there exists a strategy $\sigma^{\prime}$ that plays only Dirac moves in histories of value $\leq 0$ such that $\sigma\simeq^{\texttt{A}}\sigma^{\prime}$. 2. (ii)

If $\sigma$ is S-admissible then there exists a Dirac strategy $\sigma^{\prime}$ such that $\sigma\simeq^{\texttt{S}}\sigma^{\prime}$.

Proof.

Take $\sigma$ is A-admissible. We define $\sigma^{\prime}$ as follows. From histories of value $-1$, plays arbitrary Dirac strategies. From histories of value $1$, plays winning strategies. If $\star=\texttt{S}$ we can further requires that such winning strategies are Dirac. If there exists histories of value [math] then necessarily the initial state $s_{\mathsf{init}}$ is such a history and we build $\sigma^{\prime}$ inductively as follows such that $\texttt{Hist}_{0}(\sigma^{\prime})=\texttt{Hist}_{0}(\sigma)$. Consider $h\in\texttt{Hist}_{0}(\sigma)$, then define $\sigma^{\prime}(h)$ to be an arbitrary Dirac move $a\in\textrm{Supp}(\sigma(h))$. Then by Lemma 2 (iii) and the fact that $\sigma(h)$ is $\star$-LA we deduce that $\sigma^{\prime}(h)\simeq^{\star}_{h}\sigma(h)$; The histories of the form $hs^{\prime}$ that are in $\texttt{Hist}_{0}(\sigma^{\prime})$ are exactly those that belongs to $\texttt{Hist}_{0}(\sigma)$ (see Lemma 4). By induction, $\texttt{Hist}_{0}(\sigma^{\prime})=\texttt{Hist}_{0}(\sigma)$ and for every $h\in\texttt{Hist}_{0}(\sigma)$, $\sigma^{\prime}(h)\simeq^{\star}_{h}\sigma(h)$. We can use Lemma 5 and deduce that $\sigma\simeq^{\star}_{h}\sigma^{\prime}$ with $\sigma^{\prime}$ Dirac in histories of value $\leq 0$, and $\leq 1$ when $\star=\texttt{A}$. ∎

4 Assume admissible synthesis

In this section we discuss an assume-admissible synthesis framework for concurrent games. With classical synthesis, one tries and compute winning strategies for all players, i.e., strategies that always win against all possible strategies of the other players. Unfortunately, it might be the case that such unconditionally winning strategies do not exist, as in our example. As explained in the introduction, the assume-admissible synthesis rule relaxes the classical synthesis rule: instead of searching from strategies that win unconditionally, the new rule requires winning against the admissible strategies of the other players. So, a strategy may satisfy the new rule while not winning unconditionally. Nevertheless, we claim that winning against admissible strategies is good enough assuming that the players are rational; if we assume that players only play strategies that are good for achieving their objectives, they will be playing admissible ones.

The general idea of the assume-admissible synthesis algorithm is to reduce the problem (in a concurrent $n$-player game) to the synthesis of a winning strategy in a $2$-player zero-sum concurrent game of imperfect information, in the S-semantics (even when the original assume-admissible problem is in the A-semantics), where the objective of player $1$ is given by an LTL formula. Such games are solvable using techniques presented in [10].

More precisely, from a concurrent game $\mathcal{G}$ in the semantics $\star\in\{\texttt{S},\texttt{A}\}$ and player $p$, we build a game $\mathcal{G}^{\star}_{p}$ with the above characteristics, which is used to decide the assume-admissible synthesis rule. If such a solution exists, our algorithm constructs a witness strategy. For example, the game $\mathcal{G}^{\star}_{1}$ corresponding to the game in Figure 2 is given in Figure 3. The main ingredients for this construction are the following.

(i) In $\mathcal{G}^{\star}_{p}$, the protagonist is player $p$, and the second player is $-p$.

(ii) Although randomisation is needed to win in such games in general, we interpret $\mathcal{G}^{\star}_{p}$ in the S-semantics only. In fact, we have seen that for the protagonist, Dirac moves suffice in states of value [math]; so the only states where he might need randomisation are those of value $1$ (randomisation does not matter if the value is $-1$ since the objective is lost anyway). Hence we define winning condition to be $\Phi(p)\vee\Diamond\texttt{Val}^{\star}_{p,1}$ enabling us to consider only histories of values [math] in $\mathcal{G}^{\star}_{p}$; and thus hiding the parts of the game where randomisation might be needed. We also prove that we can restrict to Dirac strategies for $-p$ when it comes to admissible strategies.

(iii) In order to restrict the strategies to admissible ones, we only allow $\star$-LA moves in $\mathcal{G}^{\star}_{p}$. These moves can be computed by solving classical $2$-player games ([2]) using Lemma 3. For example, in Figure 3, moves $c$ and $c^{\prime}$ are removed since they are not A-LA.

(iv) Last, since $\star$-admissible strategies are those that are both $\star$-LA and $\star$-SCO (see Theorem 1), we also need to ensure that the players play $\star$-SCO. This is more involved than $\star$-LA, as the $\star$-SCO criterion is not local, and requires information about the sequence of actual moves that have been played, which cannot be deduced, in a concurrent game, from the sequence of visited states. So, we store, in the states of $\mathcal{G}^{\star}_{p}$, the moves that have been played by all the players to reach the state. For example, in Figure 3, the state labelled by $s_{1},(b,b^{\prime})$ means that $\mathcal{G}$ has reached $s_{1}$, and that the last actions played by the players were $b$ and $b^{\prime}$ respectively. However, players’ strategies must not depend on this extra information since they do not have access to this information in $\mathcal{G}$ either. We thus interpret $\mathcal{G}^{\star}_{p}$ as a game of imperfect information where all the states labelled by the same state of $\mathcal{G}$ are in the same observation class. Thanks to these constructions, we can finally encode the fact that the players must play $\star$-SCO strategies in the new objective of the games, which will be given as an LTL formula, as we describe below.

To simplify the presentation, we restrict ourselves to prefix independent winning conditions, although the results can be generalised. Also, to ensure we can effectively solve subproblems mentioned above, we consider $\omega$-regular objectives. The values of the histories depend thus only on their last states, i.e. for all pairs of histories $h_{1}$ and $h_{2}$: $\mathrm{last}(h_{1})=\mathrm{last}(h_{2})$ implies that $\chi_{p}^{\star}(h_{1})=\chi_{p}^{\star}(h_{2})$. We thus denote by $\chi_{p}^{\star}(s)$ the value $\chi_{p}^{\star}(h)$ of all histories $h$ s.t. $\mathrm{last}(h)=s$. Last, we assume that a player cannot play the same action from two different states, i.e. $\forall s_{1}\neq s_{2}$, $\Sigma_{s_{1}}(p)\cap\Sigma_{s_{2}}(p)=\emptyset$. Thus, we say that a given move $a$ is $\star$-LA, meaning that $a$ is $\star$-LA from all histories ending in the unique state where $a$ is available.

The game $\mathcal{G}^{\star}_{p}$

Let us now describe precisely the construction of $\mathcal{G}^{\star}_{p}$. Given an $n$-player concurrent game $\mathcal{G}=(S,\Sigma,s_{\mathsf{init}},(\Sigma_{p})_{p\in P},\delta)$ with winning condition $\Phi$ considered under semantics $\star\in\{\texttt{S},\texttt{A}\}$, and given a player $p$, we define the two-player zero-sum concurrent game $\mathcal{G}^{\star}_{p}=(\overline{S},\overline{\Sigma},\overline{s_{\mathsf{init}}},(\overline{\Sigma}_{p},\overline{\Sigma}_{-p}),\overline{\delta})$ where:

(i) $\overline{S}=S\times\overline{\Sigma}^{n}\cup\{\overline{s_{\mathsf{init}}}\}$;

(ii) $\overline{\Sigma}$is the set of Dirac $\star$-LA moves in $\Sigma$;

(iii) $\overline{s_{\mathsf{init}}}=s_{\mathsf{init}}$is the initial state;

(iv) $\overline{\Sigma}_{p}$is such that $\overline{\Sigma}_{p}(s)$ is the set of Dirac $\star$-LA moves of $p$ in $s$, for all $s\in S$;

(v) $\overline{\Sigma}_{-p}$is s.t. for all $s\in S$: $\overline{\Sigma}_{-p}(s)$ is the set of moves $\bm{a}$ of $-p$ in $s$ s.t. for all $q\neq p$, $a_{q}$ is a Dirac $\star$-LA move;

(vi) $\overline{\delta}$updates the state according to $\delta$, remembering the last actions played: $\overline{\delta}(\overline{s_{\mathsf{init}}},\bm{b})=(\delta(s_{\mathsf{init}},\bm{b}),\bm{b})$ and $\overline{\delta}((s,\bm{a}),\bm{b})=(\delta(s,\bm{b}),\bm{b})$ for all $s\in S$.

Note that the game $\mathcal{G}^{\star}_{p}$ depends on whether $\star=\texttt{A}$ or $\star=\texttt{S}$ because the two semantics yield different sets of LA-moves. However, we interpret $\mathcal{G}^{\star}_{p}$ in the sure semantics, so both players can play Dirac strategies only in $\mathcal{G}^{\star}_{p}$.

Let us now explain how we obtain an imperfect information game by defining an observation function $\mathfrak{o}$. Note that histories in $\mathcal{G}^{\star}_{p}$ are of the form: $\overline{h}=\overline{s_{\mathsf{init}}}(s_{1},\bm{a}_{1})(s_{2},\bm{a}_{2})\cdots(s_{n},\bm{a}_{n})$. Then, let $\mathfrak{o}:\overline{S}\to S$ be the mapping that, intuitively, projects moves away from states. For example, in Figure 3, states with observation $s_{0}$ are in the dashed rectangle. That is: $\mathfrak{o}(s,\bm{a})=s$ for all states $s$, and $\mathfrak{o}(\overline{s_{\mathsf{init}}})=s_{\mathsf{init}}$. We extend $\mathfrak{o}$ to histories recursively: $\mathfrak{o}(\overline{s_{\mathsf{init}}})=s_{\mathsf{init}}$ and $\mathfrak{o}(h(s_{n},\bm{a}_{n}))=\mathfrak{o}(h)s_{n}$. To make $\mathcal{G}^{\star}_{p}$ a game of imperfect information, we request that, in $\mathcal{G}^{\star}_{p}$, players play only strategies $\sigma$ s.t. $\sigma(h_{1})=\sigma(h_{2})$ whenever $\mathfrak{o}(h_{1})=\mathfrak{o}(h_{2})$.

We relate the strategies in the original game $\mathcal{G}$ with the strategies in $\mathcal{G}^{\star}_{p}$, which we need to extract admissible strategies in $\mathcal{G}$ from the winning strategies in $\mathcal{G}^{\star}_{p}$ and thus perform assume-admissible synthesis. First, given a player $p$ strategy $\sigma$ in $\mathcal{G}$ (i.e., $\sigma\in\Gamma_{p}(\mathcal{G})$), we say that a strategy $\overline{\sigma}\in\Gamma^{\textrm{det}}_{p}(\mathcal{G}^{\star}_{p})$ is a realisation of $\sigma$ iff:

(i) $\overline{\sigma}$is Dirac; and

(ii) $\overline{\sigma}(h)\in\textrm{Supp}(\sigma(h)))$for all $h$.

Note that every $\star$-LA strategy $\sigma\in\Gamma_{i}(\mathcal{G})$ admits realisations $\sigma$ in $\Gamma_{i}(\mathcal{G}^{\star}_{p})$. Second, given a player $p$ Dirac strategy $\sigma$ in $\mathcal{G}^{\star}_{p}$ (i.e., $\sigma\in\Gamma^{\textrm{det}}_{p}(\mathcal{G}^{\star}_{p})$) we say that $\hat{\sigma}\in\Gamma_{p}(\mathcal{G})$ is an extension of $\sigma$ iff, for all $h\in\texttt{Hist}(\mathcal{G}^{\star}_{p},\sigma)$: $\hat{\sigma}(\mathfrak{o}(h))=\sigma(h)$.

The assume-admissible synthesis technique

As explained above, the assume-admissible rule boils down to computing a winning strategy $\overline{\sigma}$ for player $p$ in $\mathcal{G}^{\star}_{p}$ w.r.t. to winning condition $\Phi_{\mathcal{G}^{\star}_{p}}$, and extracting, from $\overline{\sigma}$, the required admissible strategy in $\mathcal{G}$.

We will now formally define $\Phi_{\mathcal{G}^{\star}_{p}}$. Let $p$ be a player (in $\mathcal{G}$); and let us denote by $\mathsf{st}(a)$ the (unique) state from which $a$ is available, for all actions $a$. We define $\texttt{AfterHelpMove}^{\star}_{p}$ as

[TABLE]

That is, when $(s,\bm{a})\in\texttt{AfterHelpMove}^{\star}_{p}$, in $\mathcal{G}$, player $p$ has played $a_{p}$ from $\mathsf{st}(a_{p})$ and, due to player $-p$’s choice, $\mathcal{G}$ has reached $s$. However, with another choice of player $-p$, the game could have moved to a different state $s^{\prime}$ from which $-p$ can help $p$ to win as $\chi_{p}^{\star}(s^{\prime})\geq 0$. Intuitively, in runs that visit states of value [math] infinitely often, states from $\texttt{AfterHelpMove}^{\star}_{p}$ should be visited infinitely often for player $i$ to play SCO, i.e. such runs might not be winning, but this cannot be blamed on player $p$ who has sought repeatedly the collaboration of the other players to enforce his objective. Observe further that the definition of this predicate requires the labelling of the states (by actions) we have introduced in $\mathcal{G}^{\star}_{p}$. For example, in Figure 3, \texttt{AfterHelpMove}^{\texttt{A}}_{2}=\big{\{}\big{(}s_{0},(a,b^{\prime})\big{)},\big{(}s_{1},(b,b^{\prime})\big{)}\big{\}}. We let $\Phi_{0}^{\star}(p)=\Diamond\neg\texttt{Val}^{\star}_{p,0}\vee\Phi(p)\vee\Box\Diamond\texttt{AfterHelpMove}^{\star}_{p}$ and $\Phi_{1}^{\star}(p)=\left(\Diamond\texttt{Val}^{\star}_{p,1}\right)\rightarrow\Phi(p)$. Let us define $\Phi_{\mathcal{G}^{\star}_{p}}=\left(\bigwedge_{q\neq p}\Phi_{0}^{\star}(q)\wedge\Phi_{1}^{\star}(q)\right)\rightarrow(\Phi(p)\vee\Diamond\texttt{Val}^{\star}_{p,1}).$

To establish the correctness of this approach, we need several auxiliary lemmas.

Lemma 6**.**

If a strategy $\sigma\in\Gamma_{p}(\mathcal{G})$ is $\star$-admissible then for all of its realisations $\overline{\sigma}\in\Gamma^{\textrm{det}}_{p}(\mathcal{G}^{\star}_{p})$, $\mathcal{G}^{\star}_{p},\overline{\sigma}\models^{\texttt{S}}\Phi_{0}^{\star}(p)$.

Proof.

Assume toward a contradiction that there is a $\star$-admissible strategy $\sigma\in\Gamma_{p}(\mathcal{G})$ for which there exists a realisation $\overline{\sigma}\in\Gamma^{\textrm{det}}_{p}(\mathcal{G}^{\star}_{p})$ that does not satisfy $\Phi_{0}^{\star}(p)$. We can further assume wlog. that $\sigma$ plays Dirac moves in states of value [math]. There is a run $\rho\in\texttt{Outcome}(\mathcal{G}^{\star}_{p},\overline{\sigma})$ that does not satisfy $\Phi_{0}^{\star}(p)$. More precisely, $\rho$ satisfies

[TABLE]

The run $\rho$ does not satisfy $\Phi(p)$ but all values of its prefixes are equal to [math] and there is $k_{0}$ such that for every $k\geq k_{0}$, $\rho_{k}\not\in\texttt{AfterHelpMove}^{\star}_{p}$. We now show that for every $\rho^{\prime}\in\texttt{Outcome}(\mathcal{G},\sigma)$, such that $\mathfrak{o}(\rho_{\leq k_{0}})\subseteq_{\mathsf{pref}}\rho^{\prime}$, it holds that $\rho^{\prime}\not\in\Phi(p)$. If $\rho^{\prime}=\mathfrak{o}(\rho)$ then $\rho^{\prime}\not\in\Phi(p)$. If $\rho^{\prime}\neq\mathfrak{o}(\rho)$ then there exists $k\geq k_{0}$ for which, $\rho^{\prime}_{\leq k}=\mathfrak{o}(\rho)_{\leq k}$ and $\rho^{\prime}_{\leq k+1}\neq\mathfrak{o}(\rho)_{\leq k+1}$. Let $h^{\prime}=\rho^{\prime}_{\leq k}=\mathfrak{o}(\rho)_{\leq k}$, $s=\mathrm{last}(h^{\prime})$, $a=\overline{\sigma}(\rho_{\leq k})$. $h^{\prime}$ as a prefix of $\mathfrak{o}(\rho)$ has value [math] so $\sigma(h^{\prime})$ is Dirac and thus equal to $a$. Let $c,c^{\prime}\in\Sigma_{-p}(s)$ such that $\delta(s,(a,c))=\mathfrak{o}(\rho)_{k+1}$, $\delta(s,(a,c^{\prime}))=\rho^{\prime}_{k+1}$. From $\mathfrak{o}(\rho)_{k+1}\not\in\texttt{AfterHelpMove}^{\star}_{p}$ we know that $\chi_{p}^{\star}(\rho^{\prime}_{\leq k+1})=\chi_{p}^{\star}(h^{\prime}\delta(s,(a,c^{\prime})))=-1$. We have found a prefix of $\rho^{\prime}$ that has value $-1$, thus $\rho^{\prime}\not\in\Phi(p)$. We have proved that for all run $\rho^{\prime}\in\texttt{Outcome}(\mathcal{G},\sigma)$ such that $\mathfrak{o}(h)\subseteq_{\mathsf{pref}}\rho^{\prime}$, it holds that $\rho^{\prime}\not\in\Phi(p)$. This implies that $\chi_{\sigma}^{\star}(\mathfrak{o}(h))=-1<0=\chi_{p}^{\star}(\mathfrak{o}(h))$ proving that $\sigma$ is not $\star$-SCO and hence not $\star$-admissible. This is a contradiction. ∎

Lemma 7**.**

Given a $\star$-admissible strategy $\sigma\in\Gamma_{p}(\mathcal{G})$ and $\overline{\sigma}\in\Gamma^{\textrm{det}}_{p}(\mathcal{G}^{\star}_{p})$ one of its realisation. If a run $\rho\in\texttt{Outcome}(\mathcal{G}^{\star}_{p},\overline{\sigma})$ satisfies $\Box(\neg\texttt{Val}^{\star}_{p,1})\wedge\bigwedge_{q\neq p}\Phi_{0}^{\star}(q)\wedge\Phi_{1}^{\star}(q)$ in $\mathcal{G}^{\star}_{p}$ then there exists a profile $\tau\in\Gamma_{-p}(\mathcal{G})$ of $\star$-admissible strategies such that $\texttt{Outcome}(\mathcal{G},(\sigma,\tau))=\{\mathfrak{o}(\rho)\}$.

Proof.

For every $k\geq 1$ there exists moves $a^{k}_{1},\ldots,a^{k}_{n}\in\overline{\Sigma}$ such that $\delta(\rho_{k},a^{k}_{1},\ldots,a^{k}_{n})=\rho_{k+1}$ and $a^{k}_{p}=\overline{\sigma}(\rho_{\leq k})$. For every $q\neq p$, let $\tau_{q}\in\Gamma_{q}(\mathcal{G})$ be a strategy such that for every $k\geq 1$, $\tau_{q}(\mathfrak{o}(\rho_{\leq k}))=a^{k}_{q}$ and that plays an admissible strategy as soon as the current history is not a prefix of $\mathfrak{o}(\rho)$. We now show that $\texttt{Outcome}(\mathcal{G},(\sigma,\tau))=\{\mathfrak{o}(\rho)\}$. Denote by $a^{k}_{-p}=(a^{k}_{q})_{q\in P\setminus\{p\}}$ the Dirac move played by $-p$ in $\mathfrak{o}(\rho_{\leq k})$. Since $\sigma$ is $\star$-admissible; for every $k\geq 1$, $\sigma(\rho_{\leq k})$ is $\star$-LA and by Lemma 2 (iii) equivalent to the move of its support $a^{k}_{p}$, then by Lemma 4, we get $\delta_{r}(\mathfrak{o}(\rho_{k}),(\sigma(\mathfrak{o}(\rho_{\leq k})),a^{k}_{-p}))(\mathfrak{o}(\rho_{k+1}))=\delta_{r}(\mathfrak{o}(\rho_{k}),(a^{k}_{p},a^{k}_{-p}))(\mathfrak{o}(\rho_{k+1}))=1$. This implies that $\texttt{Outcome}(\mathcal{G},(\sigma,\tau))=\{\mathfrak{o}(\rho)\}$.

We now show that $\tau_{q}$ is admissible in $\mathcal{G}$ for every $q\neq p$. It is clearly $\star$-LA as the moves $a^{k}_{q}$ are $\star$-LAs and $\tau_{q}$ plays $\star$-LA moves at histories not prefix of $\mathfrak{o}(\rho)$. It is also $\star$-SCO at histories not prefix of $\mathfrak{o}(\rho)$. We now show that $\tau_{q}$ is $\star$-SCO at every $h\subseteq_{\mathsf{pref}}\mathfrak{o}(\rho)$.

If $\chi_{q}^{\star}(h)=1$ then by $\Phi_{1}^{\star}(q)$, $\rho$ is winning for $\Phi(q)$, and hence so is $\mathfrak{o}(\rho)$. As $a^{k}_{q}$ is a $\star$-LA move for every $k$, all histories of the form $\mathfrak{o}(\rho_{\leq k})$ for $k\geq|h|$ and their successors through $a^{k}_{q}$ have value $1$. Consider a profile ${\bm{\sigma}}$ such that ${\bm{\sigma}}_{q}=\tau_{q}$, $h\in\texttt{Hist}({\bm{\sigma}})$, we show that $\mathcal{G},{\bm{\sigma}}\models^{\star}_{h}\Phi(q)$. We do this part of proof for $\star=\texttt{A}$ (the proof for $\star=\texttt{S}$ is a bit easier and omitted). We show that $\mathbb{P}_{{\bm{\sigma}}}(\neg\Phi(q)\cap\textrm{Cyl}(h))=0$. For this, we decompose the set $\neg\Phi(q)\cap\textrm{Cyl}(h)$ into disjoint sets of runs:

[TABLE]

where the last union range over the state $s^{\prime}\in\textrm{Supp}(\delta_{r}(\rho_{k},{\bm{\sigma}}(\mathfrak{o}(\rho_{\leq k})))\setminus\{\mathfrak{o}(\rho_{k})\}$. The histories $\mathfrak{o}(\rho_{\leq k})s^{\prime}$ quantified above have value $1$, and $\tau_{q}$ is A-admissible at these histories by construction since the histories are not prefixes of $\mathfrak{o}(\rho)$. Hence, A-winning from these histories, so $\mathbb{P}_{{\bm{\sigma}}}(\neg\Phi(q)\cap\textrm{Cyl}(\mathfrak{o}(\rho_{\leq k})s^{\prime}))=0$. $\mathbb{P}_{{\bm{\sigma}}}(\neg\Phi(q)\cap\{\mathfrak{o}(\rho)\})=0$ because $\mathfrak{o}(\rho)\in\Phi(q)$. The set $\neg\Phi(q)\cap\textrm{Cyl}(h)$ is a countable union of sets of probability [math], it is thus also of probability [math]. The proof for the sure semantics is similar: it suffices to replace the fact that a set has probability zero by emptiness of this set. We have thus proved that $\chi_{\sigma}^{\star}(h)=\chi_{q}^{\star}(h)=1$.

If $\chi_{q}^{\star}(h)=0$. We show that there exists a profile ${\bm{\sigma}}$ such that ${\bm{\sigma}}_{q}=\tau_{q}$, $h\in\texttt{Hist}(\mathcal{G},{\bm{\sigma}})$ and ${\bm{\sigma}}\models^{\star}\Phi(q)$. Let $k_{0}=|h|$. If $\mathfrak{o}(\rho)\in\Phi(q)$ then it suffices to take ${\bm{\sigma}}=(\sigma,\tau)$. Otherwise we begin to show that there is $k\geq k_{0}$ such that $\rho_{k+1}\in\texttt{AfterHelpMove}^{\star}_{q}$. Assume toward a contradiction that such a $k$ does not exists, then $\Phi_{0}^{\star}(q)$ tells us that there exists $k_{2}$ such that $\rho_{k_{2}}\in\texttt{Val}^{\star}_{q,-1}$ or $\rho_{k_{2}}\in\texttt{Val}^{\star}_{q,1}$. Necessarily $k_{2}>k_{0}$ because as $\star$-LA moves only are played the states of value $1$ cannot be escaped once entered. In the case $\rho_{k_{2}}\in\texttt{Val}^{\star}_{q,1}$, $\rho$ satisfies $\Diamond\texttt{Val}^{\star}_{q,1}$ and hence $\Phi(q)$ by virtue of $\Phi_{1}^{\star}(q)$. This contradict the fact that we are considering the case $\mathfrak{o}(\rho)\not\in\Phi(q)$. Consider now that $\rho_{k_{2}}\in\texttt{Val}^{\star}_{q,-1}$. Let $k_{1}$ be the unique number in $\{k_{0},\ldots,k_{2}-1\}$ such that $\chi_{q}^{\star}(\rho_{k_{1}})=0$ and $\chi_{q}^{\star}(\rho_{k_{1}+1})=-1$. Since $k_{1}\geq k_{0}$, $\rho_{k_{1}+1}\not\in\texttt{AfterHelpMove}^{\star}_{q}$, from which we deduce that $\mathrm{Succ}(\rho_{k_{1}},a_{q}^{k})\subseteq\texttt{Val}^{\star}_{q,-1}$. This contradicts the fact that $a_{q}^{k}$ is a $\star$-LA move in a history of value [math]. We have showed the existence of a prefix length $k\geq|h|$ such that $\rho_{k+1}\in\texttt{AfterHelp}^{\star}_{\rho_{k},q}$ and we resume the proof of $\chi_{\sigma}^{\star}(h)=0=\chi_{q}^{\star}(h)$. There exists a state $s^{\prime\prime}\in\mathrm{Succ}(a^{k+1}_{q})\setminus\{\mathfrak{o}(\rho_{k+1})\}$ such that $\chi_{q}^{\star}(s^{\prime\prime})\geq 0$. Moreover $\tau_{q}$ is $\star$-admissible from $\mathfrak{o}(\rho_{\leq k})s^{\prime\prime}$, so there is a profile ${\bm{\sigma}}$ such that $\mathfrak{o}(\rho_{\leq k})s^{\prime\prime}\in\texttt{Hist}({\bm{\sigma}})$, ${\bm{\sigma}}_{q}=\tau_{q}$ and $\mathcal{G},{\bm{\sigma}}\models^{\star}\Phi(q)$. Since $h\subseteq_{\mathsf{pref}}\mathfrak{o}(\rho_{\leq k})s^{\prime\prime}$, this implies that $\chi_{\sigma}^{\star}(h)\geq 0$ as required.

It remains the case of histories $h$ prefix of $\mathfrak{o}(\rho)$ such that $\chi_{q}^{\star}(h)=-1$. This case is straightforward because the following sequence of inequalities holds for every history $-1\leq\chi_{\sigma}^{\star}(h)\leq\chi_{q}^{\star}(h)$. At the end, for every $q\neq p$, $\tau_{q}$ is $\star$-admissible as both $\star$-LA and $\star$-SCO, and $\mathfrak{o}(\rho)=\texttt{Outcome}(\mathcal{G},(\sigma,\tau))$. ∎

Lemma 8** (Admissible and dominant synthesis).**

In concurrent games with prefix independent $\omega$-regular winning conditions with semantics $\star\in\{\texttt{S},\texttt{A}\}$, given a finite memory strategy $\sigma$ for player $p$ that is $\star$-LA, one can construct effectively a finite memory strategy $\sigma^{\prime}$ such that $\sigma\preccurlyeq^{\star}\sigma^{\prime}$.

Proof.

We assume that the strategy $\sigma$ is given by a stochastic Moore machine ${\cal M}_{\sigma}$ with set of memory states $M=\{m_{1},m_{2},\dots,m_{k}\}$, with a designated initial memory state $m_{\sf init}$ and such that after an history $h$, the machine is in memory state ${\cal M}_{\sigma}(h)\in M$. Each such memory state is labelled with a move noted ${\cal L}_{\sigma}(m)$. If we take the product of ${\cal M}_{\sigma}$ with the game $\mathcal{G}$, we obtain a structure with states that are pairs $(s,m)$ where $s$ is a state of the original game and $m$ is a memory state of ${\cal M}_{\sigma}$. This product can be seen as a new Moore machine that behaves exactly as ${\cal M}_{\sigma}$. From now on, we make the hypothesis that ${\cal M}_{\sigma}$ has this state space.

We note $\chi_{p}^{\star}(s)$ the value of state $s$ in $\mathcal{G}$, this value is well defined as $\Phi(p)$ is prefix independent, and we note $\chi_{\sigma}^{\star}(s,m)$ the value of the strategy $\sigma$ for any history $h$ that ends up in state $s$ of the $\mathcal{G}$ and memory state $m={\cal M}_{\sigma}(h)$ of the machine.

As the strategy $\sigma$ is $\star$-LA, if it is not admissible then it must be the case that there are state $s$, memory state $m$, and histories $h$ such that after history $h$, the game $\mathcal{G}$ is in state $s$, ${\cal M}_{\sigma}$ is in state $m$, and $\chi_{p}^{\star}(s)\not=\chi_{\sigma}^{\star}(s,m)$, i.e. $h$ is a witness that shows that $\sigma$ is not SCO. Then, we will modify systematically ${\cal M}_{\sigma}$ in a way that it behaves as ${\cal M}_{\sigma}$ in all other histories and plays SCO in the histories that witness the fact that $\sigma$ is not SCO.

We only need to consider the two following cases:

$s$ and $(s,m)$ are such that: $\chi_{p}^{\star}(s)=1$ and $\chi_{\sigma}^{\star}(s,m)\leq 0$, then we replace $(s,m)$ by a sub-machine that implements a $\star$-winning strategy from $(s,m)$. We know that finite memory machines that are $\star$-winning always exist and can be computed effectively for all $\omega$-regular objectives. 2. 2.

$s$ and $(s,m)$ are such that: $\chi_{p}^{\star}(s)=0$ and $\chi_{\sigma}^{\star}(s,m)=-1$, then we replace $(s,m)$ by a sub-machine that plays any admissible strategy from $s$. We show this by establishing in the next claim that there is always such a finite state strategy and it can be computed effectively.

Claim. Given a game $\mathcal{G}$, a state $s$, and a player $p$, we can construct a finite state stochastic Moore machine that encodes an admissible strategy.

We establish this claim constructively. We consider the following case study to describe the machine:

• •

if the value of $\chi_{p}^{\star}(s)=1$, then the machine plays a finite state $\star$-winning strategy, such a finite memory strategy always exists and can be computed effectively.

• •

if the value of $\chi_{p}^{\star}(s)=-1$, then the machine plays arbitrarily.

• •

if the value of $\chi_{p}^{\star}(s)=0$, then the machine selects a finite lasso-shape path $\rho=\rho_{1}\cdot\rho^{\omega}_{2}$ such that $\rho$ is compatible with $\star$-LA moves of player $p$ and such that $\rho\in\Phi(p)$. Such a finite lasso-path always exists as $\chi_{p}^{\star}(s)=0$. Then the machine plays according to this lasso-path either forever or up to a deviation by another player. If the lasso path is played forever then the outcome is $\rho\in\Phi(p)$, and if there is a deviation, the new state of the game is $s^{\prime}$ and the three rules here are applied from $s^{\prime}$ (according to the value of state $s^{\prime}$).

Clearly, if entering a state $s$ with value [math], we always choose the same finite lasso-path then the machine has finite state. As in states with value [math], it always plays $\star$-LA moves and $\rho$ from $s$ is such that $\rho\in\Phi(p)$, then we conclude that the strategy is $\star$-SCO and $\star$-LA and thus $\star$-admissible. So, we are done. ∎

Theorem 2** (Assume-admissible synthesis).**

Player $p$ has a $\star$-admissible strategy $\sigma$ that is $\star$-winning against all player $-p$ $\star$-admissible strategies in $\mathcal{G}$ iff Player $p$ has an S-winning strategy in $\mathcal{G}^{\star}_{p}$ for the objective $\Phi_{\mathcal{G}^{\star}_{p}}$. Such a $\star$-admissible strategy $\sigma$ can be effectively computed (from any player $p$ S-winning strategy in $\mathcal{G}^{\star}_{p}$).

Proof.

Completeness: Assume there exists an admissible strategy $\sigma\in\Gamma_{p}(\mathcal{G})$ that wins against every admissible strategy. Let $\overline{\sigma}\in\Gamma^{\textrm{det}}_{p}(\mathcal{G})$ be a realisation of $\sigma$. Note that every runs $\rho\in\texttt{Outcome}(\mathcal{G}^{\star}_{p},\overline{\sigma})$ that satisfies $\Diamond\texttt{Val}^{\star}_{p,1}$ also satisfies $\Phi_{\mathcal{G}^{\star}_{p}}$. The other runs $\rho\in\texttt{Outcome}(\mathcal{G}^{\star}_{p},\overline{\sigma})$ satisfy $\neg\Diamond\texttt{Val}^{\star}_{p,1}\equiv\Box(\neg\texttt{Val}^{\star}_{p,1})$; for these runs we show that $\bigwedge_{q\neq p}\Phi_{0}^{\star}(q)\wedge\Phi_{1}^{\star}(q)\rightarrow\Phi(p)$. So let $\rho\in\texttt{Outcome}(\mathcal{G}^{\star}_{p},\overline{\sigma})$ be such that $\Box(\neg\texttt{Val}^{\star}_{p,1})\wedge\bigwedge_{q\neq p}\Phi_{0}^{\star}(q)\wedge\Phi_{1}^{\star}(q)$. By Lemma 7, there exists $\tau$ that only contains admissible profiles such that $\texttt{Outcome}(\sigma,\tau)=\{\mathfrak{o}(\rho)\}$. By assumption $(\sigma,\tau)$ is winning for $\Phi(p)$, hence so is $\rho$.

Correctness: We show the following stronger statement. If a strategy $\sigma$ is winning for $\Phi_{\mathcal{G}^{\star}_{p}}$ in $\mathcal{G}^{\star}_{p}$ then one can construct a strategy $\hat{\sigma}$ admissible that wins against every profile of admissible strategies as follows:

(i) take an extension $\sigma^{\prime}$ of $\sigma$;

(ii) modify $\sigma^{\prime}$ into $\sigma^{\prime\prime}$ that plays a winning strategy as soon as a history of value $1$ is entered;

(iii) use Lemma 8 to design an admissible strategy $\hat{\sigma}$ that weakly dominates $\sigma^{\prime\prime}$.

We do the proof for the almost-sure semantics only, that is, for $\star=\texttt{A}$. The slightly simpler but similar proof for $\star=\texttt{S}$ is omitted. We first show that if a strategy $\sigma$ is winning for $\Phi_{\mathcal{G}^{\texttt{A}}_{p}}$ in $\mathcal{G}^{\texttt{A}}_{p}$ then for every extension $\sigma^{\prime}$ of $\sigma$ and every profile $\tau$ of admissible strategies, it holds that $\mathcal{G},(\sigma^{\prime},\tau)\models^{\texttt{A}}\Phi(p)\vee\Diamond\texttt{Val}^{\texttt{A}}_{p,1}$.

Let $\tau$ be a profile of admissible strategies. Note that $\mathbb{P}_{(\sigma^{\prime},\tau)}(\Diamond\texttt{Val}^{\texttt{A}}_{p,1}\vee\Phi(p))=1$ is equivalent to $\mathbb{P}_{(\sigma^{\prime},\tau)}(\Box(\neg\texttt{Val}^{\texttt{A}}_{p,1})\wedge\neg\Phi(p))=0$. For $q\neq p$, $\tau_{q}$ is admissible, so, winning from histories of value $1$, hence $\mathbb{P}_{(\sigma^{\prime},\tau)}(\Phi_{1}^{\texttt{A}}(q))=1$ and we have $\mathbb{P}_{(\sigma^{\prime},\tau)}(\Box(\neg\texttt{Val}^{\texttt{A}}_{p,1})\wedge\neg\Phi(p))=\mathbb{P}_{(\sigma^{\prime},\tau)}(\bigwedge_{q\neq p}\Phi_{1}^{\texttt{A}}(q)\wedge\Box(\neg\texttt{Val}^{\texttt{A}}_{p,1})\wedge\neg\Phi(p))$. To show that this probability is null it suffices to show that every run $\rho\in\texttt{Outcome}(\mathcal{G},(\sigma^{\prime},\tau))$ that satisfies $\bigwedge_{q\neq p}\Phi_{1}^{\texttt{A}}(q)\wedge\Box(\neg\texttt{Val}^{\texttt{A}}_{p,1})$ also satisfies $\Phi(p)$. Take such a run $\rho$, then there is a sequence of move profile $\bm{a}^{k}$ such that $a^{k}_{q}\in\textrm{Supp}(\tau_{q}(\rho_{k}))$ and $\rho_{k+1}=\delta(\rho_{k},\bm{a}^{k})$. Define the run $\overline{\rho}$ by $\overline{\rho}_{k}=(\rho_{k},\bm{a}^{k})$ for $k\geq 1$ and $\overline{\rho}_{0}=s_{\mathsf{init}}^{\prime}$ and note that $\rho=\mathfrak{o}(\overline{\rho})$. We also have that $\overline{\rho}$ is a run of $\texttt{Outcome}(\mathcal{G}^{\texttt{A}}_{p},\sigma)$ and for $q\neq p$ of $\texttt{Outcome}(\mathcal{G}^{\texttt{A}}_{p},\overline{\tau_{q}})$ where $\overline{\tau_{q}}$ is any realisation of $\tau_{q}$ for which $a^{k}_{q}=\tau_{q}(\rho_{k})$ for every $k\geq 1$. The run $\overline{\rho}$ satisfies $\bigwedge_{q\neq p}\Phi_{1}^{\texttt{A}}(q)$ by assumption on $\rho$ and $\bigwedge_{q\neq p}\Phi_{0}^{\texttt{A}}(q)$ because all the $\tau_{q}$ are admissible (Lemma 6). Putting all the things together $\overline{\rho}$ satisfies $\Phi(p)$ and so does $\rho$. We conclude that $\sigma^{\prime}$ satisfies that for every profile $\tau$ of admissible strategies, it holds that $(\sigma^{\prime},\tau)\models^{\texttt{A}}\Phi(p)\vee\Diamond\texttt{Val}^{\texttt{A}}_{p,1}$. By construction $\sigma^{\prime\prime}$ wins against every profile $\tau$ for which $(\sigma^{\prime},\tau)\models^{\texttt{A}}\Diamond\texttt{Val}^{\texttt{A}}_{p,1}$. So $\sigma^{\prime\prime}$ is A-winning against every profile $\tau$ of A-admissible profile. Since $\sigma^{\prime\prime}\preccurlyeq^{\texttt{A}}\hat{\sigma}$, we deduce that $\hat{\sigma}$ is A-winning against every A-admissible profile. ∎

Let us explain how we build a strategy in $\mathcal{G}$ with the desired properties, from any player $p$ strategy enforcing $\Phi_{\mathcal{G}^{\star}_{p}}$ in $\mathcal{G}^{\star}_{p}$. Remember that $\mathcal{G}^{\star}_{p}$ ensures that the players play $\star$-LA moves only. We will use $\Phi_{\mathcal{G}^{\star}_{p}}$ to make sure that, when SCO strategies are played by $-p$ (relying on the extra information we have encoded in the states), then $p$ reaches a state of value $1$. First, consider $\Phi_{0}^{\star}(q)$ for $q\neq p$. Runs that satisfy this formula are either those that visit states of value [math] only finitely often ($\Diamond\neg\texttt{Val}^{\star}_{q,0}$); or those that stay in states of value [math], in which case they must be either winning ($\Phi(q)$) or visit infinitely often states where Player $q$ could have been helped by the other players ($\Box\Diamond\texttt{AfterHelpMove}^{\star}_{q}$). This is a necessary condition on runs visiting only value [math] states for the strategy to be SCO. Next, observe that $\Phi_{1}^{\star}(q)$ states that if a history of value $1$ is entered then Player $q$ must win. This allows us to understand the left part of the implication in $\Phi_{\mathcal{G}^{\star}_{p}}$: the implication can be read as ‘if all other players play a $\star$-admissible strategy, then either $p$ should win ($\Phi(p)$) or a state of value $1$ for player $p$ should eventually be visited ($\Diamond\texttt{Val}^{\star}_{p,1}$)’. Then a strategy $\hat{\sigma}$ (in $\mathcal{G}$) that wins against admissible strategies can be extracted from a winning strategy $\overline{\sigma}$ (in $\mathcal{G}^{\star}_{p}$) in a straightforward way, except when $\overline{\sigma}$ enforces to reach a state of value $1$ ($\Diamond\texttt{Val}^{\star}_{p,1}$ in $\Phi_{\mathcal{G}^{\star}_{p}}$). In this case, $\sigma$ cannot follow $\overline{\sigma}$, but must rather switch to a winning strategy, which:

(i) is guaranteed to exist since the state that has been reached has value $1$; and

(ii) can be computed using classical techniques [10].

The strategy $\hat{\sigma}$ is not necessarily admissible but by Theorem 1 (i), there is an admissible strategy $\sigma$ with $\hat{\sigma}\preccurlyeq^{\star}\sigma$. By weak domination, $\sigma$ wins against more profiles than $\hat{\sigma}$, in particular, it wins against the profiles of admissible strategies of the other players.

Example 7**.**

In our running example, observe that $\neg\texttt{Val}^{\texttt{A}}_{2,0}=\texttt{Val}^{\texttt{A}}_{2,1}=\{Win\}$ since there is no state of value $-1$ in $\mathcal{G}$. Hence, $\Phi(2)=\Diamond Win=\Diamond\texttt{Val}^{\texttt{A}}_{2,1}=\Diamond\neg\texttt{Val}^{\texttt{A}}_{2,0}$. Finally, \texttt{AfterHelpMove}^{\texttt{A}}_{2}=\big{\{}\big{(}s_{0},(a,b^{\prime})\big{)},\big{(}s_{1},(b,b^{\prime})\big{)}\big{\}}, so, after simplification: \Phi_{\mathcal{G}^{\texttt{A}}_{1}}=\big{[}\Diamond Win\vee\Box\Diamond\big{(}(s_{0},(a,b^{\prime}))\vee(s_{1},(b,b^{\prime}))\big{)}\big{]}\rightarrow\Diamond Win. Thus, to win in $\mathcal{G}^{\texttt{A}}_{1}$ (under the sure semantics), player 1 must ensure to reach $Win$ as long as player 2 visits the set of bold states in Figure 3 infinitely often. A winning strategy $\overline{\sigma}$ in $\mathcal{G}^{\texttt{A}}_{1}$ consists in (eventually) always playing $b$ from all states in the dashed rectangle; and $d$ from \big{(}s_{1},(b,b^{\prime})\big{)}. Observe that this strategy is compatible with $\mathfrak{o}$. From $\overline{\sigma}$, we can extract an admissible player $1$ strategy in $\mathcal{G}$: always play $b$ in $s_{0}$; always play $d$ in $s_{1}$; and play a winning strategy from $s_{2}$ (which is of value $1$), for instance: always play $0.5f+0.5g$ from $s_{2}$ like $\sigma_{3}$ does.

We conclude by a remark on games with simple safety objectives.

Remark 1**.**

In the case of simple safety games, the situation is much simpler. We have seen in Theorem 1 that, for simple safety objectives, $\star$-LA strategies are exactly the admissible strategies. So, can simply build $\mathcal{G}_{p}$ from $\mathcal{G}$ by pruning the actions which are not $\star$-LA (the labelling by actions is not necessary anymore since its sole purpose is to enforce SCO), and look for a player $p$ winning strategy in the resulting game.