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博弈因其实际重要性及不动点定义涉及最大不动点与最小不动点交替的特征，成为特别值得关注的情形。我们证明，在精确意义上，半环语义提供了所有吸收主导策略（即最小成本获胜的策略）的信息，并探讨了此类策略与位置策略及更具通用性的持久策略之间的关系。这些信息可用于游戏合成、确定改变博弈结果所需的最小修改量等实际应用。最后，我们讨论了该方法的局限性，并提出了半环语义无法直接回答的问题。