Skip to content

Can the workflow keep running sensibly forever? (parity and mean-payoff games)

A workflow such as an incident run-book never really ends: alerts keep arriving, the machine keeps moving between states. Before any decision is made, the library asks two questions about the machine itself: is there a way to keep running forever that never settles into a state you marked as "must not stay here", and is there a way to run forever whose long-run reward is not negative? This page explains how those two questions are answered (as small games on the policy's graph), what the answers actually guarantee, and what the check assumes about who chooses the next event.

It assumes you know what a policy's states and events are (see Write a policy). The plain-language version of this check is Progress. Symbols and trust levels are explained in How to read these pages.

The question and the product situation

The incident_response example has four states:

  • watch: nothing happening (the start);
  • mitigating: proposes mitigate;
  • paging: proposes page_oncall (waking a human has a cost);
  • resolved: proposes close.

Events move between them: alert goes from watch or resolved to mitigating; still_bad escalates to paging; ack returns to mitigating; clear goes to resolved.

Each state carries two numbers that you choose:

  • a priority, a small whole number. An odd priority marks a state the workflow must not stay in forever; an even priority marks one it may. When several states are visited forever, the largest priority among them decides.
  • a payoff, a reward per step spent there (negative for costly states).

The question the game check answers: from the start state, can the workflow run forever so that the largest priority it keeps returning to is even, and so that its average payoff is at least zero?

Intuition: a token moving on a graph

Put a token on the start state. Each step, the token follows one edge. An infinite run is a "play". Two outcomes are scored:

  • Parity. Look at the states visited infinitely often. If the largest priority among them is even, the controller (the side choosing moves) wins the play; if odd, it loses.
  • Mean payoff. Average the edge weights along the play. The controller wants that average to be at least 0.

In this library the controller is the service: it chooses the next event in every state, except in states marked environment=True, where an adversarial environment (a customer, a pager) chooses. The token can only follow arrows the policy draws; a state with no arrow out (a final state) gets a self-loop, so the play stays finished there.

Here is the incident graph as the library compiles it. Each edge shows the event and its weight (the target state's payoff, since this chart gives transitions no payoff of their own). Every state has an arrow out, so there are no self-loops.

graph LR
    W["watch<br/>priority 0, payoff 0"] -- "alert / 1.0" --> M["mitigating<br/>priority 0, payoff 1"]
    M -- "still_bad / -0.2" --> P["paging<br/>priority 2, payoff -0.2"]
    P -- "ack / 1.0" --> M
    M -- "clear / 2.0" --> R["resolved<br/>priority 0, payoff 2"]
    R -- "alert / 1.0" --> M

All priorities are even, so every play is a parity win. The best average payoff comes from cycling between mitigating and resolved: \((2.0 + 1.0)/2 = 1.5\).

Worked example from the code

Run the example:

uv run grounded-decision examples incident_response

Every decision in its output shows the game check passing:

         game             PASS  can the policy keep making progress (parity win, nonnegative mean)?

The numbers behind that line, from compiling the chart with grounded_decision.statechart.game.compile_game(incident_response.build().chart) and running the two solvers:

Quantity Value
states watch, mitigating, paging, resolved
priorities 0, 0, 2, 0
controller wins parity from each state (even_wins) True, True, True, True
best long-run average payoff from start (max_mean_payoff) 1.5

The check is solved once, when the Module is built, and every decision record repeats the cached result in the game check (metrics.parity_win, metrics.nonnegative_mean).

Now small charts that show what does and does not fail (built with Statechart(...) and solved the same way):

Chart Priorities Best average payoff Parity win from start Check
waiting ⇄ stuck on tick, both priority 1 1, 1 0.0 False fails
polling ⇄ retry on fail, payoffs −1.0 and −0.5 0, 0 −0.75 True fails
polling ⇄ retrying on timeout; closed exists but nothing leads to it 0, 0, 0 0.0 True passes
the same, with polling and retrying marked priority 1 1, 1, 0 0.0 False fails

The third row matters: a retry loop that can never reach close passes when its author leaves every priority at 0, because then every loop is "acceptable". Marking the loop's states odd (fourth row) makes the check catch it.

Text policies get their priorities from the policy itself: states that propose an action, and final states, get 2; all others get 1. The workflow_liveness policy (test(submit) ; (test(approve) ; act(provision) | test(reject) ; act(close)))* compiles to s0, s2 (priority 1) and s3 (provision), s4 (close) (priority 2); every cycle passes through an action state, so parity win is True. A policy that can loop without proposing anything, such as (test(ping))*, fails. An event that arrives out of order (an approve before any submit) has no arrow, so the entity stays where it is and nothing is proposed; there is no dead state for it to fall into.

The precise statement

Parity games and Zielonka's algorithm

A parity game is a directed graph whose vertices are split between two players, Even and Odd, with a priority \(\mathrm{pr}(v) \in \mathbb{N}\) on each vertex. The owner of a vertex chooses the next edge. A play \(v_0 v_1 v_2 \dots\) is won by Even iff

\[ \max \{\, \mathrm{pr}(v) : v \text{ occurs infinitely often in the play} \,\} \text{ is even.} \]

Even wins from \(v\) if Even has a strategy that wins every play starting at \(v\), whatever Odd does. Parity games are determined: every vertex is won by exactly one player.

Zielonka's recursive algorithm (1998) computes both winning regions. On a vertex set \(V\):

  1. Let \(p\) be the largest priority in \(V\), and let the favoured player be Even if \(p\) is even, Odd otherwise.
  2. Let \(A\) be the favoured player's attractor of the vertices with priority \(p\): every vertex from which that player can force the token into that set (a vertex joins if its owner is the favoured player and some edge leads into the set, or its owner is the opponent and every edge does).
  3. Solve the game on \(V \setminus A\) recursively.
  4. If the other player wins nowhere in \(V \setminus A\), the favoured player wins all of \(V\): it can keep returning to priority \(p\).
  5. Otherwise, let \(B\) be the other player's attractor of its winning region in \(V \setminus A\). The other player wins \(B\). Solve \(V \setminus B\) recursively; the favoured player wins what it wins there, and the other player wins the rest plus \(B\).

The algorithm is exponential in the worst case. The best known algorithms run in quasipolynomial time (Calude, Jain, Khoussainov, Li and Stephan, 2017); whether parity games are solvable in polynomial time is open.

One-player case. If Even owns every vertex, Even wins from \(v\) iff some path from \(v\) reaches a cycle whose largest priority is even.

Mean-payoff games and Karp's algorithm

With an edge weight \(w(e)\), the mean payoff of a play is \(\liminf_{n\to\infty} \frac{1}{n}\sum_{i<n} w(e_i)\). When one player owns every vertex, the best achievable mean payoff from the start \(s\) is the largest mean weight of a cycle reachable from \(s\). Karp's algorithm (1978) computes it exactly: let \(D_k(v)\) be the largest weight of a walk of exactly \(k\) edges from \(s\) to \(v\), with \(n = \lvert V\rvert\); then

[ \lambda^{*} = \max_{v} \; \min_{0 \le k < n} \frac{D_n(v) - D_k(v)}{n - k}, ]

in \(O(n \cdot \lvert E\rvert)\) time. For two-player mean-payoff games, pseudo-polynomial and randomized subexponential algorithms are known; whether they can be solved in polynomial time is open.

What is known, and what the catalog claims

Where this result stands

In the wider literature: Zielonka's algorithm and Karp's minimum/maximum mean-cycle algorithm are classical and correct. Parity games are solvable in quasipolynomial time (2017); polynomial time is open for both parity and mean-payoff games. A tropical-elimination step proposed by Truffet for two-player mean-payoff games has been discussed as an optimisation.

In this project's math catalog (result 104): the manuscripts claim deterministic quasipolynomial-time algorithms for mean-payoff games and related stochastic and parity variants. The Lean statement (see in the companion math catalog, kept outside this repository) covers two narrower things: a finite counterexample showing a two-step run of Truffet's elimination ends feasible but not optimal, and a randomized quasipolynomial algorithm for the zero-threshold winning set of mean-payoff games.

What this library relies on: only the classical algorithms (Zielonka for two-player parity, Karp for one-player mean payoff), on charts of at most 200 states. It never runs Truffet's step (that is the "Truffet ban" pinned as REF_TRUFFET_BAN). It does not use the catalog's quasipolynomial claims. See Where each result stands.

What the code does, and how it differs from the theory

compile_game(chart, limits) turns a statechart into a game:

  • one vertex per state, with that state's priority (0 by default on a hand-built chart; 2 or 1 on a text policy, as above);
  • one edge per transition, weighted by the transition's payoff plus the target state's payoff (both default 0);
  • one _final self-loop on each vertex with no outgoing transition, weighted by that state's payoff;
  • each vertex owned by the controller (Even), except states marked environment=True, which the environment (Odd) owns.

Module then computes, once at construction:

  • parity_win: does Even win from the start? (statechart/parity.py, standard Zielonka as above);
  • nonnegative_mean: is the best reachable cycle mean \(\ge -10^{-12}\)? (statechart/mean_payoff.py, Karp).

The game check on every decision passes iff both are true.

What the check assumes

  • The service sends the right event in its own states. In a service-owned state, the check assumes the service picks the arrow that keeps the workflow progressing. If nobody ever sends give_up, a retry loop with a give_up exit still retries forever. Mark states the service does not control as environment=True.
  • The payoff part is best-case. Karp's algorithm is one-player: it ignores owners and reports the best reachable cycle mean, even through environment-owned states.
  • Hand-built priorities are yours. A chart left at priority 0 everywhere passes the parity part whatever its shape (third row above). Give odd priorities to the states the workflow must not circle in forever.
  • An action that can never be proposed is not detected. The check asks whether progress is possible, not whether every action is reachable.

Other differences from the textbook setting:

  • Parity and mean payoff are checked separately. Different plays may satisfy the two conditions; no single play is certified to satisfy both. The catalog's "mean payoff conjoined with parity" objective is not computed.
  • Two players for parity, one for payoff. Environment-owned states make the parity part a genuine two-player game; the payoff part remains one-player (best case).
  • Size and depth caps. More than Limits.max_game_vertices (200) states raises GameTooLarge; Zielonka recursion deeper than Limits.max_parity_depth (64) raises ParityUnsolved. Recursion depth can grow with the number of vertices, not just the number of distinct priorities. In either case both flags are false and every decision abstains, with the error text in the game summary.
  • Trust tag. The game check reports trust=lean when it passes and operational when it fails. lean here names catalog result 104 as the pinned reference; the library does not run Lean, and the algorithms it uses are the classical ones.
  • Not re-solved. If you change a statechart after building the Module, the cached answer is stale. Build a new module.

Health.game_solved reports only the parity bit. Read channels[game].metrics for both.

Limits, and how to choose priorities and payoffs

A pass means the workflow can keep making progress from its start, given the priorities, owners and payoffs you set. It is not a test of your workflow's behaviour; step the module through every expected event sequence in a unit test as well, as tests/test_runtime.py does.

How to annotate a hand-built chart:

You want to say Set Effect on the check
"Coming back here forever is fine" even priority (0, 2), payoff \(\ge 0\) Loops through it are acceptable
"Never circle here forever" odd priority (1, 3, …) Fails if the service cannot force every run out of loops whose largest priority is odd
"Someone else picks the next event here" environment=True The parity part assumes the worst choice in this state
"Staying here is costly" negative payoff Fails only if every reachable cycle averages below 0
"Escalating is legal but expensive" (paging in the example) even priority, small negative payoff Never fails on its own

A chart larger than 200 states abstains on every decision. Split it or raise max_game_vertices (and max_karp_vertices) deliberately; see Choose parameters.

What a pass does not establish: that every action is reachable, that the service will in fact send the events that make progress, or anything about the evidence. The game check never looks at the evidence snapshot; an incident_response decision on weak evidence still has a passing game check and abstains for the evidence reasons.