1 Introduction
Computer science models systems interacting concurrently with their environment via infinite duration twoplayer win/lose games played on graphs: a play starts at a state of the graph, where the players concurrently choose one action each and thus induce the next state, and so on for infinitely many rounds. The winning condition is a given subset of the infinite sequences of states, and Player 1 wins the play iff the sequence of visited states belongs to . A strategy of a player prescribes one action depending on what has been played so far, and a winning strategy is a strategy ensuring victory regardless of the opponent strategy.
There are games where neither of the players has a winning strategy, but Borel determinacy [25] guarantees the existence of a winning strategy in games where the players play alternately and the winning condition is a Borel set. Under Borel condition again, Blackwell determinacy [26] guarantees a weaker conclusion when the players play concurrently: there exists a value such that for all
the players have stochastic strategies guaranteeing victory with probability
and , respectively.In the special case of concurrent games played on finite graphs with regular winning conditions, [11] designed algorithms to decide the existence of (stochastic) strategies that are winning, winning with probability one, and winning with probability for all . [11] also mentions a threestate game where only the latter exist, which exemplifies the complexity of the concurrent regular games on finite graphs. Then [6] studied concurrent prefix independent winning conditions, which is strictly more general than the regular conditions, and [13] further improved upon some results. Some of these results were extended recently to multiplayer multioutcome games, see e.g. [3], [15].
The new games This article studies slightly different games: when the players concurrently choose one action each, it also produces a color; the winning condition is now a given subset of the infinite sequences of colors; and Player 1 wins the play iff the produced sequence of colors belongs to . There are two differences between the classical games and the new games. First, the winning condition does not involve the visited states but the transitions instead; second it does so indirectly, via colors labeling the transitions. E.g. in the game on the lefthand side of Figure 1, starting at , the action sequence yields the state sequence and the color sequence .
There are several reasons why these new games are interesting.

The classical games can be encoded easily into the new ones by using state names as colors. Variants such as the games with colored states, or the colorless games with winning condition on the transitions can also be encoded easily into the new games.

The converse encoding may increase the state space (to infinity for games with infinitely many actions). Note that the transitionversusstate issue was already studied in the turnedbased setting in [10]. Likewise, colorless games are encoded easily in games with colors without size increase, and colors usually lead to more succinct winning conditions.

Colors are widely used in turnbased games, and for all games they help to study the winning conditions independently from the game structure, and thus to approximate or even characterize nice winning conditions for classes of games (usually simple to check) rather than for single games (usually more accurate but harder to check). This is exemplified by the difference between Theorems 5 and 7 in [27].

Whereas classical onestate games are trivial, the new onestate games are fairly complex and constitute a nice intermediate object towards the understanding of the more complex general games. Likewise, some onestate (aka stateless) objects from the literature are interesting in their own right: [1]
studied onestate multiobjective Markov decision processes; vector addition systems (VAS,
[17]) are still studied despite the vector addition systems with states (VASS, [16]); the Minkowski games [24] defined with finite sets are a special case of the onestate games from this article.
The main results

If is closed under interleaving and prefix removal, and if states and colors are finitely many, the existence of a Player 1 winning (finitememory) strategy is equivalent to the existence of winning (finitememory) strategies in finitely many derived oneplayer games.

If, in addition, is factorprefix complete and there are finitely many actions, either Player 1 has a winning strategy from one state, or every Player 2 constant (stronger than positional!), positive, stochastic strategy is winning almost surely from all vertices. This is semirandom determinacy.

Onestate games enjoy a stronger conclusion under somewhat weaker assumptions: if the winning condition is factorset complete and closed under interleaving, if Player 2 has finitely many actions, either Player 1 has a winning strategy, or every Player 2 constant, positive stochastic strategy is winning almost surely.
The finitary flavor of the above characterizations yields decidability and memory sufficiency, in the rough range of double exponentials in the number of states times the number of colors.
In the context of semirandom determinacy, a neutral, random Player 2 is therefore as bad for Player 1 as a hostile environment. Also, the victory is clearcut in the above results: no need for approximate optimal strategies, no need for the notion of value, etc. This is due to the assumptions, and it is legitimate to wonder how restrictive they are.
Several classical winning conditions from computer science are closed under interleaving, see Section 5. The Muller condition is not, but the parity condition is, so the first characterization result extends to the concurrent Muller games via the Last Appearance Record (LAR), as done in [28]. So, closeness under interleaving is not as restrictive as it may seem.
Fewer classical winning conditions are factorprefix complete (defined in Section 3.2), but the boundedness condition from [24] and a variant of the regular languages are both closed under interleaving and factorprefix complete. The variant is as follows: each produced color requests some combinations of colors to occur in the future. In winning plays, the number of currently unsatisfied requests should be uniformly bounded over time. It may be relevant even as a business model: at every time unit the system can pay penalties for every currently unsatisfied request, which may be covered by greater, albeit bounded, instantaneous income.
The above variant relates to the notion of fairness, which requires that cofinitely many requests are eventually satisfied. The finitary fairness [2] additionally requires uniformly bounded response time. This idea was use in [12] to study temporal logic, and in [9] to study finitary parity games. Requiring uniformly bounded response time (or variants thereof) to study games has been further used later, e.g. in [5]. However, these notions of fairness do not enjoy closeness under interleaving and factorprefix completeness. (Details in Section 5.)
Related works The semirandom determinacy implies the bounded limitone property from [11] for the new games: if one state has positive value, one state has value one.
Corollary 3.1 generalizes the nice Theorem 4 from [18]. Note that the convexity of winning conditions defined in [18] is essentially the same as the interleaving closeness defined here.
This article also shares similarities with [14]: both use abstract winning conditions, and both characterize the existence of winning strategies in twoplayer games by the existence of winning strategies in finitely many derived oneplayer games. Several articles adopted a similar approach: [19] and [20] reduce multiplayer multioutcome Borel games to simpler twoplayer win/lose Borel games, and characterize the preferences and structures that guarantee the existence of Nash equilibrium in infinite treegames; [21] does the same to characterize the preferences that guarantee the existence of subgame perfect equilibrium (at low levels of the Borel hierarchy); [23] does the same to almost characterize the existence of finitememory Nash equilibrium in games on finite graphs; [22] reduces oneshot concurrent twoplayer multioutcome games to simpler oneshot concurrent twoplayer win/lose games, with applications to generalized Muller games and generalized “parity” games.
2 Definitions
The folklore Observation 2 below will be used extensively to lift properties from finite words to infinite words. It will be first explicitly invoked, and then only implicitly used.
Observation .
Let be such that . Then can be uniquely extended to such that for all and .
Games A game (with colors and states) is a tuple such that

and are nonempty sets (of actions for Player 1 and Player 2),

is a nonempty set (of states),

(is the initial state),

(is the state update function).

is a nonempty set (of colors),

(is a color trace),

(is the winning condition for Player 1)
Histories The full histories (full runs) of such a game are the finite (infinite) words over , the Player 2 histories (Player 2 runs) are the finite (infinite) words over , and the Player 1 histories (Player 1 runs) are the finite (infinite) words over .
Strategies A Player 1 strategy is a function from to . Informally, it requires Player 1 to remember exactly how Player 2 has played so far, and it tells Player 1 how to play.
Induced histories The function is defined inductively below. As arguments it expects a strategy and a Player 2 history in , and it returns a full history: the very full history that, morally, should happen if Player 1 followed the given strategy while Player 2 played the given Player 2 history. and .
By Observation 2 the function is extended to expect opponents runs in and return full runs: is the only action run whose prefixes are the for .
Winning strategies A Player 1 strategy is winning if for all . If there is a Player 1 winning strategy in a game, one says that Player 1 wins the game.
Extending the update and trace functions The state update function is extended to inductively: and . Using , the trace function is naturally lifted to full histories by induction: and . The trace is further extended to full runs by Observation 2. When considering several games, indices may be added to the corresponding and .
Memory A Player 1 strategy is said to use memory , or memory size , if there exist a set and , and two functions and such that , where is defined inductively by and . If is finite, is called a finitememory strategy. Note that every Player 1 strategy uses memory .
Oneplayer games Intuitively, a oneplayer game (with colors and states) amounts to a game where Player 2 has only one strategy available, i.e. . Formally, it is a tuple such that , , and are nonempty sets, , , , and . In this context, the full histories (full runs) of such a game are the finite (infinite) words over , and the Player 2 histories of Player 1 are the natural numbers (telling how many rounds have been played). There is only one Player 2 run, namely . Then, a Player 1 strategy is a function from to , and the notation for the induced full histories is overloaded: and . By Observation 2 the function is (again) extended: is the only action run whose prefixes are the for . A Player 1 strategy is winning if .
Prefix removal A set of infinite sequences is closed under prefix removal if the tails of the sequences from the set are again in the set. Formally, is closed under prefix removal if the following holds: . Note that closeness under prefix removal is weaker than the prefix independence assumed in [6], [13], and [18].
Interleaving Interleaving two infinite sequences consists in enumerating sequentially (part of) the two sequences to produce a new infinite sequence. For example, interleaving and can produce the sequences (perfect alternation), , and (by enumerating the first sequence only), but not the sequences or .
Delayed response Consider a game with finite and . For every let be the elements of , where for all . The elements of are called the Player 2 delayed responses. Intuitively, a Player 2 delayed response amounts to a Player 2 positional strategy in (and only in) a sequentialized version of the game. In every round of this version, Player 1 chooses an action first, then Player 2 chooses an action (or more precisely some color and state among the pairs he could induce by choosing an action). E.g. is a delayed response for Figure 1. It means that at state , Player 2 selects for both actions of Player 1, and at state it selects if Player 1 chooses action . Note that delayed responses are not Player 2 (positional) strategies in the concurrent game, e.g. as is not achievable in any column.
Derived oneplayer games Let be a Player 2 delayed response. The oneplayer game is defined by , the projection of on the component such that . Intuitively, is the game obtained by letting Player 2 fix his strategy (to realize) in the sequentialized version of . For example, the game on the lefthand side of Figure 1 applied to the delayed response yields the game on the righthand side of Figure 1.
3 Main results
Section 3.1 characterizes the existence of Player 1 winning strategies and gives a complexity result. Section 3.2 defines additional concepts and uses the above characterization to characterize the existence of Player 2 everywherewinning stochastic strategies. Section 3.3 studies the special case of onestate games and presents the semirandom determinacy.
3.1 Existence of Player 1 winning strategies
Theorem 3.1 below characterizes the existence of Player 1 winning strategies in a game via the existence of winning strategies in finitely many derived oneplayer games. Theorem 3.1 afterwards drops the assumption on closeness under prefix removal from Theorem 3.1, but at the cost of a universal quantification over the starting state of the game. In Theorems 3.1 and 3.1, the finiteness and the closeness assumptions are used only to prove the 21 implications. Consider a game . If and are finite, and is closed under interleaving and prefix removal, the following are equivalent.

Player 1 wins .

Player 1 wins for all delayed responses .
If is finite and Player 1 wins, she can do it with memory size , where is a sufficient memory size to win the oneplayer games using , and . Consider games parametrized by . If and are finite and is interleavingclosed, the following are equivalent.

Player 1 wins for all .

Player 1 wins for all and delayed responses .
If the above holds, Player 1 wins every with memory size as in Theorem 3.1.
In games that are (or encode) turnbased games, the delayed responses are Player 2 positional strategies. So, restricting Theorems 3.1 and 3.1 to turnbased games yields Corollaries 3.1 and 3.1, respectively. Note that Corollary 3.1 generalizes Theorem 4 from [18] by only assuming closeness under prefix removal instead of prefix independence. This is significant since the safety condition is closed under interleaving and prefix removal, but is not prefix independent. Consider a game encoding a turnbased game. If and are finite, and is closed under interleaving and prefix removal, either Player 1 has a winning strategy or Player 2 has a positional winning strategy. Consider games parametrized by and encoding a turnbased games. If and are finite, and is closed under interleaving, either Player 1 wins all , or Player 2 has a positional winning strategy for some .
The characterizations from Theorems 3.1 and 3.1
yields decidability results and rough algorithmic complexity estimates in Corollary
3.1 below. Note that checking all the possible strategies using memory size given by Theorems 3.1 and 3.1 would be slower than Corollary 3.1. Let , let be closed under interleaving and prefix removal (resp. by interleaving), and let be such that for all finite and all oneplayer games , it takes at most computation steps to decide the existence of a (finitememory) winning strategy in the game. Then for all finite games it takes at mostcomputation steps to decide whether Player 1 wins (with finite memory).
(resp. computation steps to decide whether Player 1 wins (with finite memory) for all .)
3.2 Existence of Player 2 almost surely winning random strategies
Consider a game .
Probability distribution
A probability distribution on a finite set
is a function such that . Let us call the set of the probability distributions on .Stochastic strategies A Player 2 stochastic strategy is a function .
Induced stochastic histories The function is defined inductively below. As arguments it expects a Player 2 stochastic strategy and a Player 1 history , and it returns a probability distribution on . Informally, it tells the probability of a full history if Player 1 plays and Player 2 follows for many rounds. Formally, , and if , and .
Induced probability measure The function is extended to expect Player 1 runs: . Thus, every pair induces a probability measure on .
Almost surely winning stochastic strategies A Player 2 stochastic strategy is said to be winning almost surely if for all .
Factorprefix completeness Informally, is factorprefix complete if the following holds: if the prefixes of an infinite sequence occur as factors arbitrarily far in the tail of a second sequence in , the first sequence is also in . (A factor, aka substring, is a subsequence of consecutive elements.) Formally, is factorprefix complete if the following holds: .
In Theorem 3.2 below, a distribution is said to be positive if it assigns only positive masses. A (stochastic) strategy is said to be constant if it is a constant function, i.e. it returns always the same distribution, which is stronger than being Markovian, memoriless, or positional. [semirandom determinacy] Consider games parametrized by . If and are finite, if is factorprefix complete and closed under interleaving and prefix removal, the following are equivalent.

for all , Player 1 has no winning strategy in .

for all , Player 2 has a constant, positive, stochastic strategy winning almost surely.

for all every Player 2 stochastic strategy involving probabilities bounded away from (i.e. with positive infimum) wins almost surely.
So in the setting of Theorem 3.2, either Player 1 has a winning strategy for some , or every constant, positive strategy is winning almost surely, hence the determinacy. Also note that semirandom determinacy implies the bounded limitone property from [11] for the new games: if one state has positive value, one state has value one.
3.3 The special case of stateless (i.e. onestate) games
Stateless games Intuitively, a stateless game (with colors) amounts to a game with only one state, i.e. . Formally, it is a tuple such that , , and are nonempty sets, (as opposed to in the general case), and . Histories, runs, strategies, and induced histories are defined as in the general case . It is easier to extend the trace in this context: and .
Restricting Theorem 3.1 to stateless games yields a simpler Corollary 3.3 below. (Note that restricting Theorem 3.1 would yield a weaker variant of Corollary 3.3, i.e. additionally assuming closeness under prefix removal.) Memory size and algorithmic complexity estimates could be obtained essentially by replacing with in Theorem 3.1 and Corollary 3.1. Consider a game with finite and interleavingclosed . Let be the elements of . The following are equivalents.

Player 1 has a winning strategy (resp. finitememory winning strategy).

(resp. ),
where are the regular infinite sequences over .
Restricting Theorem 3.2 to stateless games cancels the universal quantification over states, but an even stronger version can be obtained: finiteness of and prefix removal closeness are dropped, and the assumption on factorprefix completeness is weaken into factorset completeness, as below.
Factorset completeness A language of infinite sequences is called factorset complete if the following holds: if a sequence in the language has factors of unbounded length over some , the language has a sequence over . This is formally defined by contraposition: is factorset complete if for all and for all , we have .
Observation .
Factorprefix completeness implies factorset completeness (finite alphabets).
[Stateless semirandom determinacy] Consider a stateless game with finite and . Let us assume that is interleavingclosed and factorset complete. Then either Player 1 has a winning strategy, or every Player 2 constant, positive, stochastic strategy is winning almost surely.
4 The proofs
Theorems 3.1 and 3.1 characterize a concurrent game by finitely many oneplayer games. A natural idea would be to split their proof into two parts: first, reduce the problem to turnbased games via the wellknown observation that a player has a winning strategy in a concurrent game iff she has one in the sequential version of the game where she plays first; second, use similar techniques as in [18]. For this to work, the sequential versions of the concurrent games must allow for colorless transitions, or a fresh color should be used for the transitions where Player 1 plays. This raises three issues: first, true colors should occur infinitely often in every run in these turnbased games, which would require a more complex notion of turnbased game; second, the winning condition should be rephrased to take the fresh color into account, and so should its closeness properties; third, it would be much difficult to obtain stronger results for the onestate concurrent games, since the onestate property may be hard to track through the translation into turnbased games. Instead, this article overcomes the concurrency directly thanks to Lemma 4.
Let be a family of sets. Then
.
Proof.
Towards a contradiction, let us assume the negation of the claim, i.e. . By collecting one witness for each , one constructs such that . In particular, taking yields for all , which contradicts the type of . ∎
Consider the onestate game in Figure 2 (to the left), where each cell encloses one vector of the real plane. Player 1’s objective is that the sum of the outcome vectors remains bounded, which is closed under interleaving and prefix removal, so is a concurrent version of the Minkowski games [24]. There are delayed responses, and five of the corresponding oneplayer games are displayed to the right in Figure 2. Player 1 wins , since for each the vector is in the convex hull of the three vectors defining . The idea is to let Player 1 play as if she were playing in parallel, more specifically in an interleaved way. Then, summing up the eight bounded trajectories yields a bounded trajectory for .
The main difficulty to play the in an interleaved way is that at every stage, Player 1 should pick an action such that whichever action Player 2 chooses, the resulting vector is exactly the expected one by the (fixed) winning strategy for some . Let be the function that tells which action should be played currently in each of the oneplayer games. By Lemma 4 there exists an action such that the following holds: if Player 2 chooses , there exists expecting the vector in the cell , and likewise if Player 2 chooses , there exists expecting the vector in the cell .
Let us now quickly mention semirandom determinacy. The proof of Theorem 3.2 below uses similar techniques as, e.g., a proof in the submitted journal version of [24].
Proof of 1 3 from Theorem 3.2.
Let and let be a Player 2 stochastic strategy that always assigns probability at least to every action.
For all , by contraposition of Theorem 3.1 let be a delayed response (in ) such that Player 1 loses the oneplayer game . For all , anytime a play reaches the state , the probability that from then on Player 2 follows for rounds in a row, as if secondguessing Player 1, is greater than or equal to .
Consider a play where Player 2 follows . Let be a state that is visited infinitely often. (Such a state exists since is finite.) Thanks to the argument above, for all , the probability that, at some point, Player 2 follows for rounds in a row from on is one. Since the countable intersection of measureone sets has also measure one, the probability that, for all , at some point Player 2 follows for rounds in a row from on is one.
Let be the corresponding full histories. Since and are finite, the tree induced by prefix closure of the is finitely branching, so by Koenig’s Lemma it has an infinite path , which corresponds to Player 2 following infinitely many rounds in a row. So . By factorprefix closeness the original play is also losing for Player 1, i.e. winning for Player 2. ∎
5 Applications
Abstract assumptions need not only be general, they also need to be practical. Section 5.1 shows that the closeness and completeness axioms enjoy nice algebraic properties: individually, w.r.t. Boolean combination, as well as collectively via the derived closure or completion operators. Section 5.2 mentions several classical or recent winning conditions from computer science and tells which of them satisfy the closeness and completeness axioms. Section 5.3 introduces the notion of bounded residual load as an alternative to the finitary fairness [2], and uses it to define a finitary variant of the regular languages that satisfies the closeness and completeness axioms.
5.1 Algebraic properties of the closeness and completeness axioms
Lemma 5.1 below shows how the axioms behave w.r.t. Boolean combination.

The set of the factorset complete languages is closed under union.

The set of the interleavingclosed languages is closed under intersection.

The set of the factorprefix complete languages is closed under intersection and union.
The set of the interleavingclosed languages is not closed under union: and are closed under interleaving (and by prefix removal), but is not. The set of the interleavingclosed languages is not closed under complementation: the interleaving of two infinite sequences that are not eventually constant is not eventually constant, but interleaving the eventually constant sequences and may yield . The set of the factorset complete languages is not closed under intersection: indeed, both twoelement sets and are factorset complete, but their intersection is not. The set of the factorset (prefix) complete languages is not closed under complementation: is factorset (prefix) complete, but is not.
The closeness under interleaving and prefix removal, and the factorprefix completeness induce closure operators. If a relevant winning condition fails to satisfy an equaly relevant axiom, such an operator conveniently constructs a (more generous, axiom satisfying) variant of the winning condition. The closure by prefix removal of a set consists in adding the tails of the sequences from the set; the closure by interleaving consists in adding sequences obtained by interleaving the sequences from the set; and the factorprefix completion consists in adding the sequences whose prefixes occur arbitrarily far in a sequence from the set. Note that factorset completeness does not induce a canonical closure operator due to the existential quantifier in its definition.
Lemma 5.1
below shows that the operators behave as expected. This is not for granted in general, as one may need to perform the addition operation an ordinal number of times. Here, one step suffices, which is convenient if computation is of concern.

Closure by prefix removal yields sets that are closed under prefix removal.

Closure by interleaving yields sets that are closed under interleaving

Factorprefix completion yields sets that are factorprefix complete.
Lemma 5.1 shows that the operators preserve the existing properties.(Lemma 5.1 is invoked as a proof technique.)

Closure by prefix removal preserves closeness under interleaving.

Closure by prefix removal preserves factorset and factorprefix completeness.

Closure by interleaving preserves closeness under prefix removal.

Closure by interleaving preserves factorset and factorprefix completeness.

Factorprefix completion preserves closeness under prefix removal.
5.2 Concrete winning conditions
The noncomprehensive list below displays classical or recent winning conditions from computer science. It especially shows that new winning conditions obtained by conjunction of older winning conditions have been recently studied, e.g. in [7] and [4].
Parity for some . A sequence is winning iff the least number occurring infinitely many times in the sequence is even.
Muller for some . Let be a set of subsets of . A sequence is winning iff the numbers occurring infinitely many times in the sequence constitute a set in .
Meanpayoff , and a sequence is winning iff the limit superior of the partial sums is nonnegative: is winning iff . (Variants exist with limit inferior or positivity instead of nonnegativity.)
Energy , and a sequence is winning iff its partial sums are nonnegative: is winning iff .
Boundedness [24] , and a sequence is winning iff its partial sums are uniformly bounded: is winning iff .
Discounted sum is a bounded subset of . Let and . A sequence is winning iff .
Energyparity [7] for some . The winning condition is the conjunction of the energy (first component) and the parity (second component) conditions.
Average energy [4] . The objective is to maintain a nonnegative energy while keeping the average level of energy below a threshold : a sequence is winning iff .
Observation .

The Muller and discounted sum conditions are not closed under interleaving.

The boundedness condition is factorprefix complete; the others are not.

The energy, energyparity, and discounted sum conditions are not closed under prefix removal; the others are.
The turnbased safetymeanpayoffparity games are halfpositionally determined. (By Corollary 3.1 and Section 5.1.)
It may be disappointing that the Muller condition is not even closed under interleaving, but Proposition 5.2 below extends Theorem 3.1 to the concurrent Muller games. Using results from [11] is likely to yield a better algorithmic complexity, though, but the point here is mainly that Theorem 3.1 can be extended.
Proposition .
[Similar to [11]] Consider the finite games where is a Muller condition. Deciding the existence of a Player 1 winning (finitememory) strategy can be done in big of
computation steps.
5.3 Bounded residual load
Unlike Theorems 3.1 and 3.1, Theorems 3.2 and 3.3 are not likely to be extended to include regular languages. Before defining a variant of the regular languages that satisfies the closeness and completeness properties from this article, let us consider notions of fairness that can be defined via a predicate on . Intuitivily is supposed to mean that the sequence has satisfied, with delay at most , a request that was formulated in at time .
There are several reasonable ways to express the good behavior of an infinite sequence using the . The classical definition of fairness requires that all problems be eventually solved (see below), or cofinitely many problems (see below), for a usual weakening that ensures prefix independence of the condition. Arguing that this kind of fairness gives no guarantee about response time, [11] strengthened fairness into finitary fairness, which requires the existence of a uniform bound on the waiting time (see below).
Yet another variant, bounded residual load (), is introduced below. It says that satisfies wrt bounded residual load, if the number of problems that have currently not yet been solved is uniformly bounded overtime.
Observation .



and are incomparable in general.
The finitary fairness and the like may be too strict for some applications: gladly accepting to wait time units, but categorically refusing to wait time units sounds unusual indeed. Instead, the system (which is responsible for solving the problems) could pay a penalty for each problem spending each time unit unsolved. Thanks to the bounded residual load, one has then the guarantee that the amount of money to be paid per time unit is bounded.
It is possible to combine the two ideas, though: by setting an acceptable response time and an acceptable uniform bound on the number of missed deadlines. This however, turns out to be equivalent to the simple , which argues for the robustness of the concept.
Observation .
Let , then .
A second justification for the is that it has nice properties that the other notions of fairness lack when is defined to minic regular languages, as shown below. Consider a nonempty set of colors and a function . A sequence is said to satisfy from position after delay , denoted , if the following holds.
Intuitively, each color is a problem or a request, and the problem may be solved in several ways, each way consisting in enumerating suitable colors quickly. (This might very well correspond to the positive fragment of some boundedtime temporal logic.) To simulate the parity condition, one can set and and for all . The corresponding is the parity condition with bounded residual load.
Lemma 5.3 below says that however may be instantiated, all Theorems 3.1, 3.1, 3.2, and 3.3 can be applied with the winning condition.
For every nonempty set of colors and every function , the winning condition is closed under prefix removal and interleaving, and factorprefix complete.
Even when simulates the parity condition as above, none of the corresponding , , or is both closed under interleaving and factorset complete. is not closed under interleaving: and , but , where can be obtained by interleaving and . is not factor setcomplete: , where , but altough factors of ’s occur with arbitrary length in . is neither: first, and , but , altough can be obtained by interleaving and ; second, as above for . Note that the windowparity condition [8],[5] is not closed under interleaving either, as again exemplified by and .
References
 [1] Rajeev Alur, Marco Faella, Sampath Kannan, and Nimit Singhania. Hedging Bets in Markov Decision Processes. In JeanMarc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1–29:20, Dagstuhl, Germany, 2016. Schloss Dagstuhl–LeibnizZentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2016/6569, doi:10.4230/LIPIcs.CSL.2016.29.
 [2] Rajeev Alur and Thomas A. Henzinger. Finitary fairness. ACM Trans. Program. Lang. Syst., 20(6):1171–1194, November 1998. URL: http://doi.acm.org/10.1145/295656.295659, doi:10.1145/295656.295659.
 [3] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Concurrent games with ordered objectives. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures, pages 301–315, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
 [4] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Averageenergy games. Acta Informatica, Jul 2016. URL: https://doi.org/10.1007/s0023601602741, doi:10.1007/s0023601602741.
 [5] Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 1416 September 2016., pages 135–148, 2016. URL: https://doi.org/10.4204/EPTCS.226.10, doi:10.4204/EPTCS.226.10.
 [6] Krishnendu Chatterjee. Concurrent games with tail objectives. Theoretical Computer Science, 388(1):181 – 198, 2007. URL: http://www.sciencedirect.com/science/article/pii/S0304397507005804, doi:https://doi.org/10.1016/j.tcs.2007.07.047.
 [7] Krishnendu Chatterjee and Laurent Doyen. Energy parity games. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, pages 599–610, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.
 [8] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and JeanFrançois Raskin. Looking at meanpayoff and totalpayoff through windows. Inf. Comput., 242:25–52, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.010, doi:10.1016/j.ic.2015.03.010.
 [9] Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn. Finitary winning in regular games. ACM Trans. Comput. Logic, 11(1):1:1–1:27, November 2009. URL: http://doi.acm.org/10.1145/1614431.1614432, doi:10.1145/1614431.1614432.
 [10] Thomas Colcombet and Damian Niwiński. On the positional determinacy of edgelabeled games. Theoretical Computer Science, 352(1):190 – 196, 2006. URL: http://www.sciencedirect.com/science/article/pii/S0304397505008303, doi:https://doi.org/10.1016/j.tcs.2005.10.046.
 [11] Luca de Alfaro and Thomas A. Henzinger. Concurrent omegaregular games. In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 2629, 2000, pages 141–154, 2000. URL: https://doi.org/10.1109/LICS.2000.855763, doi:10.1109/LICS.2000.855763.
 [12] Nachum Dershowitz, D. N. Jayasimha, and Seungjoon Park. Bounded Fairness, pages 304–317. Springer Berlin Heidelberg, Berlin, Heidelberg, 2003. URL: https://doi.org/10.1007/9783540399100_14, doi:10.1007/9783540399100_14.
 [13] Hugo Gimbert and Florian Horn. Solving simple stochastic tail games. In Proceedings of the Twentyfirst Annual ACMSIAM Symposium on Discrete Algorithms, SODA ’10, pages 847–862, Philadelphia, PA, USA, 2010. Society for Industrial and Applied Mathematics. URL: http://dl.acm.org/citation.cfm?id=1873601.1873670.
 [14] Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. In CONCUR 2005  Concurrency Theory, volume 3653 of Lecture Notes in Computer Science, pages 428–442. Springer Berlin Heidelberg, 2005.

[15]
Julian Gutierrez, Aniello Murano, Giuseppe Perelli, Sasha Rubin, and Michael
Wooldridge.
Nash equilibria in concurrent games with lexicographic preferences.
In
Proceedings of the TwentySixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 1925, 2017
, pages 1067–1073, 2017. URL: https://doi.org/10.24963/ijcai.2017/148, doi:10.24963/ijcai.2017/148.  [16] John Hopcroft and JeanJacques Pansiot. On the reachability problem for 5dimensional vector addition systems. Theoretical Computer Science, 8(2):135 – 159, 1979. URL: http://www.sciencedirect.com/science/article/pii/0304397579900410, doi:https://doi.org/10.1016/03043975(79)900410.
 [17] Richard M. Karp and Raymond E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147 – 195, 1969. URL: http://www.sciencedirect.com/science/article/pii/S0022000069800115, doi:https://doi.org/10.1016/S00220000(69)800115.
 [18] Eryk Kopczyński. Halfpositional determinacy of infinite games. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, pages 336–347, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.
 [19] Stéphane Le Roux. Infinite sequential Nash equilibrium. Logical Methods in Computer Science, 9, 2013. Special Issue for the Conference "Computability and Complexity in Analysis" (CCA 2011).
 [20] Stéphane Le Roux. From winning strategy to Nash equilibrium. Mathematical Logic Quarterly, 2014. (to appear).
 [21] Stéphane Le Roux. Infinite subgame perfect equilibrium in the hausdorff difference hierarchy. In Topics in Theoretical Computer Science  The First IFIP WG 1.8 International Conference, TTCS 2015, Tehran, Iran, August 2628, 2015, Revised Selected Papers, pages 147–163, 2015. URL: https://doi.org/10.1007/9783319286785_11, doi:10.1007/9783319286785_11.
 [22] Stéphane Le Roux and Arno Pauly. Infinite sequential games with realvalued payoffs. In Proceedings of LiCS, 2014.
 [23] Stéphane Le Roux and Arno Pauly. Extending finite memory determinacy to multiplayer games. In Proceedings of the 4th International Workshop on Strategic Reasoning, SR 2016, New York City, USA, 10th July 2016., pages 27–40, 2016. URL: https://doi.org/10.4204/EPTCS.218.3, doi:10.4204/EPTCS.218.3.
 [24] Stéphane Le Roux, Arno Pauly, and JeanFrançois Raskin. Minkowski games. In 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 811, 2017, Hannover, Germany, pages 50:1–50:13, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.50, doi:10.4230/LIPIcs.STACS.2017.50.
 [25] Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363–371, 1975. URL: http://www.jstor.org/stable/1971035.
 [26] Donald A. Martin. The determinacy of blackwell games. Journal of Symbolic Logic, 63(4):1565–1581, 1998. doi:10.2307/2586667.
 [27] Stéphane Le Roux and Arno Pauly. Extending finitememory determinacy to multiplayer games. Information and Computation, pages –, 2018. URL: https://www.sciencedirect.com/science/article/pii/S0890540118300270, doi:https://doi.org/10.1016/j.ic.2018.02.024.
 [28] Wolfgang Thomas. Languages, automata, and logic. In Salomaa A. Rozenberg G., editor, Handbook of Formal Languages. Springer, Berlin, Heidelberg, 1997.
Appendix A Existence of Player 1 winning strategies
a.1 More on interleaving
Interleaving two finite word consists in enumerating sequentially the two words to produce a new word. For example, interleaving and can produce the words and , but neither nor . Formally, interleaving finite words over some alphabet is defined by induction: for all and , set and .
Observation .
Interleaving finite words is associative and commutative.
Let us now give a possible formalization of the interleaving of infinite words. Let . Then iff there exist such that

,

,

.
Let . Then iff for all there exists such that for all and can be obtained by interleaving the .
Proof.
Let us first assume that , and let us prove by induction on that . For the base case, since for all . For the inductive case by definition of the interleaving of infinite words. By I.H . On the one hand, for all , from follows ; on the other hand, since . Therefore by definition of interleaving of finite words.
Conversely, let us assume that for all there exists such that for all and can be obtained by interleaving the . ∎
a.2 More on Lemma 4
Below is a short story that might help provide useful insight to some readers. Once upon a time, there was a capricious king who loved pastry. There were many bakeries in his kingdom, and each of them could bake a wide range of delicious cakes. Each shop would bake only one type of cake per day, though, and the only way to know which was to visit the shop. One morning, the king summoned his minister to bring him his favorite cake for dinner (among the cakes of the day). Unfortunately, the shops were far apart and one could only visit one of them within a day, and the king’s favorite depended on the cakes of the day in an irrational way. The minister considered buying a cake from some shop and lying about the cakes of the day in the other shops. But the king knew the range of each shop, what if there were no plausible lie? Desperate, the minister sought help from a mathematician: she enquired about the king’s preferences and the range of each shop, bought a cake from one shop, lied about the cakes of the day, and the king ate happily. Lemma 4 shows that the mathematician was bound to succeed: given the ranges of the shops and the king’s preferences, there always exists a safe shop. T
Corollary A.2 below is derived from Lemma 4 by partial Skolemization, i.e. by pulling the before the , and the before the , thus automatically yielding the and the , respectively. Whereas Lemma 4 could be invoked to characterize the existence of winning strategies, Corollary A.2 will be invoked to characterize the existence of winning strategies with (finite) memory, which will be constructed via the functions and . Note that in the statement of Corollary A.2 uses natural numbers as von Neumann ordinals. .
a.3 Using Lemma 4
Lemma 4 is then used in Lemma A.3 which factors out most of the proof burden of Theorems 3.1 and 3.1. Lemma A.3 involves games that are concurrent at fewer states than in the original game, and then the proofs of Theorems 3.1 and 3.1 proceed by induction on the degree of concurrency. To define these simpler games, consider .
States involving a player A state is said to involve Player 2 if
Comments
There are no comments yet.