Motivation

A parity game is a finite graph game in which two players choose an infinite walk and the largest priority recurring on the walk determines the winner. Such games supply algorithmic tasks in verification. An algorithm may solve many practical instances quickly and still require many updates on a deliberately constructed family. This mission concerns the number of updates made by two specified strategy-improvement rules. It formalizes a known lower-bound result, rather than asking whether parity games themselves have polynomial-time algorithms. The source is Friedmann's 2011 journal treatment, extending his LICS 2009 work.

Setting

The formal model uses finite vertex sets, a total directed edge relation, an owner for each vertex, and distinct natural-number priorities. Player 0 is encoded by false; player 1 is encoded by true. A positional strategy chooses one legal successor at each vertex owned by that player. Its values at other vertices are ignored.

Two strategies and a starting vertex determine an eventually periodic walk. Its valuation has three components: the largest recurring priority, the set of more important vertices preceding the first visit to its dominating cycle vertex, and the number of steps before that visit. The cycle component is compared first. For equal cycle components, the largest priority in the symmetric difference of the two path sets decides their ordering, with an even priority favorable to player 0. A remaining length comparison favors a shorter route to an even cycle and a longer route to an odd cycle. The valuation of one player-0 strategy at a vertex is the minimum over actual legal player-1 replies.

A local update chooses a successor with greatest current valuation at every player-0 vertex. A global update chooses a strategy with greatest resulting valuations among strategies allowed by the current improvement arena. Every active update must contain a strict improvement. A complete execution starts at its stated initial strategy, performs improving updates, and stops precisely when no improving switch remains. Its cost counts updates, excluding the initial strategy.

Formalization targets

The goal includes the two parity-game rules and their payoff-game counterparts. For each rule the required family has a constant $C>0$, independent of its parameter $n$, such that

$$|E_n|\le Cn,\qquad T_n\ge 2^n\quad(n>0).$$

For parity games the priorities are also bounded by $Cn$. An instance must admit a complete execution, and every complete execution respecting the stated rule must meet the lower bound. This explicitly prevents a universal claim about executions from becoming true merely because no execution exists. The two rules may use different hard families.

Supporting targets cover simultaneous optimal counterstrategies, strict improvement, extraction of both winning regions at termination, the local-rule lower bound, binary-outdegree refinements, discounted payoff equations, comparison preservation under reduction, and absorption values for stopping stochastic games. Discounted and stochastic lower bounds are separate supporting results within this paper's mission. Mean-payoff policy iteration is represented through the paper's specified reduction to discounted games.

Significance

The requested artifact is a reusable formal interface for constructing and analyzing long algorithm executions. It exposes the improvement arena, counterstrategy minimization, strictness of updates, termination condition, and cost model. Subsequent constructions can use those interfaces without encoding their own meaning of an iteration.

The mathematical lower bounds are already published. The open items here are proof obligations for these explicit Lean models. Successful elaboration checks the declarations' types; it does not prove the lower bounds or establish that the definitions match the paper. The goal needs actual witness games and initial strategies, together with execution analysis. Neither a structure field assuming a long run nor a hypothesis asserting the desired growth can discharge it.

Difficulty

A large number of possible strategies does not establish that an algorithm visits them. The lower-bound obligation concerns the updates actually permitted by the selected rule and their stopping condition. Global updates additionally compare the resulting valuations of complete successor strategies, so a definition based only on locally greatest current values would describe a different rule. Equal-valued choices also need care: the target ranges over every complete execution admitted by its relation.

Counterstrategy minima are constrained by legal replies. Their existence, the validity of the ultimately periodic valuation, and the connection between non-improvability and winning regions remain mathematical proof obligations. The payoff models add matrix nonsingularity and the interpretation of rational equation solutions.

Formalization scope

Game size means edge count. It does not mean binary coefficient encoding length. The parity targets retain the linear-edge refinement in the source's Section 7 and the corresponding global-rule refinement in Section 8; the basic quadratic-edge drawings alone are insufficient for that stated size bound. The goal states existence of hard families, leaving their construction to the proof. It does not transcribe the source's specific vertex-label tables as unchecked constants.

Discounted games use rational rewards and a rational discount strictly between zero and one. For fixed strategies, values are defined by the exact rational inverse of $I-\beta P$. The associated milestone requires the unique discounted Bellman solution. The mean-payoff target explicitly uses rewards $(-|V|)^{\Omega(v)}$ and the specified near-one discount. It does not replace the source algorithm with an update based only on raw mean rewards, which the source warns can stall.

Stopping stochastic games have separate Max, Min and random vertices, two distinct terminals, nonnegative rational transition probabilities with row sum one, and a positive-probability route to a terminal from each state under every legal strategy pair. Values solve the finite absorption equations. The model allows arbitrary random probabilities and outdegrees, as in the source's treatment. The matrix and counterstrategy definitions are shared infrastructure; none contains an unproved lower-bound assertion.

Selected references

• Oliver Friedmann, An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms, Logical Methods in Computer Science, 2011. Author PDF, arXiv version.
• Oliver Friedmann, An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it, LICS, 2009. Author PDF.