This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in B\"uchi 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\"uchi 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.

翻译：本文针对Büchi博弈中的策略分析问题，展示了半环语义在不动点公式中的应用案例研究。半环语义通过允许来自特定半环的多真值，推广了经典的布尔语义。在适当的多项式半环中对定义博弈获胜区域的不动点公式进行求值，不仅能提供谁获胜的布尔信息，还能揭示其获胜方式及可能采用的策略。这一方法在可达性博弈中已得到充分理解——其获胜区域可定义为最小不动点。Büchi博弈案例尤为特殊：不仅因其实际重要性，更因其不动点定义涉及真正的最优不动点与最小不动点交替——这是最简单的此类情形。我们精确证明：半环语义能提供关于所有吸收主导策略（以最小代价获胜的策略）的完备信息，并讨论这些策略与位置策略及更广义的持久策略之间的关系。该信息可支撑博弈综合、最小修改博弈以改变结果等应用。最后，我们讨论本方法的局限性，并提出半环语义无法直接回答的若干问题。