Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials

TL;DR

This paper investigates semiring semantics for fixed-point logic as a tool to analyze strategies in Büchi games, extending Boolean winning information with provenance-like detail. By employing absorptive, fully-continuous semirings, notably the universal absorptive polynomial semiring ${f S}^{\infty}[X]$ and dual-indeterminates, it proves a Sum-of-Strategies Theorem tying the valuation of the Büchi win formula to the sum of valuations of all absorption-dominant winning strategies. The approach yields concrete, actionable insights: it identifies edge usage patterns, counts positional strategies, and supports minimal repairs and target synthesis from a fixed Büchi game, albeit with limitations for cost-related questions. The work highlights a flexible framework for strategy analysis and suggests extensions to parity games, while acknowledging cases where semiring-based cost computations may be ill-suited or require alternative algebraic structures. Overall, the method provides a compact, expressive lens on why strategies work and how they could be altered, with practical implications for synthesis and repair of reactive systems.

Abstract

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth values from certain semirings. Evaluating the fixed-point formula that defines the winning region in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. This is well-understood for reachability games, where the winning region is definable as a least fixed point. The case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the fixed-point definition involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies -- strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables applications such as game synthesis or determining minimal modifications to the game needed to change its outcome. Lastly, we discuss limitations of our approach and present questions that cannot be immediately answered by semiring semantics.

Figures (4)

• Figure 1: Running example of a Büchi game and a winning strategy.
• Figure 2: Venn diagram depicting various classes of winning strategies.
• Figure 3: Semiring interpretations used in this paper (the notation $a/0$ indicates the value $a$ if the literal is true, and $0$ if it is false in $\mathcal{G}$).
• Figure 4: Illustration of the model-checking game $\mathsf{MC}(\mathcal{G},v_i)$ for a Büchi game with positions $V = \{v_1,\dots,v_n\}$. Rounded nodes belong to Verifier, rectangular nodes to Falsifier. Nodes without border are terminal positions representing literals, dashed nodes are target positions.

Theorems & Definitions (43)

• Definition 2.1
• Definition 2.2
• Example 2.3
• Definition 3.1
• Example 3.2
• Definition 3.3
• Example 3.4
• Proposition 3.5
• proof
• Lemma 3.6