Admissibility in Concurrent Games
Nicolas Basset, Gilles Geeraerts, Jean-Fran\c{c}ois Raskin and, Ocan Sankur

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
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Game Theory and Applications · Computability, Logic, AI Algorithms
Admissibility in Concurrent Games111Work partially
supported by the ERC inVEST (279499) project.
Nicolas Basset
Université libre de Bruxelles, Brussels, Belgium
{nicolas.basset, gilles.geeraerts, jraskin}@ulb.ac.be
Gilles Geeraerts
Université libre de Bruxelles, Brussels, Belgium
{nicolas.basset, gilles.geeraerts, jraskin}@ulb.ac.be
Jean-François Raskin
Université libre de Bruxelles, Brussels, Belgium
{nicolas.basset, gilles.geeraerts, jraskin}@ulb.ac.be
Ocan Sankur
CNRS, IRISA, Rennes, France
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 -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 strategies only.
1 Introduction
In a concurrent -player game played on a graph, all players independently and simultaneously choose moves at each round of the game, and those 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 -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 , a strategy is said to be dominated by a strategy if does as well as with respect to against all the strategies of the other players and strictly better for some of them. A strategy 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 -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 ’s objective is to reach , while Player wants to reach . 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 to and from to requires the cooperation of both players. Moreover, the transitions from behave as in the classical ‘matching pennies’ game: player must chose between and ; player between and ; and the target is reached only when the choices ‘match’. So, randomisation is needed to make sure is reached with probability one, from . 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 -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 be a set of players. A concurrent game played on a finite graph by the players in is a tuple where,
(i) is a finite set of states; and the initial state;
(ii) is a finite set of actions;
(iii) For all , is a action assignment that assigns, to all states , the set of actions available to player from state .
(iv) is the transition function.
We write for all . It is often convenient to consider a player separately and see the set of all other players as a single player denoted . Hence, the set of actions of in state is: . We assume that for all and . We denote by the set of possible successors of the state when player performs action . A particular case of concurrent games are the turn-based games. A game is turn-based iff for all states , there is a unique player s.t. the successors of depend only on ’s choice of action, i.e., contains exactly one state for all .
A history is a finite path s.t.
(i) ;
(ii) ; and
(iii) for every , there exists with .
The length of a history is its number of states ; for every , we denote by the state and by the history . We denote by the last state of , that is, . A run is defined similarly as a history except that its length is infinite. For a run and , we also write and . Let (resp. ) denote the set of histories (resp. runs) of . The game is played from the initial state for an infinite number of rounds, producing a run. At each round , with current state , all players select simultaneously a action , and the state 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 probability distribution on , is a function such that ; and we let be the support of . We denote by the probability of a given set according to . The set of probability distributions on is denoted by . A randomised move of player in state is a probability distribution on , that is, an element of . A randomised move that assigns probability 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 denotes the randomised move that assigns probability to and (and [math] to all other actions). In particular, we denote by a Dirac move that assigns probability to action .
Given a state and a tuple of randomised moves from , one per player, we let be the probability distribution on states s.t. for all : , where . Intuitively, is the probability to reach from when the players play according to .
A strategy for player is a function from histories to randomised moves (of player ) such that, for all : . A strategy is called Dirac at history , if is a Dirac move; it is called Dirac if it is Dirac in all histories. We denote by the set of player- strategies in the game, and by the set of player- strategies that only use Dirac moves (those strategies are also called deterministic); we might omit if it is clear from context. A strategy profile for a subset of players is a tuple with for all . When the set of players is omitted, we assume . Let be a strategy profile. Then, for all players , we let denote the restriction of to (hence, can be regarded as a strategy of player that returns, for all histories , a randomised move from ). We sometimes denote by the pair . Given a history , we let .
Let be a history and let be a history or a run. Then, we write iff is a prefix of , i.e., . Consider two strategies and for player , and a history . We denote by the strategy that follows strategy and shifts to as soon as has been played. Formally, is the strategy s.t., for all histories : if ; and otherwise.
Probability measure and outcome of a profile
Given a history , we let be the cylinder of . To each strategy profile , we associate a probability measure on certain sets of runs. First, for a history , we define inductively on the length of : , and when and . Based on this definition, we can extend the definition of to any Borel set of runs on cylinders. In particular, the function is well-defined for all -regular sets of runs, that we will consider in this paper [18]. We extend the Hist notation and let be the set of histories such that . Given a profile we denote by the set of runs s.t. all prefixes of belong to . In particular, . Note that when is composed of Dirac strategies then is a singleton. The outcome (set of histories) of a strategy , denoted by (), is the union of outcomes (set of histories, respectively) of profile s.t. .
Winning conditions
To determine the gain of all players in the game , 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 is a subset of called winning runs. From now on, we assume that concurrent games are equipped with a function , called the winning condition, and mapping all players to a winning condition . A profile is A-winning for if which we write . A profile is S-winning for if which we write . Note that when is Dirac, the two semantics coincide: iff . The profile is A-winning from if and which we denote . The profile is winning for the sure semantics from if , which we denote . We often omit 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 as in the following definition. Given a semantics , a strategy for player (from a history ) is called -winning for player if for every , the profile is -winning for player (from ). Note that a strategy for player is S-winning iff . We often describe winning conditions using standard linear temporal operators and ; e.g. means the set of runs that visit infinitely often . See [3] for a formal definition.
A winning condition is prefix-independent if for all , and all : . When contains all runs that do not visit some designated set of states, we say that is a safety condition. A safety game is a game whose winning condition is such that is a safety condition for all players . Without loss of generality, we assume that safety games are so-called simple safety games: a safety game is simple iff for all players , for all : implies that no is reachable from . 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 , iff for every .
Proof.
The only non-trivial implication is: if then for every which we show by contraposition. Assume there exists such that . This means that and . It follows that . ∎
Example 1**.**
*Let us consider three player- strategies in Fig. 2.
(i) is any strategy that plays in ;
(ii) is any strategy that plays in , in and in ; and
(iii) is any strategy that plays in , in , and in .
Clearly, never allows one to reach while some runs respecting and do (remember that there is no -winning strategy in this game). We will see later that the best choice of player (among , ) depends on the semantics we consider. In the almost-sure semantics, is ‘better’ for player , because is an A-winning strategy from all histories ending in , while is not. On the other hand, in the sure semantics, playing is ’better’ for player than . Indeed, for all player- strategies , either contains only runs that do not reach , or contains at least a run that reaches , but, in this case, it also contains a run of the form (because, intuitively, player plays both and from ). So, is not winning against any , while wins at least against a player strategy that plays in , in and in . 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 dominates another strategy when wins every time 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 , a player , and, following our previous conventions, we denote by the set .
Admissible strategies
We first recall the classical notion of admissible strategy [4, 1]. Given two strategies , we say that is -weakly dominated by , denoted , if for all : implies . This indeed captures the idea that is not worse that , because it wins (for ) every time does. Note that is not anti-symmetric, hence we note when and are equivalent, i.e. and . In other words iff for every , . When but we say that is -dominated by , and we write . Observe that holds if and only if and there exists at least one , such that and . That is, is now strictly better than . Then, a strategy is -admissible iff there is no strategy s.t. , i.e., is -admissible iff it is not -dominated.
Example 2**.**
Let us continue our running example, by formalising the intuitions we have sketched in Example 1. Since does not allow to reach the target, while some runs respecting and do, we have: and . Moreover, because is A-winning from any history that ends in while is not because it does not A-win against a player strategy that would always play in (and both strategies behave the same way in and ). On the other hand, . In fact, , so, for all , whenever , all runs of reach , and we also have . Moreover, for the strategy that plays at , profile is S-winning but not . We will see later that is A-admissible and is S-admissible.
Values of histories
Before we discuss strongly cooperative optimal and locally admissible strategies, we associate values to histories. Let be a history, and be a strategy of player . Then, the value of w.r.t. for semantics is defined as follows. if is -winning from ; if there are and s.t. , and ; and otherwise.
Value corresponds to the case where is -winning for player from (thus, against all possible strategies in ). When , is not -winning from (because of in the definition), but the other players can still help to reach his objective (by playing some s.t. , which exists by definition). Last, when there is no hope for to -win, even with the collaboration of the other players. In this case, there is no s.t. . Hence, having is stronger than saying that is not winning—when is not winning, we could have as well.
We define the value of a history for player as the best value he can achieve with his different strategies: . Last, for , let be the set of histories s.t. .
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 of Player is -SCO at iff ; and is -SCO iff it is -SCO at all . Intuitively, when is a -SCO strategy of Player , the following should hold:
(i) if has a -winning strategy from (i.e. ), then, should be -winning (i.e. ); and
(ii) otherwise if has no -winning strategy from but still has the opportunity to -win with the help of other players (hence ), then, should enable the other players to help fulfil his objective (i.e. ).
Observe that when , no continuation of is -winning for , so for all strategies .
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: , and . Let us Consider again the three strategies , and from Example 1. We see that is S-SCO but it is not A-SCO because, for all profiles ending in : while . On the other hand, is A-SCO; but it is not S-SCO. Indeed, one can check that, for all strategies : if contains a run reaching , then it also contains a run that cycles in . So, for all such strategies , , hence for all histories that end in ; while since for all Dirac strategies .
*Next, let us build a strategy that is A-dominated by (hence, not A-admissible), but A-SCO. We let play as except that plays the first time is visited (hence ensuring that the self-loop on will be taken after the first visit to ). Now, is A-dominated by , because
(i) A-wins every time does; but
(ii) does not A-win against the player strategy that plays only when is visited for the first time, while A-wins against .
However, is SCO because playing keeps the value of the history equal to (intuitively, playing 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 -SCO strategies which are not admissible, so, being -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 be a history, and let and be two randomised moves in . We say that is -weakly dominated at by (denoted ) iff for all such that and , there exists s.t. and . Observe that the relation is not anti-symmetric. We let be the equivalence relation s.t. iff and . When but we say that is -dominated at by and denote this by . When a randomised move is not -dominated at , we say that is -admissible at . This allows us to define a more local notion of dominated strategy: a strategy of player is -locally-admissible (LA) if is a -admissible move at , for all histories .
Example 4**.**
Consider the Dirac move and the non-Dirac move played from in the example in Figure 2. One can check that . Indeed, consider a strategy s.t. for some with . Then, playing from will never allow Player 1 to reach surely at the next step, whatever Player 2 plays; while playing, for instance, (Dirac move) ensures player 1 to reach surely at the next step, against a Player-2 strategy that plays . Thus, is S-LA but is not.
On the other hand, after every randomised move played in state , the updated state is or from which A-winning strategies exist, thus for all and all histories s.t. (so, in particular, and ). It follows that both and are A-LA. However, in the long run, player 1 needs to play , with , infinitely often in order to A-win. In fact, is A-winning from while is not. Thus, there are -LA strategies which are not admissible, so being -LA is not a sufficient criterion for -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 surely from , while playing repeatedly and with equal probability ensures to reach 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 plays some action with some positive probability, then is dominated by the Dirac move . 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 and all randomised moves :
- (i)
For all : ; 2. (ii)
Dirac moves that are not -dominated at by another Dirac move are admissible; 3. (iii)
*A move is -LA at iff, for all : *
(1) *is -LA at ; and * (2) *for all . * **
Proof.
Proof of (i): Take a strategy such that and . Define the strategy that plays as except in where it plays instead of . One show that . Consider any such that . This means that , so, in particular , for all . Since and are identical in all other histories, including those extending , we deduce that . The proof for the sure semantics is similar.
Proof of (ii): If a Dirac move is -dominated at by a move then by (i) it is -dominated at by a Dirac move . This shows (ii) by contraposition.
Proof of (iii): Assume is a -LA move at . By (i), for every , and (because is a -LA move at ) so . Hence all the elements of are equivalent and -LA at .
Assume now that , is -LA at and , . We take . By Lemma 2 it holds that ; so it remains to show that . Let be such that . We construct a strategy such that and . For every , there exists a strategy such that and . We construct as follows. We start with , we set , for every and for every , we do . This shows that . We conclude that is -LA at . ∎
Example 5**.**
As we have seen in Example 4, . Note that a strategy s.t. for all with has value , while .
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 would hold iff the value of the history obtained by playing is smaller than or equal to the value obtained by playing ). This is not true for histories of value [math]: we have seen that and are -incomparable, yet playing or from yields a history with value [math] in all cases (even when 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 , histories with and Dirac moves : if, and only if the following conditions hold for every where we write and :
- (i)
; 2. (ii)
if then .
Proof.
Direction (i)(ii): Assume that . Let such that and and strategy such that and .
Proof of (i): We take , and show that . For every , if then . In particular, if then . We deduce that is winning from if is winning from . As is arbitrary this shows that . Dually if then is losing from and so is from . This shows the implication . These two implications yield .
Proof of (ii): We show the contrapositive, consider such that and show that and cannot be both equal to [math]. For this purpose we assume that and show that . Since is chosen arbitrary we take it such that . In particular there exists such that . Let be an arbitrary player strategy. By , we have implies . Since and are equal on histories incomparable to , it then holds that for every arbitrary profile . We have shown that is winning from and hence that as claimed.
Direction (i)(ii) : We assume that (i) and (ii) hold and show that . Let be such that and . We define such that and in several steps. We start with . We set . For every we take a strategy such that and update to . For every such that we do the same operation. Note that for all states such that the strategies and coincide from . Now we show that . We take an arbitrary such that and show that . Assume that , otherwise and behave exactly the same. Let . We show that . This is equivalent to show that for every . Let . If and then and play the same from and so . If then by (ii) and (i), either , or , or . The first case is not possible since witnesses that . In the second case, by construction, we have , thus . Assume the third case, which means . Then (the first equality is due to the construction of , the last inequality is due to the fact that ). We deduce that is winning from and hence that . This concludes the proof of . As agrees with on histories for which is not a prefix, this implies that . ∎
Now, we turn our attention to randomised moves in general, and show, again, how the notion of -LA equivalence between -LA moves relates to values of histories. Let be a history ending in , and assume that player 1 has the choice between two randomised moves and which are -LA and equivalent (). Then, the probability of ending up in some state will be the same by playing or , provided has value [math] (for player ). A similar property exists for histories of value : the probability of producing a history of value is the same under and :
Lemma 4**.**
Let be a history s.t. , and let and be two randomised moves in s.t. . Then, for all :
- (i)
* for all s.t. ; and* 2. (ii)
, with .
Proof.
We first prove the properties for Dirac moves and such that . By Lemma 3, for every and if this value is [math] it further holds that: . Then for every such that , for every , it holds that . Thus (i) holds when and are Dirac moves:
[TABLE]
Next, we know that, for all Dirac moves , , by definition of Dirac moves. We use this to establish point (ii), again when and are Dirac moves:
[TABLE]
Notice that the third inequality follows from and Lemma 3, since we have .
To finish the proof, we establish both properties for general randomised moves and . We know that ’s and ’s supports are equivalent Dirac moves by Lemma 2. We start by selecting some , in order to reuse the results above. We have:
[TABLE]
So, summing up:
[TABLE]
However:
[TABLE]
Therefore establishing (i).
Finally, we proceed similarly for . Again, we start by fixing . 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 -admissible strategies are exactly those that are both -LA and -SCO (Theorem 1). Then, we show that admissible strategies always exist in concurrent games (Theorem 1).
To establish Theorem 1, we need an ancillary lemma, which relates the notions of -admissibility and the notions of -LA. To this end, we draw a link between (global) equivalence of strategies (in terms of ) and the local equivalence of moves (in terms of ). For all player strategies and all , let us define as , i.e., the set of histories of that have value . Then:
Lemma 5**.**
*Let and be two player strategies s.t.:
(i) is -LA; and
(ii) for all histories : implies that and are -winning from .
Then, the following conditions are equivalent:*
- (1)
* for all ;* 2. (2)
* and for all ;* 3. (3)
**
Proof.
Proof of : By induction and application of Lemma 4.
Proof of We assume that , and show that .
It suffices to take an arbitrary and show that iff . We first show that:
[TABLE]
This can be shown by induction using Lemma 4 where the base case is and the induction step is that implies:
[TABLE]
We decompose the set of runs as . When intersecting with , the last set in the union becomes empty and we have:
[TABLE]
Hence for , where we used that implies almost surely because is winning from histories of value .
Hence it suffices to show that and . The former equality is due to (3). To prove the latter equality, we write for ,
[TABLE]
This equality traduces the decomposition of the even into the disjoint events parametrised by the history of value [math] just before entering . Using (4), Lemma 4 and (3) we deduce that , ending the proof.
**Proof of : **Straightforward. ∎
Theorem 1** **(Characterisation and existence of admissible
strategies).
The following holds for all strategies in a concurrent game with semantics :
- (i)
* is -admissible iff is -LA and -SCO; in the special case of simple safety objectives, if is -LA then is -admissible.* 2. (ii)
there is a -admissible strategy such that .
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).
” is -admissible” implies ” is -SCO”: We show the contrapositive. Let be a strategy that is not -SCO, and let us show that is not -admissible. Since is not -SCO, there is, by definition of -SCO, a history s.t. . Recall that . Hence, implies that and that there exists a strategy s.t. . Consider the strategy that plays like and switches to after history . We claim that . Observe that, by construction: . Note also that is not possible, because this means that all continuations of are losing for , so it is not possible to have with . So we have necessarily and . This means that is winning from (against all possible strategies of ), while, by definition of , is, from , losing for against at least one strategy of . Hence, and is not -admissible.
” is -admissible” implies ” is -LA”: We show the contrapositive: we assume that is not -LA and show that is not -admissible. There exists a history such that is -dominated at by an -LA move that can be chosen Dirac by virtue of Lemma 2 (i). There exists such that (otherwise all the moves of the support of would be equivalent to the -LA move and so would be by Lemma 2 (ii)). We already saw in the proof of Lemma 2 (i), that where is the strategy that plays like everywhere except in where it plays instead of . Then it suffices to show that is -dominated. Using Lemma 3 and notation therein with , we know that for every , and if then . Here we can reuse the end of the proof of Lemma 3 to find a strategy such that and that satisfies the further properties that it is -SCO at for every , and it plays as in every proper prefix of . It remains to show that there exists a profile such that and . Using Lemma 3, this time with we get the existence of a Dirac move such that . We define such that , and a further property depending on cases described as follows. If then and we further require that . If then and we further require that . In both cases it holds that and . So and . We conclude that is not -LA because .
” is -SCO and -LA” implies ” is -admissible”: Let be a strategy that is both -LA and -SCO. We show that for every such that implies ; which is a way of proving that is -Admissible. Let such that . We can assume without loss of generality that is winning from histories of value (otherwise it suffices to change so that when a history of value it switches to a winning strategy from that history). we deduce that for every , then because is -LA at . We can apply Lemma 5, and deduce that as required.
In simple safety games: ” is -LA” implies ” is -admissible”: To establish this case, we prove that, in simple safety games, ” is -LA” implies ” is -SCO”. This implies that all -LA strategies are also -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 ). 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 , we build a new Dirac -LA strategy , s.t., for all histories , is an arbitrarily chosen action from . By Lemma 2, point (iii), is also -LA. We claim that is value-preserving i.e., for all histories : , for all (assuming , and hence , are player strategies). In other words, by playing , player 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 is S-winning, then is S-winning too. So is dominated by and it is sufficient to prove that is admissible to show that is admissible too.
So, when states of value are entered, ensures that they are never left, and is thus winning from states of value . On the other hand, when a history of value [math] is entered, will also ensure that only histories of value [math] or are visited. In both cases, the 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 ).
We conclude that is -SCO. Since it is also -LA, is admissible. Hence, is admissible too.
Now, we move to the proof of point (ii).
Let be a strategy for player , we build an admissible strategy that weakly dominates . This proof is similar to the proof of a similar result for SCO strategies in turn based games ([6, Lemma 7]). The strategy is built dynamically along runs. It plays a winning strategy as soon as the current history begins to be of value . When the history begins to be of value , there is nothing more to do, the strategy can play arbitrarily. Consider now, runs in which the value is always [math]. The strategy keeps in memory a wished strategy for himself and a wished strategy of player such that . The strategies and are inductively defined as follows. At the beginning, , and are chosen such that and such that is -admissible. Here and below if satisfies these properties then the choice is made by default, otherwise another strategy is chosen (and it dominates ). After history , plays . If after some history the continuation chosen is not in (this is the case only if player plays something else than ), then and are chosen such that is -admissible and . Otherwise, if the wished profile is followed then the wished strategy for player is left unchanged (); the wished strategy for player is left unchanged () if is -admissible and otherwise is defined as a strategy that plays an admissible moves in and that dominates . The constructed strategy is -LA. It is also -SCO because from every history of value [math], and from every history of value , is winning. plays as by default or a strategy that dominates . At the end is an admissible strategy that weakly dominates . ∎
Example 6**.**
We consider again the example in Figure 2, and consider strategies and as defined in Example 1. Remember that these two strategies do their best to reach , and that, from , plays deterministically , while plays and with equal probabilities. From Example 3, we know that is S-SCO but not A-SCO; while is A-SCO but not S-SCO. Indeed, we have already argued in Example 2 that is not A-admissible, and that is not S-admissible. However, from Example 4, we know that is S-LA and that is A-LA. So, by Theorem 1, is S-admissible and is A-admissible as expected.
Finally, we close the section by a finer characterisation of -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 .
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 ) in the almost sure semantics:
Proposition 1**.**
For all player strategies in a concurrent game with :
- (i)
If is A-admissible then there exists a strategy that plays only Dirac moves in histories of value such that . 2. (ii)
If is S-admissible then there exists a Dirac strategy such that .
Proof.
Take is A-admissible. We define as follows. From histories of value , plays arbitrary Dirac strategies. From histories of value , plays winning strategies. If we can further requires that such winning strategies are Dirac. If there exists histories of value [math] then necessarily the initial state is such a history and we build inductively as follows such that . Consider , then define to be an arbitrary Dirac move . Then by Lemma 2 (iii) and the fact that is -LA we deduce that ; The histories of the form that are in are exactly those that belongs to (see Lemma 4). By induction, and for every , . We can use Lemma 5 and deduce that with Dirac in histories of value , and when . ∎
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 -player game) to the synthesis of a winning strategy in a -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 is given by an LTL formula. Such games are solvable using techniques presented in [10].
More precisely, from a concurrent game in the semantics and player , we build a game 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 corresponding to the game in Figure 2 is given in Figure 3. The main ingredients for this construction are the following.
(i) In , the protagonist is player , and the second player is .
(ii) Although randomisation is needed to win in such games in general, we interpret 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 (randomisation does not matter if the value is since the objective is lost anyway). Hence we define winning condition to be enabling us to consider only histories of values [math] in ; and thus hiding the parts of the game where randomisation might be needed. We also prove that we can restrict to Dirac strategies for when it comes to admissible strategies.
(iii) In order to restrict the strategies to admissible ones, we only allow -LA moves in . These moves can be computed by solving classical -player games ([2]) using Lemma 3. For example, in Figure 3, moves and are removed since they are not A-LA.
(iv) Last, since -admissible strategies are those that are both -LA and -SCO (see Theorem 1), we also need to ensure that the players play -SCO. This is more involved than -LA, as the -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 , the moves that have been played by all the players to reach the state. For example, in Figure 3, the state labelled by means that has reached , and that the last actions played by the players were and respectively. However, players’ strategies must not depend on this extra information since they do not have access to this information in either. We thus interpret as a game of imperfect information where all the states labelled by the same state of are in the same observation class. Thanks to these constructions, we can finally encode the fact that the players must play -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 -regular objectives. The values of the histories depend thus only on their last states, i.e. for all pairs of histories and : implies that . We thus denote by the value of all histories s.t. . Last, we assume that a player cannot play the same action from two different states, i.e. , . Thus, we say that a given move is -LA, meaning that is -LA from all histories ending in the unique state where is available.
The game
Let us now describe precisely the construction of . Given an -player concurrent game with winning condition considered under semantics , and given a player , we define the two-player zero-sum concurrent game where:
(i) ;
(ii) is the set of Dirac -LA moves in ;
(iii) is the initial state;
(iv) is such that is the set of Dirac -LA moves of in , for all ;
(v) is s.t. for all : is the set of moves of in s.t. for all , is a Dirac -LA move;
(vi) updates the state according to , remembering the last actions played: and for all .
Note that the game depends on whether or because the two semantics yield different sets of LA-moves. However, we interpret in the sure semantics, so both players can play Dirac strategies only in .
Let us now explain how we obtain an imperfect information game by defining an observation function . Note that histories in are of the form: . Then, let be the mapping that, intuitively, projects moves away from states. For example, in Figure 3, states with observation are in the dashed rectangle. That is: for all states , and . We extend to histories recursively: and . To make a game of imperfect information, we request that, in , players play only strategies s.t. whenever .
We relate the strategies in the original game with the strategies in , which we need to extract admissible strategies in from the winning strategies in and thus perform assume-admissible synthesis. First, given a player strategy in (i.e., ), we say that a strategy is a realisation of iff:
(i) is Dirac; and
(ii) for all .
Note that every -LA strategy admits realisations in . Second, given a player Dirac strategy in (i.e., ) we say that is an extension of iff, for all : .
The assume-admissible synthesis technique
As explained above, the assume-admissible rule boils down to computing a winning strategy for player in w.r.t. to winning condition , and extracting, from , the required admissible strategy in .
We will now formally define . Let be a player (in ); and let us denote by the (unique) state from which is available, for all actions . We define as
[TABLE]
That is, when , in , player has played from and, due to player ’s choice, has reached . However, with another choice of player , the game could have moved to a different state from which can help to win as . Intuitively, in runs that visit states of value [math] infinitely often, states from should be visited infinitely often for player to play SCO, i.e. such runs might not be winning, but this cannot be blamed on player 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 . 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 and . Let us define
To establish the correctness of this approach, we need several auxiliary lemmas.
Lemma 6**.**
If a strategy is -admissible then for all of its realisations , .
Proof.
Assume toward a contradiction that there is a -admissible strategy for which there exists a realisation that does not satisfy . We can further assume wlog. that plays Dirac moves in states of value [math]. There is a run that does not satisfy . More precisely, satisfies
[TABLE]
The run does not satisfy but all values of its prefixes are equal to [math] and there is such that for every , . We now show that for every , such that , it holds that . If then . If then there exists for which, and . Let , , . as a prefix of has value [math] so is Dirac and thus equal to . Let such that , . From we know that . We have found a prefix of that has value , thus . We have proved that for all run such that , it holds that . This implies that proving that is not -SCO and hence not -admissible. This is a contradiction. ∎
Lemma 7**.**
Given a -admissible strategy and one of its realisation. If a run satisfies in then there exists a profile of -admissible strategies such that .
Proof.
For every there exists moves such that and . For every , let be a strategy such that for every , and that plays an admissible strategy as soon as the current history is not a prefix of . We now show that . Denote by the Dirac move played by in . Since is -admissible; for every , is -LA and by Lemma 2 (iii) equivalent to the move of its support , then by Lemma 4, we get . This implies that .
We now show that is admissible in for every . It is clearly -LA as the moves are -LAs and plays -LA moves at histories not prefix of . It is also -SCO at histories not prefix of . We now show that is -SCO at every .
If then by , is winning for , and hence so is . As is a -LA move for every , all histories of the form for and their successors through have value . Consider a profile such that , , we show that . We do this part of proof for (the proof for is a bit easier and omitted). We show that . For this, we decompose the set into disjoint sets of runs:
[TABLE]
where the last union range over the state . The histories quantified above have value , and is A-admissible at these histories by construction since the histories are not prefixes of . Hence, A-winning from these histories, so . because . The set 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 .
If . We show that there exists a profile such that , and . Let . If then it suffices to take . Otherwise we begin to show that there is such that . Assume toward a contradiction that such a does not exists, then tells us that there exists such that or . Necessarily because as -LA moves only are played the states of value cannot be escaped once entered. In the case , satisfies and hence by virtue of . This contradict the fact that we are considering the case . Consider now that . Let be the unique number in such that and . Since , , from which we deduce that . This contradicts the fact that is a -LA move in a history of value [math]. We have showed the existence of a prefix length such that and we resume the proof of . There exists a state such that . Moreover is -admissible from , so there is a profile such that , and . Since , this implies that as required.
It remains the case of histories prefix of such that . This case is straightforward because the following sequence of inequalities holds for every history . At the end, for every , is -admissible as both -LA and -SCO, and . ∎
Lemma 8** (Admissible and dominant synthesis).**
In concurrent games with prefix independent -regular winning conditions with semantics , given a finite memory strategy for player that is -LA, one can construct effectively a finite memory strategy such that .
Proof.
We assume that the strategy is given by a stochastic Moore machine with set of memory states , with a designated initial memory state and such that after an history , the machine is in memory state . Each such memory state is labelled with a move noted . If we take the product of with the game , we obtain a structure with states that are pairs where is a state of the original game and is a memory state of . This product can be seen as a new Moore machine that behaves exactly as . From now on, we make the hypothesis that has this state space.
We note the value of state in , this value is well defined as is prefix independent, and we note the value of the strategy for any history that ends up in state of the and memory state of the machine.
As the strategy is -LA, if it is not admissible then it must be the case that there are state , memory state , and histories such that after history , the game is in state , is in state , and , i.e. is a witness that shows that is not SCO. Then, we will modify systematically in a way that it behaves as in all other histories and plays SCO in the histories that witness the fact that is not SCO.
We only need to consider the two following cases:
and are such that: and , then we replace by a sub-machine that implements a -winning strategy from . We know that finite memory machines that are -winning always exist and can be computed effectively for all -regular objectives. 2. 2.
and are such that: and , then we replace by a sub-machine that plays any admissible strategy from . 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 , a state , and a player , 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 , then the machine plays a finite state -winning strategy, such a finite memory strategy always exists and can be computed effectively.
- •
if the value of , then the machine plays arbitrarily.
- •
if the value of , then the machine selects a finite lasso-shape path such that is compatible with -LA moves of player and such that . Such a finite lasso-path always exists as . 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 , and if there is a deviation, the new state of the game is and the three rules here are applied from (according to the value of state ).
Clearly, if entering a state 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 -LA moves and from is such that , then we conclude that the strategy is -SCO and -LA and thus -admissible. So, we are done. ∎
Theorem 2** (Assume-admissible synthesis).**
Player has a -admissible strategy that is -winning against all player -admissible strategies in iff Player has an S-winning strategy in for the objective . Such a -admissible strategy can be effectively computed (from any player S-winning strategy in ).
Proof.
Completeness: Assume there exists an admissible strategy that wins against every admissible strategy. Let be a realisation of . Note that every runs that satisfies also satisfies . The other runs satisfy ; for these runs we show that . So let be such that . By Lemma 7, there exists that only contains admissible profiles such that . By assumption is winning for , hence so is .
Correctness: We show the following stronger statement. If a strategy is winning for in then one can construct a strategy admissible that wins against every profile of admissible strategies as follows:
(i) take an extension of ;
(ii) modify into that plays a winning strategy as soon as a history of value is entered;
(iii) use Lemma 8 to design an admissible strategy that weakly dominates .
We do the proof for the almost-sure semantics only, that is, for . The slightly simpler but similar proof for is omitted. We first show that if a strategy is winning for in then for every extension of and every profile of admissible strategies, it holds that .
Let be a profile of admissible strategies. Note that is equivalent to . For , is admissible, so, winning from histories of value , hence and we have . To show that this probability is null it suffices to show that every run that satisfies also satisfies . Take such a run , then there is a sequence of move profile such that and . Define the run by for and and note that . We also have that is a run of and for of where is any realisation of for which for every . The run satisfies by assumption on and because all the are admissible (Lemma 6). Putting all the things together satisfies and so does . We conclude that satisfies that for every profile of admissible strategies, it holds that . By construction wins against every profile for which . So is A-winning against every profile of A-admissible profile. Since , we deduce that is A-winning against every A-admissible profile. ∎
Let us explain how we build a strategy in with the desired properties, from any player strategy enforcing in . Remember that ensures that the players play -LA moves only. We will use to make sure that, when SCO strategies are played by (relying on the extra information we have encoded in the states), then reaches a state of value . First, consider for . Runs that satisfy this formula are either those that visit states of value [math] only finitely often (); or those that stay in states of value [math], in which case they must be either winning () or visit infinitely often states where Player could have been helped by the other players (). This is a necessary condition on runs visiting only value [math] states for the strategy to be SCO. Next, observe that states that if a history of value is entered then Player must win. This allows us to understand the left part of the implication in : the implication can be read as ‘if all other players play a -admissible strategy, then either should win () or a state of value for player should eventually be visited ()’. Then a strategy (in ) that wins against admissible strategies can be extracted from a winning strategy (in ) in a straightforward way, except when enforces to reach a state of value ( in ). In this case, cannot follow , but must rather switch to a winning strategy, which:
(i) is guaranteed to exist since the state that has been reached has value ; and
(ii) can be computed using classical techniques [10].
The strategy is not necessarily admissible but by Theorem 1 (i), there is an admissible strategy with . By weak domination, wins against more profiles than , in particular, it wins against the profiles of admissible strategies of the other players.
Example 7**.**
In our running example, observe that since there is no state of value in . Hence, . 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 (under the sure semantics), player 1 must ensure to reach as long as player 2 visits the set of bold states in Figure 3 infinitely often. A winning strategy in consists in (eventually) always playing from all states in the dashed rectangle; and from \big{(}s_{1},(b,b^{\prime})\big{)}. Observe that this strategy is compatible with . From , we can extract an admissible player strategy in : always play in ; always play in ; and play a winning strategy from (which is of value ), for instance: always play from like 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, -LA strategies are exactly the admissible strategies. So, can simply build from by pruning the actions which are not -LA (the labelling by actions is not necessary anymore since its sole purpose is to enforce SCO), and look for a player winning strategy in the resulting game.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Brandenburger Adam, Friedenberg Amanda, H Jerome, et al. Admissibility in games. Econometrica , 2008.
- 2[2] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM , 49(5):672–713, 2002. URL: \url http://doi.acm.org/10.1145/585265.585270, \href http://dx.doi.org/10.1145/585265.585270 \path doi:10.1145/585265.585270.
- 3[3] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking (Representation and Mind Series) . The MIT Press, 2008.
- 4[4] Dietmar Berwanger. Admissibility in infinite games. In STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings , number 4393 in Lecture Notes in Computer Science, pages 188–199. Springer, 2007. URL: \url http://dx.doi.org/10.1007/978-3-540-70918-3_17, \href http://dx.doi.org/10.1007/978-3-540-70918-3_17 \path doi:10.1007/978-3-540-70918-3_17.
- 5[5] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Nash equilibria in concurrent games with Büchi objectives. In Proceedings of the 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’11) , volume 13 of Leibniz International Proceedings in Informatics , pages 375–386, Mumbai, India, dec 2011. Leibniz-Zentrum für Informatik.
- 6[6] Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, and Ocan Sankur. Admissibility in Quantitative Graph Games. In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) , volume 65 of Leibniz International Proceedings in Informatics (LIP Ics) , pages 42:1–42:14, Dagstuhl, Germany, 2016. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: \url
- 7[7] Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. In Luca Aceto and David de Frutos-Escrig, editors, CONCUR , volume 42 of LIP Ics , pages 100–113. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. \href http://dx.doi.org/10.4230/LIP Ics.CONCUR.2015.100 \path doi:10.4230/LIP Ics.CONCUR.2015.100.
- 8[8] Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. Acta Inf. , 54(1):41–83, 2017. URL: \url http://dx.doi.org/10.1007/s 00236-016-0273-2, \href http://dx.doi.org/10.1007/s 00236-016-0273-2 \path doi:10.1007/s 00236-016-0273-2.
