University of Gothenburg,
Swedend.hausmann@liverpool.co.ukhttps://orcid.org/0000-0002-0935-8602Supported
by the EPSRC through grant EP/Z003121/1. University of Gothenburg,
Swedennir.piterman@chalmers.sehttps://orcid.org/0000-0002-8242-5357 Daniel
Hausmann and Nir Piterman [100]Theory of computation - Formal languages and
automata theory Both authors supported by the ERC Consolidator grant D-SynMA
(No. 772459).

# Faster and Smaller Solutions of Obliging Games

Daniel Hausmann  Nir Piterman

###### Abstract

Obliging games have been introduced in the context of the game perspective on
reactive synthesis in order to enforce a degree of cooperation between the to-
be-synthesized system and the environment. Previous approaches to the analysis
of obliging games have been small-step in the sense that they have been based
on a reduction to standard (non-obliging) games in which single moves
correspond to single moves in the original (obliging) game. Here, we propose a
novel, large-step view on obliging games, reducing them to standard games in
which single moves encode long-term behaviors in the original game. This not
only allows us to give a meaningful definition of the environment winning in
obliging games, but also leads to significantly improved bounds on both
strategy sizes and the solution runtime for obliging games.

###### keywords:

Two-player games, reactive synthesis, Emerson-Lei games, parity games

###### category:

##  1 Intro

Infinite duration games [GraedelThomasWilke02] and their analysis are central
to various logical problems in computer science; problems with existing game
reductions subsume model checking [BradfieldW18, HausmannS19] and
satisfiability checking [FriedmannLange13a, FriedmannLatteLange13] for
temporal logics (such as CTL or the $\mu$-calculus), or reactive synthesis for
LTL specifications [EsparzaKRS22]. Game arenas that are used in such
reductions typically incorporate two antagonistic players (called player
$\exists$ and player $\forall$ in the current work) that have dual objectives.
Then the reductions construct game arenas and objectives in such a way that
the instance of the original problem has a positive answer if and only if
player $\exists$ has a strategy that ensures that the player’s objective is
satisfied (that is, player $\exists$ _wins_ the game). _Solving_ games then
amounts to determining their winner. Games with Borel objectives are known to
be _determined_ [Martin75], that is, for each node in them, exactly one of the
players $i$ has a winning strategy of type $V^{*}V_{i}\to V$, where $V$ is the
set of game nodes, and $V_{i}$ the set of nodes controlled by player $i$.

_Reactive synthesis_ [PnueliR89] considers a setting in which a system works
within an antagonistic environment, and the system-enviroment interaction is
modelled by means of input variables from a set $I$ (controlled by the
environment), and output variables from a set $O$ (controlled by the system).
The synthesis problem then takes a logical specification $\varphi$ over the
variables $I\cup O$ as input and asks for the automated construction of a
system in which all interactions between the system and the environment
satisfy the specification; if such a system exists, then $\varphi$ is said to
be _realizable_. The reactive synthesis problem therefore goes beyond checking
realizability by also asking for a witnessing system in the case that the
input specification is realizable. While the problem has been shown to be
2ExpTime-complete for specifications that are formulated in LTL, a landscape
of algorithms and implementations has been developed that shows good
performance in (some) practical use cases (e.g. [LuttenbergerMS20, DijkAT24]).
The feasability of these algorithms is largely owed to an underlying reduction
to infinite-duration two-player games, most commonly with parity objectives.
Answering the realizability problem then corresponds to deciding the winner of
the reduced game, while the construction of a witnessing system for a
realizable specification corresponds to the extraction of a winning strategy
from that game. This motivates the interest not only in game solving
algorithms, but also in the analysis and extraction of winning strategies. In
particular, the amount of memory required by winning strategies in the types
of games at hand determines the minimum size of witnessing systems.

Building on the described game perspective on reactive synthesis, _obliging
games_ have been proposed to deal with the situation that a system might
trivially realize a specification by disallowing most or all interactions with
the environment (cf. [BloemEJK14, ChatterjeeHL10]). Obliging games address
this problem by requiring the system player to have a strategy that not only
always guarantuees that the system’s strong objective (say $\alpha_{S}$) is
achieved, but to also always keep an interaction possible in which intuitively
both players cooperate to achieve a second, weak, objective (say
$\alpha_{W}$). Such a strategy then is called _graciously winning_ for the
system player. For example, the generalized reactivity (GR[1]) setting (cf.
[BloemJPPS12]) incorporates $k$ different _requests_ and $k$ corresponding
_grants_ ($R_{i},G_{i}$ for $1\leq i\leq k$). Then the objective $\alpha_{S}$
states that ‘if all $R_{i}$ (requests) hold infinitely often, then all $G_{i}$
(grants) hold infinitely often’. In this setting, player $\exists$ may satisfy
the objective $\alpha_{S}$ trivially by simply ensuring that, for each
interaction, there is some $R_{i}$ that is eventually avoided forever. The
obliging game setting allows to address this situation by taking $\alpha_{W}$
to require that all $R_{i}$ hold infinitely often. Then a gracious strategy
for player $\exists$ has to ensure $\alpha_{S}$ (possibly by avoiding, on most
interactions, some $R_{i}$), but it also has to enable player $\forall$ to
additionally realize $\alpha_{W}$, thereby always enabling at least one
“interesting” interaction on which all $R_{i}$ and also all $G_{i}$ hold
infinitely often.

Previous approaches to the analysis of obliging games [ChatterjeeHL10,
MajumdarSchmuck23] have been largely based on a reduction to equivalent non-
obliging games in which the players still take single steps on the original
game graph, but in addition to that, game nodes are annotated with auxiliary
memory that is used to deal with the more involved obliging game’s objectives.
Obliging GR[1] games, as in the example above, have been considered under the
names of “cooperative” [BloemEK15] and “environmentally-friendly”
[MajumdarPS19]. Independent bespoke symbolic algorithms of slightly better
complexity than the general solution have been suggested.

In this context, the contributions of the current work are threefold:

  * •

We propose a novel perspective on obliging games that is based on considering
multi-step strategies of players in the original game, rather than emulating
single-step moves. In more detail, we provide an alternative reduction that
takes obliging games to equivalent non-obliging games in which the system
player commits to certain long-term behaviors, encoded by so-called witnesses,
which are just plays of the original game (we therefore call the resulting
games _witness games_). The environment player in turn can either check
whether a given witness is valid, that is, satisfies both $\alpha_{S}$ and
$\alpha_{W}$, or accept the witness and exit it at any game node that occurs
in the witness, thereby intuitively challenging the system player to still win
when a play only traverses the witness up to the exit node and then continues
on outside of the proposed witness; in the latter case, the system player has
to provide a new witness for the challenged game node, and so on. We use the
reduction to witness games to show determinacy of obliging games with Borel
objectives (however, with respect to strategies of type $V^{*}\to V^{\omega}$
for the system player, and strategies of type $V^{\omega}\to V\cup V^{\omega}$
for the environment player).

  * •

We show that witnesses for obliging games with $\omega$-regular objectives
$\alpha_{S}$ and $\alpha_{W}$ have finite representations, as they correspond
to (accepting) runs of $\omega$-automata with acceptance condition
$\alpha_{S}\land\alpha_{W}$; we call such representations _certificates_.
Using certificates in place of infinite witnesses, we modify witness games to
obtain an alternative reduction that takes $\omega$-regular obliging games to
_finite_ $\omega$-regular non-obliging games, called _certificate games_.
Technically, we present the reduction for obliging games with Emerson-Lei
objectives. During the correctness proof for this reduction, we show that the
memory requirements of graciously winning strategies for Emerson-Lei obliging
games depend only linearly on the size of $\alpha_{W}$, improving
significantly upon existing upper bounds [ChatterjeeHL10, MajumdarSchmuck23]
that are, in general, exponential in the size of $\alpha_{W}$.

  * •

The certificate games that we propose contain an explicit game node for any
possible certificate within an obliging game. Hence they are prohibitively
large and it is not viable to solve them naively. However, we show how a
technique of fixpoint acceleration can be used to speed up the solving process
of certificate games, replacing the exploration of all certificate nodes with
emptiness checking for suitable $\omega$-automata; this technique solves
certificate games by computing nested fixpoints of a function that checks for
the existence of suitable certificates. Thereby we are able to improve
previous upper runtime bounds for the solution of obliging games; in many
cases, our algorithm outperforms existing algorithms by an exponential factor.

Summing up, we propose a novel approach to the analysis of obliging games that
provides more insight in their determinacy, and for obliging games with
Emerson-Lei objectives, we significantly improve existing upper bounds both on
strategy sizes and solution time.

_Structure._ We introduce obliging games and related notions in Section 2. In
Section 3, we reduce obliging games to witness games and use the reduction to
show that obliging games are determined (for strategies with additional
information). Subsequently, we restrict our attention to $\omega$-regular
obliging games with Emerson-Lei objectives. In Section 4 we reduce witness
games with such objectives to certificate games and use the latter to obtain
improved upper bounds on strategy sizes in obliging games. In Section 5 we
show how certificate games can be solved efficiently, in consequence improving
previous upper bounds on the runtime complexity of solving obliging games.
Full proofs and additional details can be found in the appendix.

##  2 Preliminaries

We start by recalling obliging games and extend the setup from previous work
to use general Borel objectives in place of Muller objectives; we also
introduce the special case of obliging games with Emerson-Lei objectives, and
recall the definition of Emerson-Lei automata.

_Arenas, plays, strategies._ An _arena_ is a graph $A=(V,V_{\exists},E)$,
consisting of a set $V$ of _nodes_ and a set $E\subseteq V\times V$ of _moves_
; furthermore, we assume that the set of nodes is partitioned into the sets
$V_{\exists}$ and $V_{\forall}:=V\setminus V_{\exists}$ of nodes _owned_ by
player $\exists$ and by player $\forall$, respectively. We write $E(v)=\\{w\in
V\mid(v,w)\in E\\}$ for the set of nodes reachable from node $v\in V$ by a
single move. We assume without loss of generality that every node has at least
one outgoing edge, that is, that $E(v)\neq\emptyset$ for all $v\in V$. A
_play_ $\pi=v_{0}v_{1}\ldots$ on $A$ is a (finite or infinite) sequence of
nodes such that $v_{i+1}\in E(v_{i})$ for all $i\geq 0$. The length
$|\pi|=n+1$ of a finite play $\pi=v_{0}v_{1}\ldots v_{n}$ is the number of
vertices it contains; throughout, we denote the set $\\{0,\ldots,n\\}$ for
$n\in\mathbb{N}$ by $[n]$. By abuse of notation, we denote by $A^{\omega}$ the
set of infinite plays on $A$ and by $A^{*}$ and $A^{+}$ the set of finite
(nonempty) plays on $A$. A _strategy_ for player $i\in\\{\exists,\forall\\}$
is a function $\sigma:A^{*}\cdot V_{i}\to V$ that assigns a node $\sigma(\pi
v)\in V$ to every finite play $\pi v$ that ends in a node $v\in V_{i}$. A
strategy $\sigma$ for player $i$ is said to be _positional_ if the moves that
it prescribes do not depend on previously visited game nodes. Formally this is
the case if we have $\sigma(\pi v)=\sigma(\pi^{\prime}v)$ for all $v\in V_{i}$
and all $\pi,\pi^{\prime}\in A^{*}$. A play $\pi=v_{0}v_{1}\ldots$ is
_compatible_ with a strategy $\sigma$ for player $i\in\\{\exists,\forall\\}$
if for all $j\geq 0$ such that $v_{j}\in V_{i}$, we have
$v_{j+1}=\sigma(v_{0}v_{1}\ldots v_{j})$.

_Objectives and games._ In this work we consider two types of objectives:
_Borel objectives_ and _Emerson-Lei objectives_. Borel objectives are explicit
sets of infinite sequences of vertices. A set is _Borel definable_ if it is in
the $\sigma$-algebra over the open subsets of infinite sequences of vertices
$V^{\omega}$. That is, sets that can be obtained by countable unions,
countable intersections, and complementations from the open sets (sets of the
form $wV^{\omega}$ for $w\in V^{*}$). A play $\pi$ on $A$ _satisfies_ a Borel
objective $B$ if $\pi\in B$.

Emerson-Lei objectives are specified relative to a coloring function
$\gamma_{C}:E\to 2^{C}$ (for some set $C$ of colors) that assigns a set
$\gamma_{C}(v,w)\subseteq C$ of colors to every move $(v,w)\in E$; we note
that our setup is more succinct than the one from [ChatterjeeHL10] where each
edge has (at most) one color. A play $\pi=v_{0}v_{1}\ldots$ then induces a
sequence
$\gamma_{C}(\pi)=\gamma_{C}(v_{0},v_{1})\gamma_{C}(v_{1},v_{2})\ldots$ of sets
of colors. Emerson-Lei objectives are given as positive Boolean formulas
$\varphi_{C}\in\mathbb{B}_{+}(\\{\mathsf{Inf}\leavevmode\nobreak\
c,\mathsf{Fin}\leavevmode\nobreak\ c\mid c\in C\\})$ over atoms of the shape
$\mathsf{Inf}\leavevmode\nobreak\ c$ and $\mathsf{Fin}\leavevmode\nobreak\ c$.
Such formulas are interpreted over infinite sequences
$\gamma_{0}\gamma_{1}\ldots$ of sets of colors. We put
$\gamma_{0}\gamma_{1}\ldots\models\mathsf{Inf}\leavevmode\nobreak\ c$ if and
only if there are infinitely many positions $i$ such that $c\in\gamma_{i}$,
and $\gamma_{0}\gamma_{1}\ldots\models\mathsf{Fin}\leavevmode\nobreak\ c$ if
there are only finitely many such positions; satisfaction of Boolean operators
is defined in the usual way. Then an infinite play $\pi$ on $A$ _satisfies_
the formula $\varphi_{C}$ if and only if $\gamma_{C}(\pi)\models\varphi_{C}$
and we define the Emerson-Lei objective induced by $\gamma_{C}$ and
$\varphi_{C}$ by putting

$\displaystyle\alpha_{\gamma_{C},\varphi_{C}}=\\{\pi\in
A^{\omega}\mid\gamma_{C}(\pi)\models\varphi_{C}\\}.$

_Parity objectives_ are a special case of Emerson-Lei objectives with set
$C=\\{p_{0},\ldots,p_{k}\\}$ of colors, where each edge has exactly one color
(also called _priority_), and where $\varphi=\bigvee_{i\text{
even}}\mathsf{Inf}\leavevmode\nobreak\ p_{i}\wedge\bigwedge_{i<j\leq
k}\mathsf{Fin}\leavevmode\nobreak\ p_{j}$, stating that the maximal priority
that is visited infinitely often has an even index. We can denote such
objectives by just a single function $\Omega:E\to[k]$. Further standardly used
conditions include _Büchi_ , _generalized Büchi_ , _generalized reactivity
(GR[1])_ , _Rabin_ and _Streett_ objectives, all of which are special cases of
Emerson-Lei objectives (see e.g. [HausmannLP24]); the memory required for
winning in such games has been investigated in [DziembowskiJW97].

We note that neither Borel nor Emerson-Lei objectives enable a simple
distinction between finite plays ending in existential and universal nodes;
hence we will avoid deadlocks in our game reductions, ensuring that all games
in this work allow only infinite plays.

A _standard game_ is a tuple $(A,\alpha)$, where $A=(V,V_{\exists},E)$ is an
arena and $\alpha$ is an objective. A strategy $\sigma$ is _winning_ for
player $\exists$ at some node $v\in V$ if all plays that start at $v$ and are
compatible with $\sigma$ satisfy the objective $\alpha$. A strategy $\tau$ for
player $\forall$ is defined winning dually.

An _obliging game_ is a tuple $(A,\alpha_{S},\alpha_{W})$, consisting of an
arena $A=(V,V_{\exists},E)$ together with two objectives $\alpha_{S}$ and
$\alpha_{W}$, called the _strong_ and _weak_ objective, respectively; we also
refer to such games as $\alpha_{S}$ / $\alpha_{W}$ obliging games. A strategy
$\sigma$ for player $\exists$ is _graciously winning_ for $v\in V$ if all
plays that start at $v$ and are compatible with $\sigma$ satisfy the strong
objective $\varphi_{S}$ and furthermore every finite prefix $\pi\in A^{*}$ of
a play that is compatible with $\sigma$ can be extended to an infinite play
$\pi\tau$ that is compatible with $\sigma$ and satisfies the weak objective
$\alpha_{W}$. We sometimes refer to the infinite plays $\pi\tau$ witnessing
the satisfaction of the weak objective as _obliging_ plays. It follows
immediately that player $\exists$ can only win graciously at nodes at which at
least one obliging play (satisfying $\alpha_{S}\wedge\alpha_{W}$) starts, so
we assume without loss of generality that this is the case for all nodes in
$V$.

######  Example 2.1.

We consider the Emerson-Lei obliging game depicted below with the set
$\\{a,b,c,d\\}$ of colors, a Streett condition (with two pairs $(a,b)$ and
$(c,d)$) as strong objective $\alpha_{S}$, and generalized Büchi condition
enforcing visiting both $a$ and $c$ as weak objective $\alpha_{W}$. In all
examples in this work, nodes belonging to player $\exists$ are depicted with
rounded corners, while $\forall$-nodes are depicted by rectangles; edges may
have several colors in Emerson-Lei games, but in this example, each edge has
at most one color. We use the dashed edge to illustrate both winning and
losing in an obliging game.

$v_{1}$$v_{2}$$v_{3}$$v_{5}$$v_{4}$$a$$c$$b$$d$

$\alpha_{S}=(\mathsf{Inf}\leavevmode\nobreak\
a\to\mathsf{Inf}\leavevmode\nobreak\ b)\wedge(\mathsf{Inf}\leavevmode\nobreak\
c\to\mathsf{Inf}\leavevmode\nobreak\ d)$

$\alpha_{W}=\mathsf{Inf}\leavevmode\nobreak\
a\wedge\mathsf{Inf}\leavevmode\nobreak\ c$

Consider the strategy $\sigma$ with which player $\exists$ alternatingly moves
to $v_{5}$ and to $v_{1}$ when node $v_{4}$ is reached, depending on where
they moved from $v_{4}$ the last time it has been visited. Without the dashed
edge, $\sigma$ is graciously winning: every play compatible with $\sigma$
visits the colors $a,b$ and $d$ infinitely often and hence satisfies
$\alpha_{S}$; also, $\sigma$ allows player $\forall$ to visit color $c$
arbitrarily often by moving from $v_{2}$ to $v_{3}$, so every finite prefix of
a $\sigma$-play can be continued to an obliging $\sigma$-play that infinitely
often visits $v_{3}$ and therefore satisfies $\alpha_{S}\wedge\alpha_{W}$. If
the dashed edge is added to the arena, then $\sigma$ is no longer graciously
winning. Indeed, when playing against $\sigma$, player $\forall$ can prevent
$b$ from ever being visited by always moving from $v_{5}$ to $v_{4}$. However,
the modified strategy $\sigma^{\prime}$ that moves from $v_{4}$ to $v_{1}$
only if the last visited node is _not_ $v_{5}$ and also $b$ has been visited
more recently than $d$ (and otherwise moves back to $v_{5}$) is graciously
winning. Every $\sigma^{\prime}$-play that ends in $(v_{4}v_{5})^{\omega}$
satisfies $\alpha_{S}$ but also can be made into an obliging play by having
$\forall$ move to $v_{1}$ whenever $v_{5}$ is reached.

_Emerson-Lei automata._ Given an Emerson-Lei objective
$\alpha_{\gamma_{C},\varphi_{C}}$, an _Emerson-Lei automaton_ is a tuple
$A=(\Sigma,Q,\delta,q_{0},\alpha_{\gamma_{C},\varphi_{C}})$, where $\Sigma$ is
the alphabet, $Q$ is a set of _states_ , $\delta\subseteq Q\times\Sigma\times
Q$ is the transition relation, and $q_{0}\in Q$ is the initial state; in this
context, we assume that $\gamma_{C}:\delta\to 2^{C}$ assigns sets of colors to
transitions in $A$. A _run_ of $A$ on some infinite word
$w=a_{0}a_{1}\ldots\in\Sigma^{\omega}$ is a sequence $\pi=q_{0}q_{1}\ldots\in
Q^{\omega}$ such that $(q_{i},a_{i},q_{i+1})\in\delta$ for all $i\geq 0$. A
run $\pi$ is _accepting_ if and only if $\gamma_{C}(\pi)\models\varphi_{C}$,
and $A$ _recognizes_ the language

$\displaystyle L(A)=\\{w\in\Sigma^{\omega}\mid\text{there is an accepting run
of $A$ on $w$}\\}.$

An Emerson-Lei automaton $A$ is _non-empty_ if and only if
$L(A)\neq\emptyset$. All automata that we consider in this work will have a
single-letter alphabet $\Sigma=\\{*\\}$ so that they can read just the single
infinite word $*^{\omega}$.

##  3 Determinacy of Obliging Games

Chatterjee et al. [ChatterjeeHL10], when formalizing obliging games, stated
that the standard shape of strategies (that is, $A^{*}\cdot V_{i}\to V$) does
not allow player $\forall$ to counteract player $\exists$’s strategy with a
single strategy. We show that, for a more general form of strategy (of type
$A^{\omega}\to V\cup A^{\omega}$), this is possible. Furthermore, with these
more general strategies, the games are determined. That is, players are not
disadvantaged by revealing their strategy first and one of the players always
has a winning strategy. This insight allows offering alternative (more
efficient) solutions to obliging games in the next sections.

Fix an obliging game $G=(A,\alpha_{S},\alpha_{W})$. Let $A=(V,V_{\exists},E)$
and let $\alpha_{S}$ and $\alpha_{W}$ be Borel sets. A _witness_ for vertex
$v\in V$ is an infinite play $\pi=v_{0}v_{1}\cdots\in A^{\omega}$ such that
$v_{0}=v$; we write $\mathsf{witness}(v)$ to denote the set of witnesses for
$v\in V$. The _witness game_ $W(G)=(A^{\prime},\alpha^{\prime})$ captures the
obliging game by allowing player $\exists$ to choose an explicit witness for a
given vertex. Player $\forall$ can then either check whether the witness
satisfies both $\alpha_{S}$ and $\alpha_{W}$, or stop at some point verifying
the witness and ask for a new witness. If player $\forall$ changes witnesses
infinitely often, they still check that the resulting play satisfies
$\alpha_{S}$.

Formally, we have $A^{\prime}=(V^{\prime},V^{\prime}_{\exists},E^{\prime})$,
where $V^{\prime}=V\cup A^{\omega}$, $V^{\prime}_{\exists}=V$ and $E^{\prime}$
is as follows.

$\begin{array}[]{l c l l}E^{\prime}&=&\\{(v,\pi)\mid v\in
V,\pi\in\mathsf{witness}(v)\\}\qquad\cup\qquad\\{(v\pi,\pi)\mid v\pi\in
A^{\omega}\\}&\cup\\\ &&\\{(v\pi,v^{\prime\prime})\leavevmode\nobreak\
|\leavevmode\nobreak\ v\pi\in A^{\omega},v\in V_{\forall},v^{\prime\prime}\in
E(v)\\}.\end{array}$

Given $v\pi\in V^{\prime}_{\forall}$ put $\mathsf{head}(v\pi)=v$. We extend
$\mathsf{head}$ to sequences over $V^{\prime}$ in the natural way. Consider a
play $\pi^{\prime}\in(A^{\prime})^{\omega}$. Let
$\pi^{\prime}\Downarrow_{V^{\prime}_{\forall}}$ denote the projection of
$\pi^{\prime}$ to the elements of $V^{\prime}_{\forall}$, that is,
$\pi^{\prime}\Downarrow_{V^{\prime}_{\forall}}$ is obtained from
$\pi^{\prime}$ by removing all elements in $V^{\prime}_{\exists}=V$. Then put
$\mathsf{seq}_{A}(\pi^{\prime})=\mathsf{head}(\pi^{\prime}\Downarrow_{V^{\prime}_{\forall}})$.
Clearly, $\mathsf{seq}_{A}(\pi^{\prime})\in A^{\omega}$, that is,
$\mathsf{seq}_{A}(\pi^{\prime})$ extracts from $\pi^{\prime}$ the infinite
play in $A$ that is followed in $\pi^{\prime}$. The winning condition
$\alpha^{\prime}$ consists of plays $\pi^{\prime}$ that remain eventually in
$V^{\prime}_{\forall}$ forever such that $\mathsf{seq}(\pi^{\prime})$
satisfies both $\alpha_{S}$ and $\alpha_{W}$, or plays $\pi^{\prime}$ that
visit $V^{\prime}_{\exists}$ infinitely often such that
$\mathsf{seq}(\pi^{\prime})$ satisfies $\alpha_{S}$. Formally, we have the
following:

$\begin{array}[]{l c l l}\alpha^{\prime}&=&\\{\pi^{\prime}\in
V^{\prime*}\cdot(V^{\prime}_{\forall})^{\omega}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathsf{seq}_{A}(\pi^{\prime})\in\alpha_{S}\cap\alpha_{W}\\}&\cup\\\
&&\\{\pi^{\prime}\in
V^{\prime*}\cdot(V^{\prime}_{\exists}\cdot(V^{\prime}_{\forall})^{*})^{\omega}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathsf{seq}_{A}(\pi^{\prime})\in\alpha_{S}\\}\end{array}$

######  Example 3.1.

For brevity, we refrain from showing the complete witness game associated to
the obliging game from Example 2.1 and instead consider just two witnesses for
the node $v_{1}$, namely $(v_{1}v_{2}v_{4}v_{5})^{\omega}$ and
$(v_{1}v_{2}v_{3}v_{4}v_{1}v_{2}v_{4}v_{5})^{\omega}$. The former satisfies
the Streett objective $\alpha_{S}$ as it visits the colors $a$ and $b$.
However, it does not satisfy the generalized Büchi objective $\alpha_{W}$ as
color $c$ is not visited infinitely often. The latter witness, contrarily,
visits all colors infinitely often and hence satisfies
$\alpha_{S}\wedge\alpha_{W}$. In the witness game, player $\exists$ can move
from $v_{1}$ to these two witnesses (and to many more). Player $\forall$ in
turn can win the first witness by exploring it indefinitely, thereby showing
that it does not satisfy $\alpha_{W}$; doing the same for the second witness,
player $\forall$ loses. In both certificates, we have exit moves from every
position such that the node at the position is owned by player $\forall$, that
is, moves from positions with node $v_{2}$ to $E(v_{2})$, and similarly for
$v_{3}$ and $v_{5}$.

######  Lemma 3.2.

Player $\exists$ is graciously winning in $G$ at $v$ iff player $\exists$ is
winning in $W(G)$ at $v$.

######  Corollary 3.3.

Obliging games are determined.

######  Proof 3.4.

This follows immediately from Lemma 3.2 and the determinacy of games with
Borel winning conditions [Martin75]. Notice that Martin’s determinacy result
holds also for games with continuous vertex-spaces and continuous branching
degrees, as in the witness game.

##  4 Reducing $\omega$-Regular Obliging Games to Finite Games

From this point on, we restrict our attention to obliging games in which both
objectives are Emerson-Lei objectives; we note that every $\omega$-regular
objective can be transformed to an Emerson-Lei objective. It turns out that
due to the $\omega$-regularity of Emerson-Lei objectives, obliging plays in
such games have finite witnesses that take on the form of lassos that are
built over the game arena at hand. Formally, we show that for every such game
we can create a game that is smaller than the witness game by restricting
attention to witnesses of this specific form that satisfy the acceptance
conditions. We call such witnesses _certificates_ , which we define next.

###  4.1 Certificates from Witnesses

We fix an Emerson-Lei obliging game $G=(A,\alpha_{S},\alpha_{W})$ with arena
$A=(V,V_{\exists},E)$, objectives $\alpha_{S}=(\gamma_{S},\varphi_{S})$ and
$\alpha_{W}=(\gamma_{W},\varphi_{W})$, and put $n:=|V|$, $d:=|S|$ and
$k:=|W|$.

######  Definition 4.1 (Certificate).

Given a node $v\in V$, a _certificate_ for $v$ (in $G$) is a witness for $v$
that is of the form $c=wu^{\omega}$; if $c$ satisfies
$\varphi_{S}\land\varphi_{W}$, then we say that $c$ is a _valid certificate_.

We equally represent $c=wu^{\omega}$ by the pair $c=(w,u)$. Let
$w=w_{0}w_{1}\ldots w_{m}$ and $u=u_{0}u_{1}\ldots u_{r}$. We refer to $w$ as
the _stem_ and to $u$ as the _loop_ of $c$, and to $m$ and $r$ as the length
of the stem and the loop, respectively. When the partition of $c$ is not
important we sometimes just write $c=v_{0}\ldots v_{m+r+1}$. Clearly, as
satisfaction of Emerson-Lei objectives depends only on the infinite suffixes
of a play, it follows that in a valid certificate, $u^{\omega}$ also satisfies
$\varphi_{S}$ and $\varphi_{W}$.

Given a coloring function $\gamma_{C}$ over some set $C$ of colors, the
$C$-_fingerprint_ of a finite play $\pi=v_{0}v_{1}\ldots v_{j}\in A^{*}$ is
the set $\textstyle\bigcup_{0\leq i<j}\gamma_{C}(v_{i},v_{i+1})$ of colors
visited by $\pi$, according to $\gamma_{C}$.

Next we show that given a witness in $G$ that satisfies
$\alpha_{S}\land\alpha_{W}$, we can alway construct a valid certificate of
size at most $\mathsf{certLen}:=n\cdot
d+(d+k+1)\cdot(n+1)\in\mathcal{O}(n\cdot(\max(d,k)))$.

######  Lemma 4.2 (Certificate existence).

Let $v\in V$ and let $\pi=\pi_{0}\pi_{1}\ldots$ be a witness for $\pi_{0}=v$
that satisfies $\varphi_{S}\land\varphi_{W}$. Then there is a valid
certificate $c=(w,u)$ for $v$ with stem length at most $n\cdot d$ and loop
length at most $(d+k+1)\cdot(n+1)$, such that for all positions $i$ in $c$
there is a position $j$ in $\pi$ such that $v_{i}=\pi_{j}$ and the
$S$-fingerprints of $v_{0}\ldots v_{i}$ and $\pi_{0}\ldots\pi_{j}$ coincide.

We let $\mathsf{Cert}(v)$ and $\mathsf{Cert}$ denote the sets of all valid
certificates for some $v\in V$ in $G$ and all valid certificates for all $v\in
V$ in $G$, respectively, subject to the size bounds obtained in Lemma 4.2.
Then we have $|\mathsf{Cert}(v)|\leq|\mathsf{Cert}|\leq
n^{\mathsf{certLen}}\in 2^{\mathcal{O}(n\cdot(\max(d,k))\cdot\log n)}$.

###  4.2 Certificate Games and Smaller Winning Strategies

Next we adapt the witness games from Section 3 to use finite certificates in
place of witnesses, which leads to _certificate games_ that have finite game
arenas. In a certificate game, player $\exists$ has to pick a single valid
certificate at each node $v\in V$, thereby commiting to a long-term future
behavior that satisfies $\alpha_{S}\land\alpha_{W}$. Player $\forall$ in turn
can either accept the certificate (and thereby lose the play), or pick some
position $i$ in the certificate and challenge whether player $\exists$ still
has a strategy to graciously win when player $\forall$ exits the certificate
at position $i$. All plays then either end with player $\forall$ eventually
losing by accepting some certificate, or player $\forall$ infinitely often
exits certificates, in which case the winner of the play is determined using
just the strong objective $\alpha_{S}$.

Formally, the certificate game associated to $G$ is a (non-obliging) Emerson-
Lei game $C(G)=(B,\beta)$ with arena $B=(N,N_{\exists},R)$. The game is played
over the sets $N_{\exists}=V$ and
$N_{\forall}=\mathsf{Cert}\cup\mathsf{Cert}\times[\mathsf{certLen}]\times V$
of nodes. The moves in $C(G)$ are defined by

$\displaystyle R(v)$ $\displaystyle=\mathsf{Cert}(v)$ $\displaystyle R(c)$
$\displaystyle=\\{(c,i,v)\in N_{\forall}\mid v_{i}\in V_{\forall},v\in
E(v_{i})\\}\cup\\{c\\}$ $\displaystyle R(c,i,v)$ $\displaystyle=\\{v\\}$

for $v\in V$, $c=v_{0}v_{1}\ldots v_{m}\in\mathsf{Cert}$ and
$i\in[\mathsf{certLen}]$. Thus player $\exists$ has to provide a valid
certificate for $v$ whenever a play reaches a node $v\in V$. Player $\forall$
in turn can challenge the way certificates are combined by exiting them from
universal nodes in their stem or loop, and continuing the game at the exit
node; if a certificate $c$ does not contain a universal node, then player
$\forall$ has to take the loop at $c$, intuitively accepting the certificate
$c$. Intermediate nodes $(c,i,v)$ are used to make explicit the
$S$-fingerprint of the path through a certificate $c$ that is taken before
exiting it by moving from $v_{i}$ to $v$; this is necessary since a
certificate may contain universal nodes that allow moving from different
positions in the certificate to a single exit node $v$, potentially giving
player $\forall$ a choice on the path that is taken (and on the
$S$-fingerprint that is accumulated) through the certificate before exiting to
$v$.

As our notion of games does not support deadlocks, we annotate trivial loops
with an additional color $c_{\top}$ to encode the situation that player
$\forall$ accepts a certificate and thereby loses. The coloring function
$\gamma^{\prime}:R\to 2^{S\cup\\{c_{\top}\\}}$ also keeps track of the
$S$-fingerprints when passing through certificates and is defined by
$\gamma^{\prime}(c,(c,i,v))=\gamma_{S}(v_{0}\ldots v_{i}v)$,
$\gamma^{\prime}(v,c)=\emptyset$ and $\gamma^{\prime}((c,i,v),v)=\emptyset$
for the non-looping moves and by $\gamma^{\prime}(c,c)=c_{\top}$ for looping
moves at certificates $c\in\mathsf{Cert}$. We then define
$\varphi^{\prime}=\mathsf{Inf}(c_{\top})\vee\varphi_{S}$, intuitively
expressing that player $\exists$ can win either according to $\varphi_{S}$ or
by forcing player $\forall$ to get stuck in a trivial loop. Then we define
$\beta$ to be the objective induced by $\varphi^{\prime}$ and
$\gamma^{\prime}$.

######  Example 4.3.

Below we depict the construction for a single node $v\in V$, showing, as
examples, just two valid certificates
$c_{1}=v_{0}v_{1}v_{2}\in\mathsf{Cert}(v)$ and
$c_{2}=w_{0}w_{1}w_{2}w_{3}\in\mathsf{Cert}(v)$ (in particular, we assume
$v_{0}=w_{0}=v$ and that the certificates $c_{1}$ and $c_{2}$ satisfy both
$\varphi_{S}$ and $\varphi_{W}$). We further assume that $v_{2}\in
V_{\forall}$, $E(v_{2})=\\{v_{1},x\\}$, and that $w_{1}=w_{3}\in V_{\forall}$
and $E(w_{1})=E(w_{3})=\\{w_{2}\\}$; all other nodes in $c_{1}$ and $c_{2}$
are assumed to be contained in $V_{\exists}$.

$v$$\ldots$$c_{1}$$c_{2}$$c_{1},2,x$$c_{1},2,v_{1}$$v_{1}$$x$$c_{2},1,w_{2}$$c_{2},3,w_{2}$$w_{2}$$c_{\top}$$c_{\top}$$\gamma_{S}(v_{0}v_{1}v_{2}v_{1})\,\,\,$$\gamma_{S}(v_{0}v_{1}v_{2}x)$$\gamma_{S}(w_{0}w_{1}w_{2})$$\,\,\,\,\,\gamma_{S}(w_{0}w_{1}w_{2}w_{3}w_{2})$

At node $v$, player $\exists$ has to provide some valid certificate for $v$;
assuming that player $\exists$ picks the certificate $c_{1}=v_{0}v_{1}v_{2}$,
player $\forall$ in turn can exit the certificate at position $2$ (as
$v_{2}\in V_{\forall}$) by moving to either $(c_{1},2,v_{1})$ or $(c_{1},2,x)$
(as $E(v_{2})=\\{v_{1},x\\}$) thereby triggering $S$-fingerprint
$\gamma_{S}(v_{0}v_{1}v_{2}v_{1})$ or $\gamma_{S}(v_{0}v_{1}v_{2}x)$; player
$\forall$ intuitively cooperates during the play that leads from $v_{0}$ to
$v_{2}$, but may stop cooperating at node $v_{2}$ by moving to either $v_{1}$
or $x$. Similarly, player $\forall$ can exit the certificate $c_{2}$ at
positions $1$ or $3$, both leading to the node $w_{2}$, but with different
$S$-fingerprints, that is, with different sets of visited colors.

As the above example shows, certificate games have a three-stepped structure.
Plays progress from nodes $v$ of the original game on to certificate nodes
$c$, and then onwards to nodes $(c,i,v^{\prime})$ that encode the part of $c$
that is visited before exiting $c$, and then proceed back to some node
$v^{\prime}$ of the original game. We refer to these three-step subgames a
_gadgets_ ; each gadget has a starting node $v$ and a (possibly empty) set of
exiting nodes. We point out that, crucially, gadgets do not contain (non-
trivial) loops.

We state the correctness of the reduction to certificate games as follows.

######  Theorem 4.4.

Let $G$ be an Emerson-Lei obliging game and let $v$ be a node in $G$, and
recall that $W(G)$ and $C(G)$ respectively are the witness game and the
certificate game associated with $G$. The following are equivalent:

  1. 1.

player $\exists$ graciously wins $v$ in $G$;

  2. 2.

player $\exists$ wins $v$ in $W(G)$;

  3. 3.

player $\exists$ wins $v$ in $C(G)$.

######  Proof 4.5.

The equivalence of the first two items is stated by Lemma 3.2 and the proof of
the implication from item two to item three is technical but straight-forward.
Therefore we show just the implication from item three to item one, which also
shows how to construct a graciously winning strategy in $G$ from a winning
strategy in $C(G)$. For this proof, we use _strategies with memory_ ,
introduced next. A strategy for player $i\in\\{\exists,\forall\\}$ _with
memory $M$_ is a tuple $\sigma=(M,m_{0},\mathsf{update}:M\times E\to
M,\mathsf{move}:V_{i}\times M\to V)$, where $M$ is some set of _memory values_
, $m_{0}\in M$ is the initial memory value, the _update function_
$\mathsf{update}$ assigns the outcome $\mathsf{update}(m,e)\in M$ of updating
the memory value $m\in M$ according to the effects of taking the move $e\in
E$, and the moving function $\mathsf{move}$ prescribes a single move
$(v,\mathsf{move}(v,m))\in E$ to every game node $v\in V_{i}$ that is owned by
player $i$, depending on the memory value $m$. We extend $\mathsf{update}$ to
finite plays $\pi$ by putting $\mathsf{update}(m,\pi)=m$ in the base case that
$\pi$ consists of a single node, and by putting
$\mathsf{update}(m,\pi)=\mathsf{update}(\mathsf{update}(m,\tau),(v,w))$ if
$\pi$ is of the shape $\tau vw$, that is, contains at least two nodes.

Let $\sigma=(M,m_{0},\mathsf{update},\mathsf{move})$ be a winning strategy
with memory $M$ for player $\exists$ in the game $C(G)$. We construct a
strategy
$\tau=(M^{\prime},(m_{0},v,1),\mathsf{update}^{\prime},\mathsf{move}^{\prime})$
with memory $M^{\prime}=V\times M\times\\{1,\ldots,2|S|+|W|\\}$ for player
$\exists$ in the game $G$ such that $\tau$ graciously wins $v$. To this end,
we note that $\sigma$ provides, for each node $w\in V$ and memory value $m\in
M$, a certificate $c(w,m):=\mathsf{move}(w_{\exists},m)\in\mathsf{Cert}(w)$
for $w$ in $G$.

The strategy $\tau$ uses memory values $(w,m,i)$, where $w$ and $m$ identify a
current certificate $c(w,m)$ and $i$ is a counter used for the construction of
this certificate. We define $\tau$ such that player $\exists$ starts by
building the certificate $c(v,m_{0})$ for $v$ and $m_{0}$. This process
continues as long as player $\forall$ obliges, that is, does not move outside
of this certificate. Assuming that player $\forall$ obliges, the memory
required to construct the certificate is bounded by $2|S|+W$, walking, in the
prescribed order, through the certificate. In the case that player $\forall$
eventually stops obliging and takes a move to some node $w$ that is not the
next node on the path prescribed by the certificate, the memory for the strong
objective is updated according to the play from $v$ to $w$, resulting in a new
memory value $m$, and the memory for certificate construction is reset. Then
the certificate construction starts again, this time for the certificate
$c(w,m)$ prescribed by $\sigma$ for the new starting values $w$ and $m$.

In more detail, every node from $V$ is visited at most $2|S|+|W|$ times within
a certificate $c(v,m)=(v_{0}v_{1}\ldots v_{n})$ before the end of the loop
$v_{n}$ is reached. To each position $i$ within $c(v,m)$, we associate the
number $\sharp i$ such that $v_{i}$ is the $\sharp i$-th occurence of the node
$v_{i}$ in $c(v,m)$; we note that for all $1\leq i\leq n$, we have
$1\leq\sharp i\leq 2|S|+|W|$. Conversely, given a node $w$ and a number $j$
between $1$ and $2|S|+|W|$, we let $\mathsf{pos}(w,j)$ denote the position of
the $j$-th occurence of $w$ in $c(v,m)$. In the case $w$ occurs less than $j$
times in $c(v,m)$, we leave $\mathsf{pos}(w,j)$ undefined; below we make sure
that this value is always defined when it is used.

Let $j$ be the starting position of the loop of $c(v,m)$. Given a position $i$
in $c(v,m)$, we abuse notation to let $i+1$ denote just $i+1$ if $i<n$, and to
denote $j$ if $i=n$; in this way, we encode taking single steps within a
certificate, wrapping back to the start of the certificate loop, once the end
of the loop is reached.

We define the strategy $\tau$ to always move to the next node in the current
certificate, using the memory value $i$ together with the current node $w$ to
find the current position in the certificate $c(v,m)$, that is, we put

$\displaystyle\mathsf{move}^{\prime}(w,(v,m,i))=v_{\mathsf{pos}(w,i)+1}$

for $w\in V_{\exists}$ and $(v,m,i)\in M^{\prime}$. The memory update in
$\tau$ incorporates the memory update function from $\sigma$, but additionally
also keeps track of the memory for certificate construction. For moves
$(w,w^{\prime})$ that stay within the current certificate (that is,
$w^{\prime}=v_{\mathsf{pos}(w,i)+1}$), this memory is updated according to
proceeding one step within the certificate; for moves that leave the current
certificate, the memory for certificate construction is reset while the memory
for $\sigma$ is updated according to the path taken through the certificate
before exiting it. Formally, we put

$\displaystyle\mathsf{update}^{\prime}((v,m,i),(w,w^{\prime}))=\begin{cases}(v,m,\sharp(\mathsf{pos}(w,i)+1))&\text{$w^{\prime}=v_{\mathsf{pos}(w,i)+1}$}\\\
(w^{\prime},\mathsf{update}(m,(v_{0}v_{1}\ldots
ww^{\prime})),1)&\text{$w^{\prime}\neq v_{\mathsf{pos}(w,i)+1}$}\end{cases}$

for $(v,m,i)\in M^{\prime}$ such that $c(v,m)=v_{0}v_{1}\ldots v_{n}$ and
$(w,w^{\prime})\in E$; notice that in plays that adhere to $\tau$, the latter
case can, by definition of $\mathsf{move}^{\prime}$, only happen for $w\in
V_{\forall}$.

To see that player $\exists$ graciously wins $v$ using the constructed
strategy $\tau$, let $\pi$ be a play that adheres to $\tau$. Then $\pi$ either
eventually stays within one certificate $c(w,m)$ forever, or $\pi$ induces an
infinite play $\rho$ of $C(G)$ that adheres to $\sigma$. In the latter case,
$\pi$ changes the certificate infinitely often, and the $S$-fingerprints of
$\pi$ and $\rho$ coincide by construction, showing that $\pi$ satisfies
$\varphi_{S}$; if $\pi$ eventually stays within one certificate $c(w,m)$
forever, we note that the loop of $c(w,m)$ satisfies $\varphi_{S}$ so that
$\pi$ satisfies $\varphi_{S}$ as well. Thus every play that adheres to $\tau$
satisfies the strong objective $\varphi_{S}$. Next, let $\pi_{f}$ be a finite
prefix of some play that adheres to $\tau$, and let $\pi_{f}$ end in some node
$w$. We have to show that there is an infinite play $\pi$ that adheres to
$\tau$, extends $\pi_{f}$ and satisfies $\varphi_{W}$. Let $m$ be the value of
the memory for the strong objective at the end of $\pi_{f}$. We consider the
play of $G$ in which player $\forall$ obliges from the end of $\pi_{f}$ on,
forever. By construction, this play is $\pi_{f}$ extended with the certificate
$c(w,m)$ which adheres to $\tau$ and satisfies $\varphi_{W}$.

The strategy construction given in the proof of Theorem 4.4 yields:

######  Corollary 4.6.

Given an obliging game with Emerson-Lei objectives $\alpha_{S}$ and
$\alpha_{W}$ and $n$ nodes that contains a node $v$ at which $\exists$ is
graciously winning, there is a graciously winning strategy for $v$ that uses
memory at most $n\cdot(2|S|+|W|)\cdot m$, where $m$ is the amount of memory
required by winning strategies for player $\exists$ in standard games with
objective $\alpha_{S}$.

######  Remark 4.7 (Canonical certificates).

With the proposed strategy extraction, certificate strategies memorize the
starting point of the certificate that player $\exists$ currently attempts to
construct, leading to an additional linear factor $n$ in strategy size. We
conjecture that winning strategies in certificate games can be transformed to
make them _reuse_ certificates (so that the choice of the certificate does not
depend on the starting point). Strategies with such canonical certificate
choices would allow for removing the additional factor $n$ in Corollary 4.6.

In particular, our result shows the existence of graciously winning strategies
with quadratic sized strategies for all obliging games that have a half-
positional strong objective (i.e. one for which standard games have positional
winning strategies for player $\exists$); this covers, e.g., obliging games in
which $\alpha_{S}$ is a parity or Rabin objective.

In the table below we compare the solution via certificate games to a previous
solution method [ChatterjeeHL10, MajumdarSchmuck23] reduces $\alpha_{S}$ /
$\alpha_{W}$ obliging games to standard games with an objective of type
$\alpha_{S}\land$ Büchi. In this approach, the weak objective is encoded by a
non-deterministic Büchi automaton and graciously winning strategies obtained
in this way incorporate the state space of the automaton. The encoding of
$\alpha_{W}$ by a Büchi automaton leads to linear blow-up if $\alpha_{W}$ is a
Rabin objective, but is exponential if $\alpha_{W}$ is a Streett or general
Emerson-Lei objective.

In contrast to this, the certificate games that we propose here always have
(essentially) just $\alpha_{S}$ as objective, and the dependence of strategy
size on the weak objective $\alpha_{W}$ is in all cases linear in $|W|$. In
comparison to [ChatterjeeHL10], our approach hence leads to significantly
smaller strategies for obliging games in which $\alpha_{W}$ is at least a
Streett objective. In the cases where $\alpha_{W}$ is a Rabin objective,
strategies obtained from certificate games are slightly larger than in
[ChatterjeeHL10]; we conjecture that this can be improved by sharing
certificates (cf. Remark 4.7).

type of $\alpha_{S}$ |  type of $\alpha_{W}$ |  objective red. [ChatterjeeHL10] |  strategy size [ChatterjeeHL10] | strategy size
---|---|---|---|---
parity($d$) |  Rabin($k$) | parity($d$)$\land$ Büchi | $d(4k+2)$ | $(2d+2k)n$
Streett($k$) | $2^{k+1}dk$ | $(2d+2k)n$
EL($k$) | $2^{k+1}dk$ | $(2d+k)n$
Rabin($d$) |  Rabin($k$) | Rabin($d$)$\land$ Büchi | $d(4k+2)$ | $(4d+2k)n$
Streett($k$) | $2^{k+1}dk$ | $(4d+2k)n$
EL($k$) | $2^{k+1}dk$ | $(4d+k)n$
Streett($d$) |  Rabin($k$) | Streett($d+1$) | $(d+1)!(4k+2)$ | $(4d+2k)d!n$
Streett($k$) | $(d+1)!2^{k+2}k$ | $(4d+2k)d!n$
EL($k$) | $(d+1)!2^{k+2}k$ | $(4d+k)d!n$
EL($d$) |  EL($k$) |  EL($d+1$) | $(d+1)!2^{k+2}k$ | $(2d+k)d!n$
Table 1: Comparison of upper bounds on strategy sizes for various types of
obliging games.

For instance, for obliging games with $\alpha_{S}=$ Rabin($d$) and
$\alpha_{W}=$ Streett($k$), the approach from [ChatterjeeHL10] uses
nondeterministic Büchi automata with $2^{k}k$ states to encode the weak
(Streett) objective. The reduction leads to a game with objective
Rabin$(d)\wedge$ Büchi; winning strategies in such games require $2d$
additional memory values for each automaton state (cf. [DziembowskiJW97]),
resulting in an overall memory requirement of $2^{k+1}dk$. In contrast, the
reduced certificate game in this case is a Rabin$(d)$ game, and the extracted
gracious strategies require memory only to identify the current certificate
and a position in it; the overall memory requirement for strategies obtained
through our approach thus is $(4d+2k)n$.

##  5 Solving Certificate Games Efficiently

In the previous section we have shown how obliging games with Emerson-Lei
objectives $\alpha_{S}$ and $\alpha_{W}$ can be reduced to certificate games.
This reduction not only yields games with a simpler objective (essentially
just $\alpha_{S}$) than in the previously known alternative reduction from
[ChatterjeeHL10], but it also shows that the memory required for graciously
winning strategies in obliging games always depends only linearly on $|W|$.
However, the proposed reduction to certificate games makes explicit all
possible certificates that exist in the original obliging game and therefore
incurs exponential blowup. In more detail, given an Emerson-Lei obliging game
$G$ with $n$ nodes and sets $S$ and $W$ of colors, the certificate game $C(G)$
from the previous section is of size
$2^{\mathcal{O}(n\cdot\max(|S|,|W|)\cdot\log n)}$ and uses $|S|$ many colors;
solving it naively does not improve upon previously known solution algorithms
for obliging games.

In this section, we show that the gadget constructions in certificate games
essentially encode non-emptiness checking for non-deterministic
$\omega$-automata; intuitively, a certificate for a game node is a witness for
the non-emptiness of an Emerson-Lei automaton with acceptance condition
$\alpha_{S}\wedge\alpha_{W}$ that lives over (parts of) the original game
arena. We show that it suffices to check for the existence of a single
suitable certificate, rather than exploring all possible certificates that
occur as explicit nodes in the reduced game.

As pointed out above, the gadget parts in a certificate game do not have non-
trivial cycles (that is, we can regard them as directed acyclic graphs, DAGs).
Consequently, it is possible to simplify the solution process of these
(potentially) exponential-sized parts of the game by instead using non-
emptiness checking for suitable $\omega$-automata. If for instance both
$\alpha_{S}$ and $\alpha_{W}$ are Streett conditions (so that
$\alpha_{S}\wedge\alpha_{W}$ again is a Streett condition), then the solution
of every gadget part in the game can be reduced to non-emptiness checking of
Streett automata. As non-emptiness checking for Streett automata can be done
in polynomial time, this trick in effect removes the exponential runtime
factor that originates from the large number of certificates when solving such
games (and in general, whenever non-emptiness of
$\alpha_{S}\wedge\alpha_{W}$-automata can be checked efficiently).

Our program is as follows: We first show how Emerson-Lei certificate games can
be reduced to parity games using a tailored later-appearence-record (LAR)
construction, incurring blow-up $|S|!$ in game size, but retaining the DAG
structure of gadget subgames. Importantly, this is required to retain the
dependence of non-DAG nodes on a small number of (post DAG) successors. Then
we show the relation between attractor computation in gadget subgames within
the obtained parity games and the non-emptiness problem for specific Emerson-
Lei automata. Finally, we apply a fixpoint acceleration method from
[Hausmann24] to show that during the solution of parity games, the solution of
DAG substructures can be replaced with a procedure that decides attraction to
(subsets of) the exit nodes of the DAG. Overall, we therefore show that the
winning regions of certificate games can be computed as nested fixpoints of a
function that checks certificate existence by nonemptiness checking suitable
Emerson-Lei automata.

###  5.1 Lazy parity transform.

We intend to transform $C(G)$ to an equivalent parity game, using a lazy
variant of the later-appearance-record (LAR) construction (cf. [GurevichH82,
HunterD05]). To this end, we fix a set $C$ of colors and introduce notation
for permutations over $C$. We let $\Pi(C)$ denote the set of permutations over
$C$, and for a permutation $\pi\in\Pi(C)$ and a position $1\leq i\leq|C|$, we
let $\pi(i)\in C$ denote the element at the $i$-th position of $\pi$. For
$D\subseteq C$ and $\pi\in\Pi(C)$, we let $\pi@D$ denote the permutation that
is obtained from $\pi$ by moving _the_ element of $D$ that occurs at the
right-most position in $\pi$ to the front of $\pi$; for instance, for
$C=\\{a,b,c,d\\}$ and $\pi=(a,d,c,b)\in\Pi(C)$, we have
$\pi@\\{a,d\\}=\pi@\\{d\\}=(d,a,c,b)$ and $(d,a,c,b)@\\{a,d\\}=\pi$.
Crucially, restricting the reordering to single colors, rather than sets of
colors, ensures that for each $\pi\in\Pi(C)$ and all $D\subseteq C$, there are
only $|C|$ many $\pi^{\prime}$ such that $\pi@D=\pi^{\prime}$. Given a
permutation $\pi\in\Pi(C)$ and an index $1\leq i\leq|C|$, we furthermore let
$\pi[i]$ denote the set of colors that occur in one of the first $i$ positions
in $\pi$.

Next we show how permutations over $C$ can be used to transform Emerson-Lei
games with set $C$ of colors to parity games; the reduction annotates nodes
from the original game with permutations that serve as a memory, encoding the
order in which colors have recently been visited. The transformation is lazy
as it just moves the most significant color that is visited by a set of colors
$C$ rather than the entire set.

######  Definition 5.1.

Let $G=(A,\alpha_{C})$ be an Emerson-Lei game with arena
$A=(V,V_{\exists},E)$, set $C$ of colors and objective $\alpha_{C}$ induced by
$\gamma_{C}$ and $\varphi_{C}$. We define the parity game

$\displaystyle
P(G)=(V\times\Pi(C),V_{\exists}\times\Pi(C),E^{\prime},\Omega:E^{\prime}\to\\{1,\ldots,2|C|+1\\})$

by putting $E^{\prime}(v,\pi)=\\{(w,\pi@\gamma_{C}(v,w))\mid(v,w)\in E\\}$ for
$(v,\pi)\in V\times\Pi(C)$, as well as $\Omega((v,\pi),(w,\pi^{\prime}))=2p$
if $\pi[p]\models\varphi_{C}$ and $\Omega((v,\pi),(w,\pi^{\prime}))=2p+1$ if
$\pi[p]\not\models\varphi_{C}$, for $((v,\pi),(w,\pi^{\prime}))\in
E^{\prime}$. In the definition of $\Omega((v,\pi),(w,\pi^{\prime}))$, we write
$p$ to denote the right-most position in $\pi$ that contains some color from
$\gamma_{C}(v,w)$. For a finite play
$\tau=(v_{0},\pi_{0})(v_{1},\pi_{1})\ldots(v_{n},\pi_{n})$ of $P(G)$, we let
$p(\tau)$ denote the right-most position in $\pi_{0}$ such that
$\pi_{0}(p(\tau))\in\gamma_{C}(v_{0}v_{1}\ldots v_{n})$. The game $P(G)$ has
$|V|\cdot|C|!$ nodes and $2|C|+1$ priorities.

######  Lemma 5.2.

For all $v\in V$ and $\pi\in\Pi(C)$, player $\exists$ wins from $v$ in $G$ iff
player $\exists$ wins from $(v,\pi)$ in $P(G)$.

Now we consider the parity game $P(C(G))$ that is obtained by applying the
above LAR construction to the certificate game $C(G)$ from Section 4. It is a
parity game with $2^{\mathcal{O}(n\cdot\max(|S|,|W|)\cdot\log n)}\cdot|S|!$
many nodes and $2|S|+1$ priorities. We recall that all nodes in $C(G)$ that
are of the shape $c$ or $(c,i,v)$ such that $c,(c,i,v)\in N_{\forall}$ are
inner nodes of gadget subgames that consist of three layers. Each such subgame
has exactly one entry node and at most $n$ exit nodes, all contained in
$N_{\exists}=V$. The LAR construction preserves this general structure as it
simply annotates game nodes with permutations of colors. Specifically, $P(G)$
has $|S|!\cdot n$ entry and exit nodes for all such subgames together.
Furthermore, for all entry nodes $(v,\pi)$ of a subgame in $P(G)$, we have
that every exit node (that can be reached from $(v,\pi)$ with excactly three
moves, not accounting for trivial loops) is of the shape $(w,\pi@i)$ where
$w\in V$ and $0\leq i\leq|C|$. While an entry node for an individual subgame
in $C(G)$ has at most $n$ exit nodes, each entry node for a subgame in
$P(C(G))$ has at most $n(|S|+1)$ exit nodes. Using the classical LAR would
result in a potentially exponential number of exit nodes. Indeed, for every
possible subset $C^{\prime}\subseteq C$ there could be a different exit node.

######  Example 5.3.

Below, we depict (part of) the parity game that is obtained from the
certificate game fom Example 4.3 by using the proposed LAR construction.

$v$$\pi$$\ldots$$c_{1}$$\pi$$c_{2}$$\pi$$c_{1},2,x$$\pi@j$$c_{1},2,v_{1}$$\pi@i$$v_{1}$$\pi@i$$x$$\pi@j$$c_{2},1,w_{2}$$\pi@q$$c_{2},3,w_{2}$$\pi@r$$w_{2}$$\pi@q$$w_{2}$$\pi@r$$0$$0$$2i\,\,\,$$2j+1$$2q+1$$\,\,\,\,\,2r$

Here $i=p(v_{0}v_{1}v_{2}v_{1})$, $j=p(v_{0}v_{1}v_{2}x)$,
$q=p(w_{0}w_{1}w_{2})$, $r=p(w_{0}w_{1}w_{2}w_{3}w_{2})$ and we assume that
the sets $\pi[i]$ and $\pi[r]$ satisfy $\varphi_{S}$ and that the sets
$\pi[j]$ and $\pi[q]$ do not satisfy $\varphi_{S}$, leading to the respective
even and odd priorities. In particular, we have $2q+1\neq 2r$ so that
$(w_{2},\pi@q)$ and $(w_{2},\pi@r)$ are two distinct exit nodes from the
certificate $c_{2}$. Intuitively they correspond to two different paths
through $c_{2}$ with different $S$-fingerprints; while in the Emerson-Lei game
$C(G)$, the different fingerprints are dealt with by signalling different sets
of colors, in the parity game $P(C(G))$, the two paths have different effects
on the later-appearence memory $\pi$ and thus lead to different outcome nodes.
The self-loops at nodes $c_{1}$ and $c_{2}$ correspond to player $\forall$
giving up, so we assign priority $0$ to these moves.

###  5.2 Solving parity games using DAG attraction

A standard way of solving parity games is by computing a nested fixpoint of a
function that encodes one-step attraction in the game; the domain of this
fixpoint computation then is the set of all game nodes. For parity games that
contain cycle-free parts (DAGs), this process can be improved by instead
computing a nested fixpoint of a function that encodes multi-step attraction
along the DAG parts of the game. The domain of the latter fixpoint computation
then does not contain the internal nodes of the DAG parts, which leads to
accelerated fixpoint stabilization. We formalize this idea as follows.

######  Definition 5.4 (DAGs in games).

Let $G=(A,\Omega)$ be a parity game with $A=(V,V_{\exists},E)$ and $k+1$
priorities $0,\ldots,k$. We refer to a set $W\subseteq V$ of nodes as a _DAG_
(directed acyclic graph) if it does not contain an $E$-cycle; then there is no
play of $G$ that eventually stays within $W$ forever. A DAG need not be
connected, that is, it may consist of several cycle-free subgames of $G$.
Given a DAG $W\subseteq V$, we write $V^{\prime}=V\setminus W$ and refer to
the set $V^{\prime}$ as _real_ nodes (with respect to $W$). A DAG is
_positional_ if for each existential node $w\in W\cap V_{\exists}$ in it,
there is exactly one real node $v\in V^{\prime}$ from which $w$ is reachable
without visiting other real nodes.

######  Definition 5.5 (DAG attraction).

Given a DAG $W$ and $k+1$ sets $\overline{V}=(V_{0},\ldots,V_{k})$ of real
nodes and a real node $v\in V^{\prime}$, we say that player $\exists$ can
_attract_ to $\overline{V}$ from $v$ within $W$ if they have a strategy
$\sigma$ such that for all plays $\pi$ that start at $v$ and adhere to
$\sigma$, the first real node $v^{\prime}$ in $\pi$ such that $v^{\prime}\neq
v$ is contained in $V_{p}$, where $p$ is the maximal priority that is visited
by the part of $\pi$ that leads from $v$ to $v^{\prime}$. Given a dag $W$, we
define the _dag attractor function_
$\mathsf{DAttr}^{W}_{\exists}:\mathcal{P}(V^{\prime})^{k}\to\mathcal{P}(V^{\prime})$
by $\mathsf{DAttr}^{W}_{\exists}(\overline{V})=\\{v\in
V^{\prime}\mid\text{player $\exists$ can attract to $\overline{V}$ from $v$
within $W$}\\}$ for
$\overline{V}=(V_{0},\ldots,V_{k})\in\mathcal{P}(V^{\prime})^{k}$. We denote
by $t_{\mathsf{Attr}^{W}_{\exists}}$ the time required to compute, for every
input $\overline{V}\in\mathcal{P}(V^{\prime})^{k}$, the dag attractor of
$\overline{V}$ through $W$.

######  Remark 5.6.

The sets $V_{i}$ in the above definition correspond to valuations of fixpoint
variables in the nested fixpoint computation that is used by the fixpoint
acceleration method in Lemma 5.7 below to solve games via DAG attraction.
These sets monotonically increase or decrease during the solution process and
at each point of the solution process, a set $V_{i}$ intuitively holds game
nodes for which it currently is assumed that player $\exists$ wins if they can
force the game to reach a node from $V_{i}$ via a partial play in which the
maximal priority is $i$.

During the computation of the DAG attractor to a tuple
$\overline{V}=(V_{0},\ldots,V_{k})$, we therefore intuitively consider the
argument nodes $\overline{V}$ to be _safe_ in the sense that in order to win
from a node $v$, is suffices that existential player has a strategy that
ensures that every partial play through the DAG exits it to a node from
$V_{i}$, where $i$ the maximal priority visited by that play along the DAG.
Thus if player $\exists$ can win from all nodes in $\overline{V}$, then they
can win from all nodes in $\mathsf{DAttr}^{W}_{\exists}(\overline{V})$.

In our case, from a node $v$, a strategy $\sigma$ corresponds to choosing one
certificate. Then, player $\forall$ can attract to all successors of
$\forall$-nodes on the certificate. The path through the certificate to this
$\forall$-node and to its successor outside the certificate shows a certain
priority $j$ that implies the successor must be in the set $V_{j}$.

######  Lemma 5.7 ([Hausmann24arxiv]).

Let $G$ be a parity game with priorities $0$ to $k$ and set $V$ of nodes, let
$W$ be a positional DAG in $G$, and let $n=|V|$ and $m=n-|W|$. Then $G$ can be
solved with $\mathcal{O}(m^{\log k+1})$ computations of a DAG attractor; if
$k+1<\log m$, then $G$ can be solved with a number of DAG attractor
computations that is polynomial in $m$ (specifically: in
$\mathcal{O}(m^{5})$).

We always have $t_{\mathsf{Attr}^{W}_{\exists}}\leq|E|$, using a least
fixpoint computation to check for alternating reachability, thereby possibly
exploring all DAG edges of the game. However, in the case that $m<\log n$ and
$t_{\mathsf{Attr}^{W}_{\exists}}\in\mathcal{O}(\log n)$ (that is, when most of
the game nodes are part of a DAG, and DAG attractability can be decided
without exploring most of the DAG nodes), Lemma 5.7 enables exponentially
faster game solving.

###  5.3 Checking certificate existence efficiently

The parity game $P(C(G))$ that is obtained by applying the LAR construction
from Subsection 5.1 to the certificate game $C(G)$ has
$2^{O(n\cdot\max(d,k)\cdot\log n))}\cdot|S|!$ nodes, but only $|S|!n$ of these
are real nodes: all certificate nodes are internal nodes in a gadget that has
a DAG structure. In this section, we show that DAG attractors in $P(C(G))$ can
be computed efficiently relying on non-emptiness checking of suitable Emerson-
Lei automata.

In $P(C(G))$, the DAG attractor to a tuple
$\overline{V}=(V_{1},\ldots,V_{2|C|+1})$ consists of the nodes $(v,\pi)$ such
that there is a valid certificate starting at $v$ such that all exits points
of the cerficate are safe in the sense of Remark 5.6, that is, exiting the
certificate with fingerprint $i$ is only possible to nodes $w\in V_{i}$; we
refer to such certificates as _valid and safe_.

Next we show how the existence of valid and safe certificates can efficiently
be checked by using non-emptiness checking for Emerson-Lei automata to find
valid and safe certificate loops that reside over single sets $V_{i}$ (as the
fingerprint does not increase within certificate loops, by the construction of
certificates as in the proof of Lemma 4.2), and then using a reachability
analysis that keeps track of fingerprints to compute safe stems leading (with
fingerprint $i$) to some loop over $V_{i}$. In more detail, we check for the
existence of valid and safe certificates as follows, fixing a permutation
$\pi$ and a tuple $(V_{1},\ldots,V_{2|C|+1})$, where each $V_{i}$ is a set of
real nodes in $P(C(G))$.

  * •

_Make the fingerprints explicit._ Define the graph $M=(V\times[{2|C|+1}],R)$
as follows. Vertices of the graph are pairs $(v,i)$ consisting of a game node
$v\in V$ and a priority $i\in[{2|C|+1}]$, intuitively encoding the largest
priority that has been visited since a DAG has been entered; edges in this
graph correspond to game moves but also update the priority value according to
visited priorities, that is, $R$ contains exactly the edges $((v,i),(w,j))$
such that $w\in E(v)$ and $j=\max(i,\Omega_{\pi}(v,w))$, where
$\Omega_{\pi}(v,w)$ denotes priority associated to seeing the set
$\gamma_{C}(v,w)$ of colors on memory $\pi$ (cf. Definition 5.1).

  * •

_Remove unsafe vertices._ A vertex $(u,i)$ such that $(u,\pi@i)$ is contained
neither in $V_{2i}$ nor in $V_{2i+1}$ is _unsafe_. Remove from $M$ all
vertices $(v,i)$ such that $v\in V_{\forall}$ and there is $w\in E(v)$ such
that $(w,i)$ is unsafe; these are vertices from where player $\forall$ can
access an unsafe exit point of the DAG.

  * •

_Find safe and valid certificate loops:_ Define, for all $i\in[2|C|+1]$, a
nondeterministic Emerson-Lei automaton
$A_{i}=(Q_{i},\delta,\alpha_{S}\land\alpha_{W})$ (with singleton alphabet
$\\{*\\}$) by putting $Q_{i}=\\{(v,i)\mid(v,i)\text{ still exists in }M\\}$
and $\delta((v,i),*)=\\{(w,i)\mid w\in E(v)\text{ and }\Omega_{\pi}(v,w)\leq
i\\}$ for $(v,i)\in Q_{i}$. Compute the non-emptiness region of $A_{i}$ and
call it $N_{i}$.

  * •

_Find safe stems:_ Remove from $M$ all vertices $(v,0)$ for which there is no
$j$ such that some vertex from $N_{j}$ is reachable (in $M$) from $(v,0)$.

For all vertices $(v,0)$ that are contained in $M$ after this procedure
terminates, there is a safe stem $w$ leading (with maximal priority $j$) to
some safe and valid loop $u$ over $N_{j}$; $(w,u)$ is a valid certificate for
$v$. We state the correctness of the described procedure as follows.

######  Lemma 5.8.

Given subsets $\overline{V}=V_{0},\ldots V_{2k}$ of the real nodes in
$P(C(G))$ and a real node $(v,\pi)$ in $P(C(G))$, we have that player
$\exists$ can attract to $\overline{V}$ from $(v,\pi)$ within
$\mathsf{Cert}\times\Pi(S)$ if and only if the set $M$ contains the pair
$(v,0)$ after execution the above procedure (for parameters $\overline{V}$ and
$(v,\pi)$).

######  Corollary 5.9.

DAG attractors in $P(C(G))$ can be computed in time $\mathcal{O}(d!dt)$ where
$t$ denotes the time it takes to check $\alpha_{S}\wedge\alpha_{W}$ automata
of size $n$ for non-emptiness.

######  Proof 5.10.

In order to compute a DAG attractor in $P(C(G))$, it suffices to execute the
above procedure once for each $\pi\in\Pi(S)$, that is, $d!$ many times; a
single execution of the procedure can be implemented in time
$\mathcal{O}(dt)$.

###  5.4 Faster solution of obliging games

We are now ready to state the main result of this section.

######  Theorem 5.11.

Certificate games for objectives $\alpha_{S}$ and $\alpha_{W}$ with $n$ nodes
and $d:=|S|$ colors for the strong objective can be solved in time
$\mathcal{O}((d!n)^{5}d!dt)$, where $t$ denotes the time it takes to check
Emerson-Lei automata of size $n$ and with acceptance condition
$\alpha_{S}\wedge\alpha_{W}$ for non-emptiness. If $\alpha_{S}$ is a parity
objective, then the runtime bound is $\mathcal{O}(n^{\log(2d+1)}dt)$.

######  Proof 5.12.

By Lemma 5.2, it suffices to solve the paritized version $P(C(G))$ of $C(G)$.
By Lemma 5.8, computing DAG attractors in $P(C(G))$ can be done in time
$\mathcal{O}(d!dt)$. As we have $d<\log(d!\cdot n)$, $P(C(G))$ can be solved
with $(d!n)^{5}$ computations of a DAG attractor by Lemma 5.7. If $\alpha_{S}$
is a parity objective, then the LAR construction is not necessary as $C(G)$
already is a parity game; DAG attractors then can be computed in time
$\mathcal{O}(dt)$ and $C(G)$ can be solved with $\mathcal{O}(n^{\log(2d+1)})$
computations of a DAG attractor.

We collect results on the complexity of non-emptiness checking of Emerson-Lei
automata with acceptance condition $\alpha_{S}\wedge\alpha_{W}$ for specific
$\alpha_{S}$ and $\alpha_{W}$. It is known (cf. Table 2. in [BaierBD00S19])
that while the problem is in P for most frequently used objectives (subsuming
automata with generalized Büchi, Rabin or Streett conditions, with linear or
quadratic dependence on the number of colors), it is NP-complete for Emerson-
Lei conditions. For combinations of such objectives, the problem remains in P
unless one of the objectives is of type Emerson-Lei:

######  Lemma 5.13.

The Rabin($d$)$\land$Streett($k$) non-emptiness problem is in P (more
precisely: in $\mathcal{O}(mdk^{2})$ for automata with $m$ edges).

######  Proof 5.14.

Let $A$ be an Emerson-Lei automaton with $n$ nodes, $m$ edges and acceptance
condition Streett$(d)\land$ Rabin($k$). We check $A$ for non-emptiness as
follows. Let the Rabin($k$) condition be encoded by $k$ Rabin pairs
$(E_{i},F_{i})$. For each $1\leq i\leq k$, check the same automaton but with
acceptance condition
Streett$(d)\land\mathsf{Inf}(F_{i})\land\mathsf{Fin}(E_{i})$ for emptiness;
call this automaton $A_{i}$. The acceptance condition of $A_{i}$ can be
treated as a Streett($d+2$) condition where the two additional Streett pairs
are $(\top,F_{i})$ and $(E_{i},\bot)$. As a state in $A$ is non-empty if and
only if there is some $i$ such the state is non-empty in $A_{i}$, it suffices
to check the $k$ many Streett($d+2$) automata for emptiness. The claim follows
from the bound on emptiness checking for Streett automata given in
[BaierBD00S19].

Using the equivalence of certificate games and obliging games (Theorem 4.4),
Theorem 5.11 together with the described complexities of emptiness checking
yields improved upper bounds on the runtime complexity of solving obliging
games, shown in the table below; we let $n$ denote the number of nodes; $m$
the number of edges; $b$ the size of a nondeterministic Büchi automaton
accepting $\alpha_{W}$; and $t$ the time required for emptiness checking an
Emerson-Lei automaton of size $n$ with acceptance condition
$\alpha_{S}\wedge\alpha_{W}$; finally we let $o$ abbreviate $\max(|W|,|S|)$.
Recall that the approach from [ChatterjeeHL10] reduces an obliging game to a
standard game in which the objective $\alpha^{\prime}$ is the conjunction of
$\alpha_{S}$ with a Büchi objective, incurring blowup $b$ on the arena size.
This game then can be transformed to a parity game $\mathcal{G}$ (with
parameters $v,e$ and $r$) incurring additional blowup for the LAR
transformation of $\alpha^{\prime}$ to a parity objective. Notice the
definition of $e$ (an underapproximation of the number of edges in
$\mathcal{G}$) in column 4 and its usage in column 5.

For instance for an obliging game with objectives $\alpha_{S}=$ Streett($d$)
and $\alpha_{W}=$generalized Büchi($d$) consisting of the Streett requests,
the approach from [ChatterjeeHL10] reduces the game to a parity game
$\mathcal{G}$ with $d!nd$ nodes, at least $d!md$ edges, and $2d$ priorities;
such a game can be solved in time $\mathcal{O}(d!md^{6}(d!n)^{5})$. In
contrast, emptiness checking for $\alpha_{S}\wedge\alpha_{W}$-automata is just
emptiness checking for generalized Büchi automata so that our new algorithm
solves such games in time $\mathcal{O}(d!md^{2}(d!n)^{5})$. For objectives
$\alpha_{S}=$ Rabin($d$) and $\alpha_{W}=$ Streett($k$), the approach from
[ChatterjeeHL10] has time complexity $\mathcal{O}(m(d!k2^{k})^{6}n^{5})$ while
our algorithm has time complexity just $\mathcal{O}(m(d!)^{6}n^{5}do^{3})$;
this is due to the fact that Büchi automata that recognize Streett objectives
are of exponential size (as they have to guess a set of Streett pairs and then
verify their satisfaction), while emptiness checking for Streett($d$)$\land$
Rabin($k$)-automata can be done in time cubic in $o$.

type of $\alpha_{S}$ |  type of $\alpha_{W}$ | $b$ |  $|\mathcal{G}|(v,e,r)$ [ChatterjeeHL10] |  time [ChatterjeeHL10] |  $t$ [BaierBD00S19] | time here
---|---|---|---|---|---|---
parity($d$) |  Rabin($k$) | $k+1$ | $dnb,dmb,d$ | $\mathcal{O}(e(dnb)^{\log d})$ | $\mathcal{O}(mo^{2})$ | $\mathcal{O}(n^{\log d+1}dt)$
Streett($k$) | $2^{k}k$ | $\mathcal{O}(mo^{2})$
EL($k$) | $2^{k}k$ | $\mathcal{O}(mo^{2}2^{o})$
Rabin($d$) |  Rabin($k$) | $k+1$ | $d!nb,d!mb,2d$ | $\mathcal{O}(e(d!nb)^{5})$ | $\mathcal{O}(mo^{3})$ | $\mathcal{O}((d!n)^{5}d!dt)$
or |  Streett($k$) | $2^{k}k$ | $\mathcal{O}(mo^{3})$
Streett($d$) |  EL($k$) | $2^{k}k$ | $\mathcal{O}(mo^{2}2^{o})$
EL($d$) |  EL($k$) | $2^{k}k$ | $d!nb,d!mb,2d$ | $\mathcal{O}(e(d!nb)^{5})$ | $\mathcal{O}(mo^{2}2^{o})$ | $\mathcal{O}((d!n)^{5}d!dt)$
Streett($d$) |  g.Büchi($d$) | $d$ | $d!nb,d!mb,2d$ | $\mathcal{O}(e(d!nb)^{5})$ | $\mathcal{O}(md)$ | $\mathcal{O}((d!n)^{5}d!dt)$
GR[1]($d,k$) |  g.Büchi($d$) | $d$ | $dknb,dkmb,3$ | $\mathcal{O}(e(dknb)^{2})$ | $\mathcal{O}(md)$ | $\mathcal{O}((dk)^{3}n^{2}dt)$
Table 2: Comparison of runtime complexities for solving obliging games of
various types.

##  6 Conclusion

We propose a new angle of looking at the solution of obliging games. In
contrast to previous approaches that have been based on single-step game
reasoning, our method requires players to make promises about their long-term
future behavior, which we formalize using the concept of certificates (or,
more generally, witnesses). This new approach to obliging games enables us to
not only show their determinacy (with strategies that contain additional
information), but to also significantly improve previously existing upper
bounds both on the size of graciously winning strategies, and on the worst-
case runtime complexity of the solution of such games.

Technically, we use our new approach to show that the strategy sizes for
Emerson-Lei obliging games with strong objective $\alpha_{S}$ and weak
objective $\alpha_{W}$ are linear in the number $|W|$ of colors used in the
weak objective; we obtain a similar polynomial dependence on $|W|$ for the
runtime of solving obliging games, however with the important exception of the
case where $\alpha_{W}$ is a full Emerson-Lei objective that cannot be
expressed by a simpler (e.g. Rabin or Streett) objective. In previous
approaches, those dependencies on $|W|$ have been, in general, exponential.
Thereby we show that the strategy complexity of $\alpha_{S}$ / $\alpha_{W}$
obliging games is not significantly higher than that of standard games with
objective just $\alpha_{S}$, and that in many cases, this holds for the
runtime complexity as well.

We leave the existence of canonical certificates (cf. Remark 4.7) as an open
question for future work; such canonical certificates would allow for the
extraction of yet smaller graciously winning strategies for obliging games.

We solve certificate games by using the LAR reduction to obtain equivalent
parity games and then solving these parity games by fixpoint acceleration,
computing nested fixpoints of a function that checks for certificate
existence. We conjecture that it is possible to directly compute the more
involved nested fixpoint associated to Emerson-Lei objectives (as given in
[HausmannLP24]) over the original game arena; this would avoid the LAR
reduction step in the solution process.

## References

  * [1] Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002.  doi:10.1007/3-540-36387-4.
  * [2] Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejcek.  Generic emptiness check for fun and profit.  In Automated Technology for Verification and Analysis, ATVA 2019, volume 11781 of LNCS, pages 445–461. Springer, 2019.  doi:10.1007/978-3-030-31784-3\\_26.
  * [3] Roderick Bloem, Rüdiger Ehlers, Swen Jacobs, and Robert Könighofer.  How to handle assumptions in synthesis.  In Workshop on Synthesis, SYNT 2014, volume 157 of EPTCS, pages 34–50, 2014.  doi:10.4204/EPTCS.157.7.
  * [4] Roderick Bloem, Rüdiger Ehlers, and Robert Könighofer.  Cooperative reactive synthesis.  In Automated Technology for Verification and Analysis, ATVA 2015, volume 9364 of Lecture Notes in Computer Science, pages 394–410. Springer, 2015.  doi:10.1007/978-3-319-24953-7\\_29.
  * [5] Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa’ar.  Synthesis of reactive(1) designs.  J. Comput. Syst. Sci., 78(3):911–938, 2012.  doi:10.1016/J.JCSS.2011.08.007.
  * [6] Julian C. Bradfield and Igor Walukiewicz.  The $\mu$-calculus and model checking.  In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871–919. Springer, 2018\.  doi:10.1007/978-3-319-10575-8\\_26.
  * [7] Krishnendu Chatterjee, Florian Horn, and Christof Löding.  Obliging games.  In Concurrency Theory, 21th International Conference, CONCUR 2010, volume 6269 of LNCS, pages 284–296. Springer, 2010.  doi:10.1007/978-3-642-15375-4\\_20.
  * [8] Stefan Dziembowski, Marcin Jurdzinski, and Igor Walukiewicz.  How much memory is needed to win infinite games?  In Logic in Computer Science, LICS 1997, pages 99–110. IEEE Computer Society, 1997.  doi:10.1109/LICS.1997.614939.
  * [9] Javier Esparza, Jan Kretínský, Jean-François Raskin, and Salomon Sickert.  From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata.  Int. J. Softw. Tools Technol. Transf., 24(4):635–659, 2022.  doi:10.1007/S10009-022-00663-1.
  * [10] Oliver Friedmann and Martin Lange.  Deciding the unguarded modal $\mathrm{\mu}$-calculus.  J. Appl. Non Class. Logics, 23(4):353–371, 2013.  doi:10.1080/11663081.2013.861181.
  * [11] Oliver Friedmann, Markus Latte, and Martin Lange.  Satisfiability games for branching-time logics.  Log. Methods Comput. Sci., 9(4), 2013.  doi:10.2168/LMCS-9(4:5)2013.
  * [12] Yuri Gurevich and Leo Harrington.  Trees, automata, and games.  In Symposium on Theory of Computing, STOC 1982, pages 60–65. ACM, 1982.  doi:10.1145/800070.802177.
  * [13] Daniel Hausmann.  Faster game solving by fixpoint acceleration.  CoRR, abs/2404.13687, 2024.  URL: https://arxiv.org/abs/2404.13687, arXiv:2404.13687.
  * [14] Daniel Hausmann.  Faster game solving by fixpoint acceleration.  In Fixed Points in Computer Science, FICS 2024, EPTCS, 2024, to appear.
  * [15] Daniel Hausmann, Mathieu Lehaut, and Nir Piterman.  Symbolic solution of Emerson-Lei games for reactive synthesis.  In Foundations of Software Science and Computation Structures, FoSSaCS 2024, volume 14574 of LNCS, pages 55–78. Springer, 2024.  doi:10.1007/978-3-031-57228-9\\_4.
  * [16] Daniel Hausmann and Lutz Schröder.  Game-based local model checking for the coalgebraic $\mu$-calculus.  In Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 35:1–35:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPICS.CONCUR.2019.35.
  * [17] Paul Hunter and Anuj Dawar.  Complexity bounds for regular games.  In Mathematical Foundations of Computer Science, MFCS 2005, volume 3618 of Lecture Notes in Computer Science, pages 495–506. Springer, 2005.  doi:10.1007/11549345\\_43.
  * [18] Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert.  Practical synthesis of reactive systems from LTL specifications via parity games.  Acta Informatica, 57(1-2):3–36, 2020.  doi:10.1007/s00236-019-00349-3.
  * [19] Rupak Majumdar, Nir Piterman, and Anne-Kathrin Schmuck.  Environmentally-friendly GR(1) synthesis.  In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, volume 11428 of LNCS, pages 229–246. Springer, 2019\.  doi:10.1007/978-3-030-17465-1\\_13.
  * [20] Rupak Majumdar and Anne-Kathrin Schmuck.  Supervisory controller synthesis for nonterminating processes is an obliging game.  IEEE Trans. Autom. Control., 68(1):385–392, 2023.  doi:10.1109/TAC.2022.3143108.
  * [21] Donald A. Martin.  Borel determinacy.  Annals of Mathematics, 102(2):363–371, 1975.  doi:10.2307/1971035.
  * [22] Amir Pnueli and Roni Rosner.  On the synthesis of a reactive module.  In Principles of Programming Languages, POPL 1989, pages 179–190. ACM Press, 1989.  doi:10.1145/75277.75293.
  * [23] Tom van Dijk, Feije van Abbema, and Naum Tomov.  Knor: reactive synthesis using oink.  In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, volume 14570 of LNCS, pages 103–122. Springer, 2024\.  doi:10.1007/978-3-031-57246-3\\_7.

##  7 Appendix

Full proof of Lemma 3.2 (Correctness of witness games):

######  Proof 7.1.

  * $\Rightarrow$

Let $\sigma:V^{*}\cdot V_{\exists}\rightarrow V$ be a graciously winning
strategy for $v$. Consider the strategy tree $T\subseteq V^{+}$, where $v\in
T$ and for every $wv^{\prime}\in A^{+}$ we have that if $v^{\prime}\in
V_{\exists}$ then $wv^{\prime}\sigma(wv^{\prime})\in T$ and if
$v^{\prime}\notin V_{\exists}$ then $wv^{\prime}v^{\prime\prime}\in T$ for
every $(v^{\prime},v^{\prime\prime})\in E$. By definition of gracious
strategies, for every $w\in T$ there is a play $\pi(w)$ such that $w\pi(w)$ is
compatible with $\sigma$ and satisfies $\alpha_{W}$. Furthermore, every play
compatible with $\sigma$ (particularly, also $w\pi(w)$) satisfies
$\alpha_{S}$. We now define a strategy $\sigma^{\prime}$ for player $\exists$
in $W(G)$. Consider a finite play $\pi^{\prime}$ in $W(G)$ such that
$\pi^{\prime}$ ends in $v^{\prime}\in V^{\prime}_{\exists}$. Then,
$w=\mathsf{seq}_{A}(\pi^{\prime})$ is a finite play in $A$. We put
$\sigma^{\prime}(\pi^{\prime})=\pi(w)$. That is, $\sigma^{\prime}$ moves from
$v^{\prime}$ to the witness $\pi(w)$ appearing in $T$.

To see that $\sigma^{\prime}$ is a winning strategy, consider an infinite play
$\pi^{\prime}$ in $W(G)$ that starts at $v$ and is compatible with
$\sigma^{\prime}$.

    * –

If $\pi^{\prime}\in V^{\prime*}\cdot(V^{\prime}_{\forall})^{\omega}$, the let
$w$ be the longest prefix of $\pi^{\prime}$ ending in a vertex in
$V^{\prime}_{\exists}$ and let $v^{\prime}$ be the last vertex in $w$. It
follows that
$\mathsf{seq}_{A}(\pi^{\prime})=\mathsf{seq}_{A}(w)\cdot\sigma^{\prime}(\mathsf{seq}_{A}(w)v^{\prime})$.
By the choice of $\sigma^{\prime}(\mathsf{seq}_{A}(w)v^{\prime})$ we have that
$\mathsf{seq}_{A}(\pi^{\prime})$ satisfies $\alpha_{W}$. Furthermore, by
$\mathsf{seq}_{A}(\pi^{\prime})$ being a play compatible with $\sigma$ we
conclude that $\mathsf{seq}_{A}(\pi^{\prime})$ also satisfies $\alpha_{S}$.
Thus, $\pi^{\prime}\in\alpha^{\prime}$.

    * –

If $\pi^{\prime}\in
V^{\prime*}\cdot(V^{\prime}_{\exists}\cdot(V^{\prime}_{\forall})^{*})^{\omega}$,
then $\mathsf{seq}_{A}(\pi^{\prime})$ is a play compatible with $\sigma$. We
conclude that $\mathsf{seq}_{A}(\pi^{\prime})$ satisfies $\alpha_{S}$ and
hence $\pi^{\prime}\in\alpha^{\prime}$.

  * $\Leftarrow$

Let $\sigma^{\prime}$ be a winning strategy in $W(G)$ for $v$. We construct a
graciously winning strategy $\sigma$ in $G$ by using the witnesses. Alongside
$\sigma$ we keep track of all the histories ending also in $V_{\forall}$ which
have been handled. Thus, we build $\sigma$ and $T\subseteq A^{*}$
simultaneously such that $T$ is prefix closed. Consider the vertex $v$. By
definition, $\sigma^{\prime}(v)=\pi$ such that $\pi\in A^{\omega}$. For every
prefix $w^{\prime}$ of $\pi$, add $w^{\prime}$ to $T$. This clearly keeps $T$
prefix closed. Furthermore, consider a partition
$\pi=w^{\prime}v^{\prime}v^{\prime\prime}w^{\prime\prime}$ of $\pi$, where
$w^{\prime}\in A^{*}$, $v^{\prime}\in V_{\exists}$, $v^{\prime\prime}\in V$,
and $w^{\prime\prime}\in A^{\omega}$. Then, define
$\sigma(w^{\prime}v^{\prime})=v^{\prime\prime}$. Notice that in the case that
$w^{\prime}=\epsilon$, we have $v^{\prime}=v$.

Consider a finite play $wv$ compatible with $\sigma$ such that $wv\notin T$
and every prefix of $wv$ is contained in $T$. Then there is a play $\pi_{wv}$
in $W(G)$ such that $\mathsf{seq}_{A}(\pi_{wv})=wv$ and $\pi_{wv}$ either ends
in vertex $v$ or can be extended by $v$. Assume without loss of generality
that $\pi_{wv}$ ends in vertex $v$. Then,
$\sigma^{\prime}(\pi_{wv})=\pi^{\prime}$ for some $\pi^{\prime}\in
A^{\omega}$. As before, for every prefix $w^{\prime}$ of $\pi^{\prime}$ add
$wvw^{\prime}$ to $T$, which again keeps $T$ prefix closed. Furthermore,
consider a partition $w^{\prime}v^{\prime}v^{\prime\prime}w^{\prime\prime}$ of
$\pi^{\prime}$ such that $w^{\prime}\in A^{*}$, $v^{\prime}\in V_{\exists}$,
$v^{\prime\prime}\in V$, and $w^{\prime\prime}\in A^{\omega}$. Then, define
$\sigma(wvw^{\prime}v^{\prime})=v^{\prime\prime}$.

We have to show that $\sigma$ is graciously winning:

    * –

Consider an infinite play $\pi$ that is compatible with $\sigma$. Either $\pi$
is obtained from a finite number of moves of $\sigma^{\prime}$, in which case
the last move made by $\sigma^{\prime}$ ensures that $\pi$ satisfies
$\alpha_{S}$. Or $\pi$ is obtained from infinitely many moves of
$\sigma^{\prime}$, in which case $\pi$ satisfies $\alpha_{S}$ again.

    * –

Consider a prefix $p$ of a play $\pi$ that is compatible with $\sigma$. By
definition $p$ is obtained by some prefix $p^{\prime}$ of $p$ and a partition
of the play $\pi^{\prime}$ such that
$(p^{\prime},\pi^{\prime})=\sigma^{\prime}(p)$. It follows that
$p^{\prime}\pi^{\prime}$ extends $p$ and satisfies $\alpha_{W}$.

Full proof of Lemma 4.2 (Certificate existence):

######  Proof 7.2.

First we construct a suitable stem, intuitively by taking a finite prefix (of
sufficient length) of $\pi$ and removing redundant loops from this prefix. To
this end, we consider the finite sequence
$\rho=(\pi_{0},C_{0})(\pi_{1},C_{1})\ldots(\pi_{j},C_{j})$, where $C_{i}$ is
the $S$-fingerprint of the finite play $\pi_{0}\pi_{1}\ldots\pi_{i}$ so that
$C_{i}\subseteq C_{i+1}$ for all $i$. The position $j$ is picked to be the
least index such that each node that is visited by $\pi$ from position $j$ on
is visited infinitely often by $\pi$, and such that $C_{j}$ contains the set
of all $S$-colors that are visited by $\pi$ (including also the colors that
are visited finitely often by $\pi$). We use this position to separate the
stem and the loop of the prospective certificate as it is the first position
at which the fingerprint of $\pi$ has reached its full extent and from which
on only infinitely often occuring nodes are visited.

Now we repeatedly pick some two distinct indices $p$ and $q$ such that
$(\pi_{p},C_{p})=(\pi_{q},C_{q})$ and remove the subsequence
$(\pi_{p+1},C_{p+1})\ldots(\pi_{q},C_{q})$ from $\rho$; such subsequences
correspond to loops in $V$ that are taken by $\pi$ but along which no new
colors are added to the current fingerprint $C_{p}=C_{q}$. As $\rho$ is finite
to begin with, this process eventually terminates. In the remaining sequence,
each loop in $V$ adds at least one color from $S$ to the fingerprint; every
two pairs in the sequence are distinct, implying that its length is bounded by
$|S|\cdot|V|$. We define the stem $w$ to consist of the node components of
this shortened sequence. As $\pi$ is a play on $A$ and $w$ is obtained from a
finite prefix of $\pi$ by removing loops, $w$ is a finite play on $A$ as well.
By construction, whenever $w$ visits some node $v$ with $S$-fingerprint $C$,
so does $\pi$.

It remains to construct a suitable loop that starts at the end of $w$. To this
end, let $V_{\pi}$ and $E_{\pi}$ denote the set of nodes and moves,
respectively, that occur infinitely often in $\pi$. Then $(V_{\pi},E_{\pi})$
is a strongly connected sub-graph of $(V,E)$, that is, for all nodes
$v,v^{\prime}\in V_{\pi}$, there is a finite play of length at most
$|V_{\pi}|$ that starts at $v$, ends in $v^{\prime}$ and uses only moves from
$E_{\pi}$. It follows that there is, for all $v\in V_{\pi}$ and all moves
$e=(v_{1},v_{2})\in E_{\pi}$, a finite play of length at most $|V_{\pi}|+1$
starting at $v$ and containing the move $e$: there is a play $\tau$ of length
at most $|V_{\pi}|$ from $v$ to $v_{1}$; Thus $\tau v_{2}$ is a play of length
at most $|V_{\pi}|+1$ that starts at $v$ and contains the move $e$.

Let $C^{S}_{\pi}\subseteq S$ and $C^{W}_{\pi}\subseteq W$ be the sets of
colors that occur infinitely often in $\gamma_{S}(\pi)$ and $\gamma_{W}(\pi)$,
respectively. Recall that $\pi$ satisfies $\varphi_{S}$ and $\varphi_{W}$,
that is, that $\gamma_{S}(\pi)\models\varphi_{S}$ and
$\gamma_{W}(\pi)\models\varphi_{W}$. We construct the loop $u$, visiting one-
by-one all the colors contained in $C^{S}_{\pi}\cup C^{W}_{\pi}$, writing
$C^{S}_{\pi}\cup C^{W}_{\pi}=\\{c_{1},\ldots,c_{o}\\}$ and noting that
$o\leq|S|+|W|$. The definition is inductive: let $v_{0}$ be the last node in
the stem $w$ constructed above. For $1<i\leq o+1$, let $v_{i-1}$ be the last
node in the play $\tau_{i-1}$ constructed in the step for $i-1$. Then we
define $\tau_{i}$ to be some play of length at most $|V_{\pi}|+1$ that starts
at $v_{i-1}$ and uses some move with color $c_{i}$. We have shown above that
such a play always exists. Finally, let $\tau_{f}$ be some play of length at
most $|V_{\pi}|$ that starts at $v_{o}$ and ends in node that has a move to
the first node of $\tau_{1}$. Then the loop
$u=\tau_{1}\tau_{2}\ldots\tau_{o}\tau_{f}$ is a finite play of length at most
$(|V_{\pi}|+1)\cdot(|S|+|W|+1)$ that visits exactly the colors contained in
$C^{S}_{\pi}\cup C^{W}_{\pi}$. Furthermore, the edge $(\tau_{f},\tau_{1})$
satisfies
$\\{\gamma_{S}(\tau_{f},\tau_{1}),\gamma_{W}(\tau_{f},\tau_{1})\subseteq
C^{S})^{\pi}\cup C^{W}_{\pi}$. As $\pi$ satisfies both $\varphi_{S}$ and
$\varphi_{W}$, so does the infinite play $u^{\omega}$, showing that $(w,u)$ is
a certificate for $v$ in $G$. By construction, whenever $wu^{\omega}$ visits
some node $v$ with $S$-fingerprint $C$, so does $\pi$.

######  Example 7.3.

To see how the proof of Lemma 4.2 extracts certificates from witnesses,
consider the game depicted below, using colors $S=W=\\{a,b,c,d\\}$ and two
objectives over the same colors and color assignments

$\displaystyle\varphi_{S}$ $\displaystyle=(\mathsf{Inf}\leavevmode\nobreak\
a\to\mathsf{Inf}\leavevmode\nobreak\ c)\wedge\mathsf{Fin}\leavevmode\nobreak\
b$ $\displaystyle\varphi_{W}$ $\displaystyle=\mathsf{Inf}\leavevmode\nobreak\
d$ $x$$y$$z$$\\{a\\}$$\\{a\\}$$\\{a,d\\}$$\\{b\\}$$\\{a,c\\}$

Then $\pi=xyyz(yzz)^{\omega}$ is a play that results in the sequence
$\\{a\\}\\{b\\}\\{a\\}(\\{a,d\\}\\{a\\}\\{a,c\\})^{\omega}$ of sets of colors.
The sequence satisfies $\varphi_{S}$ and $\varphi_{W}$ since the colors $a$,
$c$ and $d$ occur infinitely often in it, but color $b$ does not. Making the
$S$-fingerprints in $\pi$ explicit, we obtain the sequence

$\displaystyle\rho=(x,\emptyset)(y,\\{a\\})(y,\\{a,b\\})(z,\\{a,b\\})(y,\\{a,b\\})(z,\\{a,b\\})((z,\\{a,b,c\\})(y,\\{a,b,c\\})(z,\\{a,b,c\\}))^{\omega}$

We note that after taking the first transition from $x$ to $y$, all nodes that
$\pi$ visits are visited infinitely often by $\pi$. Furthermore, $\pi$ is
cyclic from the third visit of $y$ on. The $S$-fingerprint however reaches its
full extent $\\{a,b,c\\}$ only upon the third visit of $z$, that is, at the
end of the first iteration of the loop $yzz$.

We obtain a stem from the fingerprint-increasing prefix

$\displaystyle\rho_{w}=(x,\emptyset)(y,\\{a\\})(y,\\{a,b\\})(z,\\{a,b\\})(y,\\{a,b\\})(z,\\{a,b\\})(z,\\{a,b,c\\})$

of $\rho$ by removing loops that do not change the fingerprint. This leads to
the sequence

$\displaystyle\rho_{w_{1}}=(x,\emptyset)(y,\\{a\\})(y,\\{a,b\\})(z,\\{a,b\\})(z,\\{a,b,c\\}).$

The node components of this sequence yield the stem $w=xyyzz$.

To obtain a suitable loop, we consider the subgraph $(V_{\pi},E_{\pi})$ that
is given by the moves that are taken infinitely often in $\pi$; this graph
consists of the edges $(y,z)$, $(z,z)$ and $(z,y)$; the colors $a$, $c$ and
$d$ are visited infinitely often by $\pi$, so we construct the loop
$u=\tau_{a}\tau_{c}\tau_{d}\tau_{f}$, using only edges from $E_{\pi}$, where
$\tau_{a}=zy$, that is, $\tau_{a}$ is a play that starts at the end node $z$
of the stem $w$ and takes some edge with color $a$ (in this case we pick the
edge $(z,y)$); furthermore, $\tau_{c}=yzz$ is a play that starts at the end
node $y$ of $\tau_{a}$ and uses the edge $(z,z)$, seeing color $c$. Then
$\tau_{d}=zy$ is a play that starts at the end node of $\tau_{c}$ and uses the
edge $(z,y)$ with color $d$, and finally, $\tau_{f}=yz$ is a play connecting
the end node of $\tau_{d}$ and the start node of $\tau_{a}$, closing the loop.
This results in an overall certificate

$\displaystyle wu=xyyzz\leavevmode\nobreak\ yzzyz$

with sequence
$\\{a\\}\\{b\\}\\{a\\}\\{a,c\\}\\{a,d\\}(\\{a\\}\\{a,c\\}\\{a,d\\}\\{a\\}\\{a,d\\})^{\omega}$
of sets of colors. Thus the certificate visits the colors $a,c$ and $d$ (but
not $b$) infinitely often so that it satisfies both $\varphi_{S}$ and
$\varphi_{W}$. Furthermore, for every node $v$ that is visited with
$S$-fingerprint $C$ in the certificate, the node $v$ is visited with
fingerprint $C$ in $\pi$ as well. In particular the choice of the starting
point of the loop ensures that the $S$-fingerprints for all nodes in the loop
have reached the full extent $\\{a,b,c\\}$.

######  Lemma 7.4.

Let $G$ be an obliging game and let $v$ be a node in $G$. If player $\exists$
wins from $v$ in $W(G)$, then player $\exists$ wins from $v$ in $C(G)$.

######  Proof 7.5.

Let $\sigma$ be a winning strategy for player $\exists$ in $W(G)$. We
inductively construct a strategy $\tau$ for the game $C(G)$; as invariant of
the inductive construction, we associate with every finite play $\pi$ of
$C(G)$ that adheres to the strategy $\tau$ constructed so far, a finite play
$\rho_{\pi}$ of $W(G)$ that adheres to $\sigma$. In the base case of the empty
play $\epsilon$ that consists just of $v$, we put $\rho_{\epsilon}=\epsilon$.

For the inductive step, let $\pi w_{\exists}$ be a finite play ending in
$w_{\exists}$ that adheres to the part of $\tau$ that has been constructed so
far, and let $\rho_{\pi}w$ be the associated play that adheres to $\sigma$. As
$\sigma$ wins $w$, there is a witness $\epsilon$ such that
$\sigma(\rho_{\pi})=\epsilon$. From $\sigma$ being winning, we conclude that
$\epsilon$ satisfies $\gamma_{W}$ and $\gamma_{S}$. By Lemma 4.2, there is
some certificate $c=w_{0}w_{1}\ldots\in\mathsf{Cert}(w)$ such that for all
positions $i$ in $c$, there is a position $j$ in $\epsilon$ such that
$w_{i}=\xi_{j}$ and the $S$-fingerprints of $w_{0}\ldots w_{i}$ and
$\xi_{0}\ldots\xi_{j}$ coincide. We put $\tau(\pi w_{\exists})=c$. For every
position $i$ in $c$ such that $w_{i}\in V_{\forall}$ and every $w^{\prime}\in
E(w_{i})$, we have a move $(c,(c,i,w^{\prime}))$ in $C(G)$. Then there is some
$j$ such that $\xi_{j}=w_{i}$ and the $S$-fingerprints of $w_{0}\ldots w_{i}$
and $\xi_{0}\xi_{1}\ldots\xi_{j}$ coincide, where $w_{0}=\xi_{0}=w$. We extend
the play $\rho_{\pi}w$ that is associated with $\pi w_{\exists}$ to the play
$\rho w\xi_{1}\ldots\xi_{j}w^{\prime}$ and associate it to the play $\pi
w_{\exists}cw_{i}w^{\prime}$. By construction, these extended plays are
compatible with $\sigma$ and the part of $\tau$ that has been constructed so
far. For moves from $E$ taken in $C(G)$, the associated play is updated
accordingly.

It remains to show that $\tau$ is a winning strategy for $v$ in $C(G)$, that
is, that every play of $C(G)$ that starts at $v$ and adheres to $\tau$
satisfies $\varphi_{S}$. To this end, let $\pi$ be a play that starts at $v$
and adheres to $\tau$ and let $\rho_{\pi}$ be the play in $W(G)$ that is
associated with $\tau$ according to the inductive invariant of the
construction of $\tau$; recall that $\rho_{\pi}$ adheres to $\sigma$. We note
that by construction, player $\exists$ always is able to pick a valid
certificate as long as they follow strategy $\tau$. As player $\exists$
graciously wins $v$ using the strategy $\sigma$, $\rho_{\pi}$ satisfies
$\varphi_{S}$. By construction, the $S$-fingerprints in $\pi$ and $\rho_{\pi}$
coincide so that $\tau$ satisfies $\varphi_{S}$ as well.

Proof of Lemma 5.2 (Correctness of lazy LAR reduction):

######  Proof 7.6.

By slight abuse of notation, we let $\Omega(\tau)$ denote the maximal
$\Omega$-priority that is visited in $\tau$, having $\Omega(\tau)=2(p(\tau))$
if $\pi_{0}[p(\tau)]\models\varphi_{C}$ and $\Omega(\tau)=2(p(\tau))+1$ if
$\pi_{0}[p(\tau)]\not\models\varphi_{C}$.

  * $\Rightarrow$

Let $\sigma=(\Pi(C),\mathsf{update}_{\sigma},\mathsf{move}_{\sigma})$ be a
strategy with memory $\Pi(C)$ for player $\exists$ in $G$ with which they win
every node from their winning region. It has been shown in a previous LAR
reduction for Emerson-Lei games [HunterD05] that winning strategies with this
amount of memory always exist. We define a strategy
$\rho=(\Pi(C),\mathsf{update}_{\rho},\mathsf{move}_{\rho})$ with memory
$\Pi(C)$ for player $\exists$ in $P(G)$ by putting
$\mathsf{update}_{\rho}(\pi,((v,\pi^{\prime}),(w,\pi^{\prime\prime})))=\mathsf{update}_{\sigma}(\pi,(v,w))$
and $\mathsf{move}_{\rho}((v,\pi^{\prime}),\pi)=(w,\pi@\gamma_{C}(v,w))$ where
$w=\mathsf{move}_{\rho}(v,\pi)$. Thus $\rho$ updates the memory and picks
moves just as $\sigma$ does, but also updates the permutation component in
$P(G)$ according to the taken moves; hence $\rho$ is a valid strategy.

We show that $\rho$ wins a node $(v,\pi)$ in $P(G)$ whenever $v$ is in the
winning region of player $\exists$ in $G$. To this end, let
$\tau=(v_{0},\pi_{0})(v_{1},\pi_{1})\ldots$ be a play of $P(G)$ that starts at
$(v_{0},\pi_{0})=(v,\pi)$ and is compatible with $\rho$. By construction,
$\pi=v_{0}v_{1}\ldots$ is a play that is compatible with $\sigma$. Since
$\sigma$ is a winning strategy for player $\exists$, we have
$\gamma_{C}(\pi)\models\varphi_{C}$. There is a number $i$ such that all
colors that appear in $\pi$ from position $i$ on occur infinitely often. Let
$p$ be the number of colors that appear infinitely often in $\pi$. It follows
by definition of $\pi@D$ for $D\subseteq C$ (which moves the single right-most
element of $\pi$ that is contained in $D$ to the very front of $\pi$), that
there is a position $j\geq i$ such that the left-most $p$ elements of
$\pi_{j}$ are exactly the colors occuring infinitely often in $\pi$ (and all
colors to the right of $\pi_{j}(p)$ are never visited from position $j$ on).
It follows that from position $j$ on, $\tau$ never visits a priority larger
than $2p$. To see that $\tau$ infinitely often visits priority $2p$ we note
that $\pi_{j}^{\prime}[p]\models\varphi_{C}$ for every $j^{\prime}>j$, so it
suffices to show that $p$ infinitely often is the rightmost position in the
permutation component of $\tau$ that is visited. This is the case since, from
position $j$ on, the $p$-th element in the permutation component of $\tau$
cycles fairly through all colors that are visited infinitely often by $\pi$.

  * $\Leftarrow$

Let $\rho$ be a positional strategy for player $\exists$ in $P(G)$ with which
they win every node from their winning region. We define a strategy
$\sigma=(\Pi(C),\mathsf{update}_{\sigma},\mathsf{move}_{\sigma})$ with memory
$\Pi(C)$ for player $\exists$ in $G$ by putting
$\mathsf{update}_{\sigma}(\pi,(v,w))=\pi@\gamma_{C}(v,w)$ and
$\mathsf{move}_{\sigma}(v,\pi)=w$ where $w$ is such that
$\rho(v,\pi)=(w,\pi@\gamma_{C}(v,w))$. Thus $\sigma$ updates the memory and
picks moves just as plays that follow $\rho$ do.

We show that $\sigma$ wins a node $v$ in $G$ whenever $(v,\pi)$ is in the
winning region of player $\exists$ in $P(G)$. To this end, let
$\pi=v_{0}v_{1}\ldots$ be a play of $G$ that starts at $v_{0}=v$ and is
compatible with $\sigma$. By construction, $\pi$ induces a play
$\tau=(v_{0},\pi_{0})(v_{1},\pi_{1})\ldots$ with $(v_{0},\pi_{0})=(v,\pi)$ and
$\pi_{i+1}=\pi_{i}@\gamma_{C}(v_{i},v_{i+1})$ for $i\geq 0$ that is compatible
with $\rho$. Since $\rho$ is a winning strategy for player $\exists$, the
maximal priority in it is even (say $2p$). Again, $p$ is the position such
that the left-most $p$ elements in the permutation component of $\rho$ from
some point on contain exactly the colors that are visited infinitely often by
$\pi$. It follows that $\gamma_{C}(\pi)\models\varphi_{C}$.

Proof of Lemma 5.8 (Correctness of efficient DAG attractor computation):

######  Proof 7.7.

For one direction, let player $\exists$ be able to attract to $\overline{V}$
from $(v,\pi)$ within $\mathsf{Cert}\times\Pi(S)$. Then there is a valid
certificate $c=v_{0}\ldots v_{m}\in\mathsf{Cert}(v)$ for $v$ (with $v_{0}=v$)
such that for all positions $i$ in $c$ such that $v_{i}\in V_{\forall}$ and
for all $w\in E(v_{i})$, we have $w\in V_{2p+1}$ or $w\in V_{2p}$, that is,
$c$ is safe. Here, $p$ is the rightmost position in $\pi$ such that
$\pi(p)\in\gamma_{S}(v_{0}\ldots v_{i}w)$. Let $u=v_{0}\ldots v_{q}$ be the
stem of $c$ and $w=v_{q+1}\ldots v_{m}$ the loop. Let $i$ be the priority
corresponding to the $S$-fingerprint of the stem $u$ with respect to $\pi$.
Define a run $\tau$ of the automaton $A_{i}$ from the procedure that computes
the set $M$ by $\tau(0)=(v_{q+1},i)$ and $\tau(j)=(v_{q+1+j},i)$ for $j>0$;
here we use $v_{q+1+j}$ to refer to the $j$-th position in the infinite run
$w^{\omega}$. As $c$ is a safe certificate, $\tau$ only visits such game nodes
$v_{r}\in V_{\forall}$ such that for all successors $w^{\prime}\in E(v_{r})$
of $v_{r}$, we have $(w^{\prime},i)\in V_{i}$. Thus $\tau$ indeed is an
admissible run of $A_{i}$. As $c$ is a valid certificate, we have
$\gamma_{S}(u)\models\varphi_{S}$ and $\gamma_{W}(u)\models\varphi_{W}$ so
that $\mathsf{Inf}(\gamma_{C}(\tau))\models\varphi_{C}$, showing that $\tau$
is accepting. Thus $(v_{q+1},i)$ is contained in $N_{i}$. Now we argue that
$(v,0)$ is contained in the graph $M$ after the construction of $M$
terminates. This indeed is the case since the stem $u$ of the certificate $c$
is safe by assumption; thus the stem corresponds to a path from $(v,0)$ to
$(v_{q+1},i)$ that visits only such nodes $(v_{j},p)$ with $v_{j}\in
V_{\forall}$ where we again have that for all $w^{\prime}\in E(v_{j})$,
$(w^{\prime},p^{\prime})\in V_{2p^{\prime}}$ or $(w^{\prime},p^{\prime})\in
V_{2p^{\prime}+1}$, where $p^{\prime}=\max(p,\Omega_{\pi}(v_{j},w^{\prime})$.

For the converse direction, let $(v,0)$ be contained in the graph $M$ after
the computation terminates. Then there is $i$ such that the automaton $A_{i}$
is non-empty and there is a path from $(v,0)$ to some $(v_{q+1},i)$ in $M$.
Let $\tau=(v_{0},p_{0})(v_{1},p_{1})\ldots$ be a path in $M$ (starting at
$(v,0)$ so that $v_{0}=v$) that witnesses these facts by combining the path
from $(v,0)$ to $(v_{q+1},i)$ and then looping within $N_{i}$. We extract a
valid certificate from $\tau$ as follows. Define the stem to be
$w=v_{0}v1\ldots v_{q+1}$. Extract the loop $u$ as in the proof of Lemma 4.2,
that is, by walking through the set of game nodes that occur infinitely often
in $\tau$ and visiting all colors from $\gamma_{S}(u)\cup\gamma_{W}(u)$. As
$\tau$ is accepting,
$\gamma_{S}(u)\cup\gamma_{W}(u)\models\varphi_{S}\wedge\varphi_{W}$, showing
that $c=wu$ is a valid certificate. It remains to show that for all positions
$i$ in $c$ such that $v_{i}\in V_{\forall}$ and for all $w\in E(v_{i})$ such
that $w\neq v_{i+1}$, we have $w\in V_{2p+1}$ or $w\in V_{2p}$, where $p$
again is the rightmost position in $\pi$ such that
$\pi(p)\in\gamma_{S}(v_{0}\ldots v_{i}w)$. This is the case since all unsafe
vertices have been removed from $M$ so that $\tau$ visits only safe vertices
(that have the required property).