A Parity Game Tale of Two Counters
Tom van Dijk


Variability and Jet Activity in the YSO MHO 3252 Y3
in Serpens South
    Rolf Chini
    December 30, 2023
====================================================================






Parity games are simple infinite games played on finite graphs with a winning condition that is expressive enough to capture nested least and greatest fixpoints.
Through their tight relationship to the modal mu-calculus, they are used in practice for the model-checking and synthesis problems of the mu-calculus and related temporal logics like LTL and CTL.
Solving parity games is a compelling complexity theoretic problem, as the problem lies in the intersection of UP and co-UP and is believed to admit a polynomial-time solution, motivating researchers to either find such a solution or to find superpolynomial lower bounds for existing algorithms to improve the understanding of parity games.

We present a parameterized parity game called the Two Counters game, which provides an exponential lower bound for a wide range of attractor-based parity game solving algorithms.
We are the first to provide an exponential lower bound to priority promotion with the delayed promotion policy, and the first to provide such a lower bound to tangle learning.





§ INTRODUCTION




Parity games are turn-based games played on a finite graph.
Two players Odd and Even play an infinite game by moving a token along the edges of the graph.
Each vertex is labeled with a natural number priority and the winner of the game is determined by the parity of the highest priority that is encountered infinitely often.
Player Odd wins if this parity is odd; otherwise, player Even wins.

Parity games play a central role in several domains in theoretical computer science.
Their study has been motivated by their relation to various problems in formal verification and synthesis that can be reduced to solving parity games, as parity games capture the expressive power of nested least and greatest fixpoint operators <cit.>.
Deciding the winner of a parity game is polynomial-time equivalent to checking non-emptiness of non-deterministic parity tree automata <cit.>, and to the explicit model-checking problem of the modal μ-calculus <cit.>.
Synthesis problems ask for an implementation of a system that satisfies the desired properties and reactive synthesis tools like Strix use parity games to synthesize controllers satisfying LTL formulas <cit.>.
Solving the related parity game either results in a correct implementation or in a counterexample demonstrating how an adversary can make the property fail.

Parity games are also interesting for complexity theory, 
as the problem of determining the winner of a parity game is known to lie in UP∩co-UP <cit.>,
which is contained in NP∩co-NP <cit.>.
This problem is therefore unlikely to be NP-complete and it is widely believed that a polynomial solution exists.

Recent work proposes novel algorithms based on the notion of a tangle <cit.>.
A tangle is a strongly connected subgame of a parity game for which one player has a strategy to win all cycles in the subgame.
Tangles play a fundamental role in various parity game algorithms, but most algorithms are not explicitly aware of tangles and can explore the same tangles repeatedly <cit.>.
The algorithms proposed in <cit.> solve parity games by explicitly computing tangles using attractor computation.

Tangles are related to snares <cit.> and quasi-dominions <cit.>, with the critical difference that tangles are strongly connected whereas snares and quasi-dominions may be composed of multiple tangles.
Thus it is an obvious question whether the subexponential counterexample of Friedmann <cit.> to Fearnley's snare-based algorithm <cit.>
can be adapted for tangle learning.
We show that this is possible and that the resulting counterexample is powerful enough to be a difficult lower bound to a wide range of algorithms.

We propose a parameterized parity game based on binary counters.
The goal is to trick the algorithms to explore the progression of the counters, only solving the game when all bits are set.
The critical ingredient to make these games difficult for attractor-based algorithms is to use two intertwined binary counters, one for each player, that progress together.
We show empirically that these games are difficult for a wide range of algorithms, in particular for those based on attractor computation, such as priority promotion <cit.> and its variations <cit.>, tangle learning <cit.>, and the recursive algorithm by Zielonka <cit.>.

For these, we provide the exponential lower bound of
Ω(2^√(n)).

We are the first to provide an exponential lower bound for the delayed promotion policy of priority promotion and for tangle learning.



§ PRELIMINARIES










A parity game  is a tuple (, , E, ) where V= is a set of n vertices partitioned into the sets  controlled by player Even and  controlled by player Odd, and E⊆ V× V is a left-total binary relation describing all moves, i.e., every vertex has at least one successor.
We also write E(u) for all successors of u and u→ v for v∈ E(u).
The function V→{0,1,…,d}
assigns to each vertex a priority, where d is the highest priority in the game.
We write α∈{,} to denote a player  or  and  for the opponent of α. 
In visual representations of parity games, we use diamonds and boxes for vertices of the two players. 

We write 
(V) for max{(v)| v∈ V} and 
similarly () for the highest priority in .
Furthermore, we write ^-1(i) for all vertices with the priority i.
A play π=v_0 v_1 … is an infinite sequence of vertices consistent with E, i.e.,
v_i → v_i+1 for all i≥ 0. 

We denote with inf(π) the vertices in π that occur infinitely many times in π.
Player Even wins a play π if (inf(π)) is even; player Odd wins if (inf(π)) is odd.
We write Plays(v) to denote all plays starting at vertex v
and Plays(V) for {π∈Plays(v)| v∈ V}.


A (positional) strategy σ V↛ V assigns to each vertex in its domain a single successor in E, i.e., σ⊆ E.
We refer to a strategy of player α to restrict the domain of σ to V_α. 
In the remainder, all strategies σ are of a player α.
Given a strategy σ, we define the subgame induced by σ as [σ] := (V_, V_, E', ) where E':={ uv ∈ E | u∉(σ) σ(u)=v }.
We write Plays(v, σ) for all plays from v consistent with σ, i.e., Plays_[σ](v), 

and Plays(V,σ) for {π∈Plays(v,σ)| v∈ V}.




A basic result for parity games is that they are memoryless determined <cit.>, i.e., each vertex is either winning for player Even or for player Odd, and the players have a positional strategy for their winning vertices.
Player α wins vertex v if there is a strategy σ such that player α wins all plays in Plays(v,σ).


A set of vertices U is called closed with respect to player α if all vertices that belong to player α have a successor in U and all vertices of player  only have successors inside U.
That is, player  cannot leave U.
If a set of vertices is closed in the full game  then we also call the set globally closed and if it is closed in some subgame of  then we call the set locally closed in that subgame.


A dominion D is a (globally) closed set of vertices for which player α has a strategy σ such that player α wins all plays in Plays(D,σ). 
That is, player α wins all cycles in the subgame [D,σ] induced by D and σ. 
We also write a p-dominion for a dominion where p is the highest priority encountered infinitely often in plays consistent with σ, i.e., p:=max{(inf(π))|π∈Plays(D,σ)}.


Several algorithms for solving parity games employ attractor computation.
Given a set of vertices A,
the attractor of A for a player α contains exactly those vertices from which player α can ensure arrival in A.
We write ^_α(A) to attract vertices in  to A as player α,
i.e., the least fixpoint of

    Z := A ∪{ v∈ V_α| E(v)∩ Z ≠∅}∪{ v∈ V_| E(v)⊆ Z }

We compute the α-attractor of A with a backward search from A, initially setting Z:=A and iteratively adding α-vertices with a successor in Z and -vertices with no successors outside Z.


We call a set of vertices A α-maximal if A=^_α(A).
The attractor also yields an “attractor strategy” by selecting a vertex in Z for every added α-vertex v when v is added to Z, and by selecting a vertex in Z for all α-vertices in A that do not yet have a strategy but can play to Z.

Attractors are often used to attract to a set A:=^-1(()) for the player that wins the highest priority in .
By repeatedly computing this attractor and removing it from the game, the game is decomposed into regions each associated with the priority p and player α=p  2.
Each such region has the property that all plays that stay in the region are won by player α, and that player  can leave the region to higher α-regions and, only via a vertex of priority p, to lower regions.
The recursive algorithm <cit.> investigates whether (lower) α-regions attract vertices from higher -regions.
Priority promotion <cit.> merges locally closed regions with higher α-regions that the opponent can escape to.
Tangle learning <cit.> computes tangles from locally closed regions which are used to improve the attractor-based decomposition. 






§ RECURSIVE ALGORITHM


































The recursive algorithm by Zielonka <cit.> is a well-known algorithm to solve parity games with fast practical performance <cit.>.
Although it requires exponential time in the worst-case, tight bounds are known for various classes of games <cit.>.
Very recently, Parys has proposed a version of the recursive algorithm that runs in quasi-polynomial time <cit.>.


The recursive algorithm is based on attractor computation.
See Algorithm <ref>.
We omit computing the winning strategy.
At each step, given the current subgame , the algorithm computes the attractor A to the highest vertices in  and recursively solves the subgame ∖ A. 



If the opponent  can attract vertices in A to W_, then  wins B := Attr^_(W_).
The vertices attracted to W_ are vertices of priority p that are now estimated to be won by player  plus vertices of priority <p that player  attracts to W_ via vertices of priority p.
The algorithm then computes the remaining subgame ∖ B recursively and returns the winning regions.
If player  does not attract any vertices to W_, then no second recursion is needed.
The winning strategies are trivially obtained as the attractor strategy plus any successor in the set W_α∪ A for α-vertices with priority p.

One can also view the recursive algorithm as decomposing the game into α-maximal regions and refining these regions starting with the lowest region.



§ PRIORITY PROMOTION




























Priority promotion was proposed in <cit.> and improved in <cit.>.
Like the recursive algorithm, priority promotion computes the top-down α-maximal decomposition of the game into regions.

These regions have the property that all plays that stay in the region are won by player α.
Regions are locally closed when all vertices of player α have a successor in the region and no vertices of player  can play to lower regions.
Because all regions are α-maximal, player  can only escape to “higher” regions of player α.
Locally closed regions are merged with the lowest higher region to which player  can escape, after which the decomposition of the game is refined by attracting to this merged region and recomputing the lower regions.
This is called promoting, as the lower region is “promoted” to the higher region.


See Algorithm <ref>.
Again we omit explicitly computing the winning strategies, but they are computed trivially by the attractors.
The  algorithm is given a game and returns a dominion and the winner of this dominion.
By repeatedly calling  and removing the dominion from , priority promotion solves parity games.
The  algorithm refines the regions until a dominion is found.
The function  records the current region (priority p) of each vertex, or  if the vertex is not in a region.
After promoting a region to a higher priority p (lines 15–16) the algorithm resets all regions below p and then attracts to the merged region at lines 5–8.

Consider some region of priority 4 that is promoted to priority 16.
By attracting to the combined region 16, priority promotion attracts vertices from regions 5…15 of player  that are attracted to the lower region 4 in one step, while the recursive algorithm attracts from each affected region of  separately.
Another difference with the recursive algorithm is that priority promotion always promotes the highest locally closed region whereas the recursive algorithm starts refining with the lowest regions.

The original algorithm <cit.> resets all lower regions after a promotion.
These lower regions might be the result of earlier promotions and these promotions are then often repeated.
The PP+ extension <cit.> only resets lower regions of player , since promoting regions of player α can only “break” regions of player .
The region restoration (RR) extension <cit.> further improves upon PP+ by only resetting a lower region if the earlier attractor strategy of the player for the vertices that are still in the original region now leaves this region to a higher region (of the opponent).
The delayed promotion (DP) policy (also <cit.>) uses a heuristic to delay promotions.
The algorithm records which regions are the result of a promotion and 
if another promotion might affect a merged region, then this promotion is delayed.
The delayed promotions are instead performed on a copy of the decomposition.
When no more normal promotions can be performed, the delayed promotions of one player are applied from this copy, where this player is the one that wins the highest merged region in the copy.
The other delayed promotions are discarded and the algorithm continues with an empty record of merged regions.





§ TANGLES AND TANGLE LEARNING




Earlier work introduced tangles as substructures of parity games <cit.>.
Tangles are strongly connected subgames of a parity game for which one player has a strategy to win all cycles in the subgame.
The losing player must therefore escape the tangle, so we extend attractor computation to simultaneously attract all vertices in a tangle when the losing player must escape to the attracting set.
This leads to the tangle learning algorithm, which computes new tangles along the decomposition of the game, computed using the extended attractor.
The algorithm solves parity games by finding tangles that are dominions.


A p-tangle is a nonempty set of vertices U⊆ V with p=(U), for which player α≡_2 p has a strategy σ U_α→ U,
such that the graph (U,E'), with 
E':= E∩(σ∪(U_× U)),
is strongly connected
and player α wins all cycles in (U,E').








	A tangle is a pair T=(U,σ) where U is a nonempty set of vertices U⊆ V and σ U_α→ U is a strategy for all vertices in U of player α := (U) 2, such that the subgame [U,σ] induced by the tangle
	
	is strongly connected and player α wins all cycles in [U,σ].

We say that a tangle with the highest priority p is a p-tangle, and that it is an α-tangle. 
We often use T for just the set of vertices in the tangle, e.g., 
writing v∈ T if a vertex v is in the tangle.
We write E_T(T) for the successors outside T from -vertices in T,

E_T(T) := {  v ∈ V∖ T | u → v | u∈ T∩ V_ }.


We have several basic observations related to tangles <cit.>.
A closed p-tangle, from which player  cannot leave, is a p-dominion.
Vice versa, every p-dominion contains at least one p-tangle.
Furthermore, tangles are often composed of subtangles with lower priorities.


We thus find a hierarchy of tangles in any dominion D with winning strategy σ
by computing the set of winning priorities
{ (inf(π))|π∈Plays(D,σ) }.
There is a p-tangle in D for every p in this set.
Tangles are thus intuitive substructures of dominions.
One can find all tangles in a dominion D by computing { inf(π)|π∈Plays(D,σ) }.

See for example Figure <ref>. Player Odd wins 
with 
strategy { d→e }.
Player Even can avoid priority 5, but then loses with priority 3.

The 5-dominion contains a 5-tangle and a 3-tangle.




 




As described in <cit.>, tangles play a central role for various parity game solving algorithms, as they implicitly explore tangles and may explore the same tangles repeatedly, especially when tangles are nested.
This motivates algorithms that explicitly target tangles, such as the “snare memoization” extension to strategy improvement <cit.> and the “tangle attractor” approach of tangle learning <cit.>.







Tangle learning is based on the tangle attractor,
extending
attractor computation to 
attract vertices of α-tangles where player  must play to the attracting set, writing ^, T_α(A) to attract vertices in subgame  and vertices of α-tangles in the set T that are in subgame  to A as player α,
i.e., the least fixpoint of

    r@l
    Z := A     ∪ { v∈ V_α| E(v)∩ Z ≠∅ } ∪ { v∈ V_| E(v)⊆ Z }
        ∪ {  v∈ T| T∈ T⊆ V(T)≡_2α
    E_T(T)⊆ Z  }


See further <cit.>.
The tangle learning algorithm (Algorithm <ref>) repeatedly decomposes the game with the tangle attractor.
By computing the bottom strongly connected components of the regions, new tangles are obtained and added to the set of tangles T (line 12).
Each iteration of this algorithm adds new tangles to this set, resulting in a different decomposition each time.
Tangles without escapes, i.e., closed tangles, are dominions, which are then maximized using the attractor and removed from the game (lines 13–16).
After removing the dominions, all tangles with solved vertices are removed from T (line 17).
As before, winning strategies are obtained from the attractor.
We omit explicitly computing the winning strategies, but we do need the strategy that the tangle attractor yields for computing the tangles at line 6 as explained in <cit.>.
A variation called “alternating tangle learning” is also described in <cit.>, which alternates between exhaustively computing only tangles for player Odd or for player Even.


A closed region is essentially a collection of possibly unconnected tangles and vertices attracted to these tangles.

Compared to tangle learning, priority promotion “attracts” all tangles in the region to the lowest region that would attract a tangle in the region, and then discards knowledge of the tangles.



§ DISTRACTIONS









We introduce the notion of a distraction <cit.> to further our understanding of parity game solving algorithms.



A distraction for player α is a vertex v with an α-priority p, such that if player α always plays to reach v along paths of priorities ≤ p, then player  wins v and all vertices that reach v.
That is, a distraction for α is a high value vertex v with an α-priority that player  can win if player α always tries to visit it.


This occurs when player  can attract v to some vertex of a higher priority of player ,
or when player  can attract v to an -dominion.



For attractor-based algorithms, the difficult distractions are those that are not immediately clear from the initial decomposition of the game, that is, when a distraction is attracted by the opponent via a lower tangle.









Initially player α believes they should play to v, but after solving the lower subgame or finding the attracting tangle in the lower subgame, playing to v is believed to be good for the opponent.
See e.g. Fig. <ref>.
Vertices a and f are distractions.
This is however not immediately clear.


We say that a distraction v distracts a tangle T, with v∉ T, if there is some distracted vertex w∈ T, that is attracted by v but can also avoid v to play inside tangle T and player  cannot escape T towards v.

In order to learn the distracted tangle, the solver first needs to identify and avoid the distraction.
As argued in <cit.>, tangle learning identifies distractions by learning the -tangle that attracts the distraction.

Zielonka's recursive algorithm and priority promotion also rely on this mechanism to avoid distractions.
In priority promotion, whenever a merged region attracts the highest vertices from -regions, then these vertices are distractions.
In the recursive algorithm, the second recursive call is only performed if the opponent attracts from A, that is, when it discovers the attracted p-vertices in A are distractions.


Thus, distractions make these algorithms slow, especially when lower distractions must be identified before and after removing a higher distraction.
If there are no distractions in the game, then both the recursive algorithm and priority promotion require at most n recursive calls or promotions.


Algorithms that are based on play valuations such as progress measures and strategy iteration (see <cit.>) rely on a fundamentally different method to deal with distractions.
They assign a higher value to vertices with α's priorities along the attractor paths towards vertices in A, and if a vertex in A is a distraction, then it does not increase in value, causing these algorithms to avoid it.








§ A TALE OF TWO COUNTERS




The design of our parameterized parity game is loosely inspired upon earlier work by Friedmann <cit.>, which provides an exponential lower bound for the non-oblivious strategy improvement algorithm <cit.>.
That algorithm is a variation of strategy improvement that learns snares, which are related to tangles.
However, attractor-based algorithms trivially solve these games and require a different approach.

The parity game consists of two binary counters.
Each kth bit of the counter is a structure that contains 2^k many tangles.
A bit in the counter of player α is set by attracting a distraction for player  called a “low” vertex via a lower α-tangle to a “high” vertex.
We use two counters, one for each player, that are intertwined and progress in turns.
First the counter of player Even increases, then of player Odd, etc.
The bits are connected to the higher bits such that this tangle is no longer “attracting” when the higher bits of the opponent change, letting the opponent escape the tangle, thus the tangle no longer attracts the distraction and the bit is reset.
So when bit x of player α is set, then all bits below x of player  are reset.
Furthermore, if lower bits of the opponent are not set, then the tangle cannot be found because the player is distracted by these distractions.
Bit x of player Odd is distracted by bits ≤x of player Even, while bit x of player Even is distracted by bits <x of player Odd.
The result is the following example progression:


	 to 0.45X[l]X[l]X[6l]
		Even     Odd     Event 

		000     000     Initial state 

		001     000     Set Even 3 

		001     001     Set Odd 3 

		011     000     Set Even 2 (reset Odd 3) 

		010     010     Set Odd 2 (reset Even 3) 

		011     010     Set Even 3 

		011     011     Set Odd 3 

		111     000     Set Even 1 (reset Odd 2, 3) 

		100     100     Set Odd 1 (reset Even 2, 3) 

		101     100     Set Even 3

		101     101     Set Odd 3 

		111     100     Set Even 2 (reset Odd 3) 

		110     110     Set Odd 2 (reset Even 3) 

		111     110     Set Even 3

		111     111     Set Odd 3 

		
	


Notice that the state of the counters after every Odd bit, colored blue, tracks the progression of the counters,
while after every Even bit the counters are in an intermediate state.






See Fig. <ref> for bit 2 of some player α in a 5-bit counter.
The highest bit is bit 0 and the lowest bit is bit 4.
Vertex l is the “low” vertex and has a high priority of player 's parity.
This vertex is a distraction for the opponent if the bit is not set.
Vertex h is the “high” vertex and has a high priority of player α's parity.
Vertices h and l of higher bits have higher priorities.
Vertex h has an edge to the input of the next higher bit, except vertex h of the highest bit has an edge to the input of the lowest bit.
When all bits are set, the algorithms can find the winning dominion by connecting all bits.
Vertex t is the “tangle” vertex and has priority 2 for even bits and priority 1 for odd bits.
All other vertices have the priority (t)-1.









To find a tangle, player α must force their opponent to play from t to z such that the opponent can only escape to h or to higher regions of player α.
Each tangle in the bit uses a different path from t to z, depending on the state of the higher bits.
As the two counters progress together, either l_α(0) is good for α and l_(0) is bad for α, or vice versa.
In Fig. <ref>, if bit 0 is set and bit 1 is unset, then the path via a(0) and b(1) forces the opponent to stay in the tangle, whereas they could play to their own region via b(0) and a(1).
Furthermore, player α must choose to play from z to t.
When lower -bits are not set, the l_ vertices are in a region of player α higher than t and are thus more attractive to play to, preventing player α from learning the tangle.
Finally, we have an asymmetry, since one player starts counting first having the lowest priority l and h vertices.
We only have the edge from vertex z to the matching vertex l_ for the bits of the second player.
This forces the second player to wait until the first player sets the matching bit.

See Table <ref> for an example with 3 bits,
and Fig. <ref> for the full 3-bit Two Counters game.
Since player Even has the lower priorities, player Even first sets bit 2, followed by player Odd.
When all bits are set, both players have a dominion consisting of their entire counter via the blue edges.

The number of vertices for a Two Counters game with N bits for both players is 3N^2+5N and the number of edges is 7N^2+4N.
















§ EMPIRICAL EVALUATION




To assess the runtime complexity of solving N-bit Two Counters games with different algorithms,
we solve them with these algorithms and obtain a relevant statistic that is indicative of the runtime.
In this section, we support the claim that the games are exponential for these solvers based on this statistic.
Although this is a weaker basis than a machine-checkable complexity proof, such a proof is more difficult to produce and to understand, while the exponential behavior is clear from the empirical data.
However, in Section <ref>,
we do take a closer look at how these algorithms solve the Two Counters games,
and we sketch out an inductive proof that the algorithms require exponentially many steps for higher N.



To solve the games we use the implementation of the algorithms in the parity game solver Oink <cit.>, but we have also confirmed the results with implementations in PGSolver <cit.>.
We use the following command line to obtain the results:



	0.75
		 

		 

		
	






















In Table <ref>,
we report the following statistic for each solver:

	
  * the number of recursive calls for Zielonka's recursive algorithm (ZLK)
	
  * the number of promotions for priority promotion (PP, DP, RR, RRDP)
	
  * the number of tangles for (alternating) tangle learning (TL, ATL)

Table <ref> shows that the relevant statistic doubles with each higher number of bits, which supports that the runtime is exponential in the number of bits.
The number of non-dominion tangles for ATL and TL is the same as the number of promotions for RR and RRDP,
namely
2×(2^N-1) tangles
to set all bits.
Since the number of vertices and edges increases quadratically,
we conclude that the Two Counters games provide an exponential lower bound to these algorithms, namely Ω(2^√(n)).
We also investigated whether inflation and compression <cit.> had any effect and this was not the case.

In Section <ref>,
we take a closer look at how these algorithms solve the Two Counters games,
and sketch an inductive proof that the algorithms require exponentially many steps for higher N.






§ ANALYSIS




We study how the three algorithms solve a Two Counters game by looking at the timeline of events obtained from the trace output of the solver.
We then sketch a proof arguing that any N-bit Two Counters game requires 2^N many steps for the three algorithms. 











 §.§ Recursive algorithm


As argued in Section <ref>,
to make the recursive algorithm take exponential time,
we need distractions such that after a “higher” distraction is attracted, all “lower” distractions must be attracted again.
First, we use the trace output of Oink to obtain a timeline of identified distractions using the command line :




4, 3, 4, 2, 4, 3, 4, 1, 4, 3, 4, 2, 4, 3, 4, 0, 4, 3, 4, 2, 4, 3, 4, 1, 4, 3, 4, 2, 4, 3, 4



We can also draw this timeline as a tree, which is an abstraction of the recursive call graph:


























































[
	distree/.style = align=center, inner sep=2pt, text centered, draw=none, minimum width=0.5em,
	level 1/.style=sibling distance=8cm,
	level 2/.style=sibling distance=3.9cm, 
	level 3/.style=sibling distance=1.9cm, 
	level 4/.style=sibling distance=0.75cm,
	level/.style=level distance = 0.6cm,
	every node/.style=distree] 
	l_1(0)
		child node l_1(1) 
			child node l_1(2) 
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)  
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)   
			child node l_1(2) 
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)  
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)    
		child node l_1(1) 
			child node l_1(2) 
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)  
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)   
			child node l_1(2) 
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)  
				child node l_1(3) 
					child node l_1(4) 
					child node l_1(4)     ;
	




From the above, it is at least clear that the algorithm
behaves as expected for the 5-bit Two Counters game.



We now sketch a proof that the recursive algorithm requires exponential time for all Two Counters games.



The recursive algorithm follows the progression of a binary counter when solving a Two Counters game.


	We follow the progression of the odd bits.
	In the initial recursive decomposition, each h vertex attracts no vertices and each l vertex attracts the connected vertices of lower bits and distracts connected z vertices.
	Since no l vertex is itself attracted, all distractions are unattracted and thus are the bits unset.
	
	Because of its strict recursive structure, the recursive algorithm cannot attract and identify a higher distraction before all lower distractions.

	After removing an even distraction, Even attracts the entire subgame except the tangle of the corresponding bit of Odd. The reason for this is that the even bit l is now good-for-Even, while odd bit l is not yet good-for-Odd, so all lower bits are trivially attracted to the even region.
	For example, in Fig. <ref>, after attracting the distraction with priority 7 (in bit 0 of Even), vertices 7 and 8 are good for Even, and all lower vertices are now attracted to the even region, except the tangle of the odd bit.
	Hence, after removing the corresponding odd distraction, the set B (line 6 of Alg. <ref>) consists exactly of the odd tangle, the attracted distraction and the directly connected lower vertices.
	That is, all the lower distractions are in the subgame that is recomputed and are distracting again.
	Thus, setting higher bits resets the lower bits.
	
	We have established that the counter starts with all bits unset, that setting higher bits resets all lower bits, and that higher bits are not set before the lower bits are set.
	Therefore the recursive algorithm follows the progression of a binary counter.

Notice that in the above proof, because of the strict recursive nature,
we do not need to distract z to make the recursive algorithm wait until all lower bits are set before setting a higher bit.


In fact, removing the edges from z vertices to lower distractions results in even more recursive calls.
Priority promotion and tangle learning 
are not bound to a strict order like the recursive algorithm.

	
	
	
	








































































 §.§ Priority promotion


In priority promotion, a bit is set when the region of tangle vertex t is closed,
promotes to a higher region and attracts the distraction l.
When solving the 3-bit TC game with the delayed promotion policy, the command line  gives us the following sequence of promotions:

 to X[0.3]X[1.2]X[1.2]X[1.1c]X[1c]X[1.5c]X[1.5c]
    Promotion     Bit     2cCounter state (DP)     Delayed     Recovered 

                                even       odd          (in DP/RRDP)               (in RR/RRDP)   

1      2 to 6       Even 2      001         000                            

2      1 to 5       Odd 2       001         001                            

3      2 to 8       Even 1      011         000        yes                 

4      1 to 7       Odd 1       010         010                            

5      2 to 8       Even 2      011         000        yes                 

6      1 to 7       Odd 1                         011         010                        yes 

7      1 to 7       Odd 2       011         011                            

8      2 to 14      Even 0      111         000        yes                 

9      1 to 15      Odd 0       000         100                            

10     2 to 14      Even 0                        100         100                        yes 

11     2 to 6       Even 2      101         100                            

12     1 to 5       Odd 2       101         101                            

13     2 to 14      Even 1      111         100        yes                 

14     1 to 15      Odd 1       000         110                            

15     2 to 14      Even 0                        100         110                        yes 

16     2 to 14      Even 1                        110         110                        yes 

17     2 to 14      Even 2      111         110                            

18     1 to 15      Odd 2       111         111                            



We record the state of the two counters after each promotion with the DP solver.




The “recovered” promotions do not occur in the RR and RRDP algorithms, as their regions are recovered.
All delayed promotions are immediately applied,
because after delaying the promotion, no normal promotion is available.
Thus the delayed promotion policy is not useful here.

Region recovery is however useful, as was already clear from Table <ref>.
Both PP and DP (based on PP+) perform additional promotions that are not necessary with region recovery.
For the 3-bit TC game, PP requires 23 promotions, DP requires 18 promotions, RR requires 14 promotions and RRDP requires 14 promotions.



Priority promotion follows the progression of a binary counter when solving a Two Counters game.


Similar to the proof of Lemma <ref>.
Initially no distractions are attracted by their opponent, so the counters start with 0.
Whenever a higher bit is reset, the PP and PP+ policies reset all lower bits of the other player and the RR algorithm cannot recover because the earlier strategy leaves the remaining subgame.
Due to the interleaving, setting odd bits resets lower even bits and vice versa.
Therefore higher bits reset lower bits.
Notice that the region of a distraction cannot be closed.
Therefore as long as a distraction is not attracted, all vertices z from the higher bits are distracted and cannot be part of a tangle until the distraction is attracted.
Thus high bits wait for lower bits.
From this follows Lemma <ref>.




 §.§ APT


See <cit.> for a description of the APT algorithm and the source code of Oink <cit.> for an efficient implementation in a single loop.
The APT algorithm is described as a nested fixed point computation that refines “Avoiding” and “Visiting” sets.
These two sets essentially encode the current knowledge of whether vertices with an odd priority are winning for odd and vertices with an even priority are winning for even, that is, whether vertices are distractions.
Initially no vertex is considered a distraction.
Each time some vertices of priority p are now considered a distraction, all vertices with a lower priority than p are reset.
We look at the trace of how often the algorithm determines that a distraction in the 3-bit TC game must be avoided.
This happens 31× in the following sequence:

 to X[10c]X[c]X[10c]X[c]X[2c]X[c]
		i_1(2)     ⇒    i_0(2)     ⇒    i_1(2)     ⇒

		i_1(1) ⇒i_1(2)     ⇒    i_0(1)⇒i_0(2)     ⇒    i_1(1)     ⇒

		i_1(2)     ⇒    i_0(2)     ⇒    i_1(2)     ⇒

		i_1(0) ⇒i_1(2)⇒i_1(1)⇒i_1(2)     ⇒    i_0(0)⇒i_0(2)⇒i_0(1)⇒i_0(2)     ⇒    i_1(0)     ⇒

		i_1(2)     ⇒    i_0(2)     ⇒    i_1(2)     ⇒

		i_1(1)⇒i_1(2)     ⇒    i_0(1)⇒i_0(2)     ⇒    i_1(1)     ⇒

		i_1(2)     ⇒    i_0(2)     ⇒    i_1(2) 

	

This is clearly similar to the timeline of the recursive algorithm. 




 §.§ Tangle learning


We already explained in Section <ref> why tangle learning follows the progression of the counters,
as the counters are designed to cause tangle learning to learn all tangles in all bits.
We see that it works as expected via the command line  which yields precisely the expected tangles:


Even 4, Odd 4, Even 3, Odd 3, Even 4, Odd 4, Even 2, Odd 2, Even 4, Odd 4, Even 3, Odd 3, Even 4, Odd 4, 
Even 1, Odd 1,
Even 4, Odd 4, Even 3, Odd 3, Even 4, …





 §.§ Other algorithms


We also considered the fixpoint algorithms <cit.>, the small progress measures algorithm <cit.>, and the two quasi-polynomial algorithms, ordered progress measures <cit.> and succinct progress measures <cit.>.

The fixpoint algorithms require exponential time as they are essentially myopic versions of the recursive algorithm, based on a one-step attractor instead of full attractors.
The other algorithms are certainly slow and appear to require lifting vertices across the entire available range, but this is not due to the design of the Two Counters games.
Rather, these algorithms tend to be extremely slow even for trivial games like winning self-loops.
The exception is in fact strategy iteration <cit.>, which is the only algorithm that can quickly and in polynomial time solve the Two Counters games.

The Two Counters games are difficult for attractor-based algorithms for the simple reason that player α prefers to play to the distractions of the opponent's counters as these have the highest value for the player.
As soon as the player decides to play from z to t, the tangle is learned.
Algorithms using progress measures and the strategy iteration algorithm assign a higher value to vertex t as soon as there is a path to t from z, because vertices with α's priority along the path receive a progressively higher value.
Thus the players are not distracted very long by the distractions.




























§ DISCUSSION




Since solving parity games is known to lie in UP∩co-UP, it is
widely believed to admit a polynomial solution.
Researchers have been studying this problem for several decades.
For some time, the focus was on variations of strategy iteration algorithms,
where a suitable improvement rule could lead to a polynomial solution.
Friedmann et al. provided superpolynomial or exponential lower bounds for many of such rules <cit.>,
as well as Fearnley and Savani recently <cit.>.

For a long time, the main attractor-based algorithm was the recursive algorithm by McNaughton <cit.> and Zielonka <cit.>, for which Friedmann also showed an exponential lower bound <cit.> and which Gazda and Willemse <cit.> later improved upon.
These lower bounds resist techniques like inflation, compression and SCC decomposition. 
As the lower bound of Friedmann can be defeated by memoization, since the number of distinct subgames is polynomial, Benerecetti et al. proposed a more resilient lower bound <cit.>. 
Their priority promotion algorithm <cit.> solves <cit.> in polynomial time, although this requires inflation for <cit.>.
For priority promotion, two exponential lower bounds have been presented <cit.>.
However for variations of priority promotion, in particular for DP <cit.>, no superpolynomial lower bound has been published.
Tangle learning <cit.> solves all these lower bound examples in polynomial time.

We presented the parameterized Two Counters game
and showed that this provides an exponential lower bound for
the recursive algorithm,
for (all variations of) priority promotion, in particular with the
delayed promotion policy,
and for tangle learning.
An N-bit Two Counters game has size n=3N^2+5N and requires at least 2×(2^N-1) steps, thus providing a lower bound of Ω(2^√(n)).









The Two Counters game is available online via <https://www.github.com/trolando/oink>.



§ ACKNOWLEDGEMENTS


We thank Veronika Loitzenbauer for the helpful discussions on these and other difficult parity games.
We also thank Marcin Jurdziński, Ranko Lazić, Laure Daviaud and Laurent Doyen for their hospitality and discussions.
Finally, we thank Armin Biere for generously supporting this research.




eptcs


