On-the-fly and partial solving
merc_vpg's symbolic solver is based on the paper:
Maurice Laveaux, Wieger Wesselink, Tim A.C. Willemse, On-The-Fly Solving for Symbolic Parity Games, TACAS 2022, LNCS 13244, pp. 137-155, DOI
A game explored on the fly never presents the solver with a complete graph: states and their successors are generated on demand, so at any point only a partial graph is available, where is the set of vertices reached but not yet expanded — each may still turn out to have successors nobody has seen yet. The four partial solvers below are not a speed-up bolted onto a finished graph; they are how vertices get decided during exploration, from whatever partial graph exists at the moment they run. A vertex either solver declares won stays won under every possible future expansion of (that soundness guarantee is Theorem 1 below), so exploration can stop the moment the vertex the caller actually cares about — typically the initial vertex — is decided, however small a fragment of the full game that took.
This page derives the four solvers from the paper's definitions and lemmas
and explains how they fit together. It assumes familiarity with
Zielonka's algorithm on symbolic parity games and does not
restate it. Every construction below is given directly in its safe form —
folding into every control-predecessor and attractor computation, per
§4.1 of the paper — since that is the form actually used while exploring;
each derivation marks with a // safety: … comment the one place this
folding happens.
safe_α: the α-safe vertex set
Definition 4. For :
i.e. remove the -attractor of 's own incomplete vertices — exactly the vertices from which could force play toward an incomplete vertex she owns, which is where a not-yet-discovered edge could later hand her an escape. Theorem 1 shows this is the largest such set: solving inside it is sound against every future extension of (Lemma 1), and any dominion reaching outside it is not (Lemma 2/Corollary 1).
safe_vertices ports this with one addition beyond the literal formula:
The extra sinks(incomplete, v) term seeds the opponent's attractor with
every structural sink of incomplete too, not only the opponent-owned
incomplete vertices Definition 4 literally names. An unexplored vertex has no
discovered successors yet regardless of who owns it, so without this term an
alpha-owned incomplete vertex with no known outgoing edges could stay
inside the returned safe set — and partial_solve, the one solver that runs
a plain zielonka over this set (below), assumes totality. The extra term is
what keeps the safe subgame actually total whenever incomplete is
non-empty; mCRL2's own compute_safe_vertices does the same for the same
reason, so this is not a merc-specific strengthening of Definition 4, just
its operational form.
The safe attractor: spre_α and SAttr_α
Computing (an extra full attractor fixed point) is only worth
doing when a solver actually needs the subgame itself, as partial_solve
does. The other three solvers below only ever need attractors, never the
subgame, so §4.1 gives them a safe control-predecessor that folds the
incomplete set directly into instead, without ever
materialising :
Lemma 3 shows agrees with the ordinary computed inside the safe subgame for any ; Lemma 4 lifts this to the whole fixed point: . This equality is what lets every solver below use freely in place of and stay just as sound as if it had first restricted itself to .
control_predecessors and attractor implement
directly, with incomplete threaded through as an ordinary parameter — the
one line in each that differs from plain is
marked:
With incomplete = ∅ the marked line vanishes and this is exactly plain
— safe_vertices above calls it that way on
purpose, since Definition 4 wants the ordinary attractor, not the safe one.
compute_total_graph's two calls to attractor (one per player, over the
already-resolved winning sets) and monotone_attractor's inner loop
(below) both go through this same pair of functions with the real
incomplete set.
Two things the paper calls "safe"
The paper uses "safe" for two related but distinct constructions, and the ambiguity is inherited from it, not a documentation accident:
- the -safe vertex set (Definition 4,
safe_vertices) — a subgame, a subset of , obtained by one extra attractor fixed point; - the safe control predecessor/attractor (§4.1, ,
control_predecessors/attractorabove) — folding into every step so that no subgame ever needs to be materialised.
Lemma 4 is what makes the choice between them purely about what a given
solver already needs, not a soundness trade-off: partial_solve below hands
a plain, unrestricted zielonka an entire subgame to work on, so it needs
materialised regardless and uses the first form directly; the
three cycle/attractor solvers after it never need anything but attractors, so
they use and skip the extra fixed point
entirely.
partial_solve
Port of mCRL2's partial_solve. This is the entry point that actually drives
solving on the fly: it is called again after each round of exploration
shrinks incomplete, and returns as soon as initial_vertex is decided —
at which point exploration itself can stop, whatever fraction of the game
remains unexplored. Internally it runs a plain zielonka restricted to each
player's own safe subgame in turn:
zielonka here is called on safe_even/safe_odd directly — no
involved, since safety was already spent building the safe
subgame itself, per the previous section; the recursion inside runs exactly
as in Zielonka's algorithm, unmodified.
detect_solitair_cycles
A solitaire cycle is a set , entirely owned by one player , at 's own priority parity, where every vertex has an edge staying inside — so can simply loop forever inside it, winning it outright with no attractor reasoning needed at all (Proposition 1: unconditionally, and the fixed point uses only plain ):
detect_solitair_cycles:
The cycle search itself never asks who controls anything — a solitaire cycle
is entirely 's own vertices at her own priority, so there is no
adversary move to account for, and plain suffices. Safety
enters exactly once, in accept_cycle (shared with detect_forced_cycles
below), which records as won (with an overapproximate merge(U, U)
strategy, later cut down to real edges by apply_strategy) and closes it off
with a safe attractor:
detect_forced_cycles
Generalises solitaire cycles to mixed-owner cycles: may include -owned vertices too, as long as has no edge that escapes from any of them — her "choice" to leave is illusory, so the whole cycle is still won by . The direct construction restricts to the safe subgame explicitly:
and Proposition 2 gives a -based reformulation that never needs materialised at all:
detect_forced_cycles implements the right-hand side directly — the form
that avoids the subgame — through control_predecessors_within
(control_predecessors with outside = v \ u):
By Proposition 2 this reaches the same that restricting to and using plain would; it just never pays for to get there.
detect_fatal_attractors
Fatal attractors (Huth, Kuo, Piterman, FOSSACS 2013) find, for each priority , a set of priority- vertices that (the player owning priority ) can always force play back into — winning the whole attractor into that set. The monotone control predecessor restricts candidates to priorities no more significant than ( under the paper's min-parity, under merc's max-parity):
and, again via the safe-attractor mechanism (Proposition 3):
detect_fatal_attractors implements :
become monotone_attractor, which folds incomplete into its inner
control_predecessors call exactly as attractor does above:
and loops over priorities in ascending order — merc's mirror of the paper's descending, least-to-most-significant loop — running for each the // fixed point that finds a fatal attractor at that priority or concludes there isn't one:
Unlike the other three solvers, this one accumulates no strategy across iterations at all: a vertex can belong to fatal attractors at different priorities on different outer-loop iterations before it is finally claimed, and no attempt is made to reconcile that history into one strategy.