Büchi 博弈的半环溯源：基于吸收多项式的策略分析
Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials
AI总结：
本文将半环语义应用于 Büchi 博弈策略分析，利用吸收多项式揭示所有吸收占优策略及其与位置策略、持久策略的关系，支持博弈综合与最小修改等应用。
摘要：
本文展示了一个案例研究，探讨将不动点公式的半环语义应用于 Büchi 博弈中的策略分析。半环语义通过允许来自特定半环的多个真值，推广了经典的布尔语义。在适当的多项式半环中对定义给定博弈中获胜区域的不动点公式进行求值，不仅能提供关于谁获胜的布尔信息，还能告诉我们他们如何获胜以及可能使用哪些策略。这一点在可达性博弈中已得到充分理解，其中获胜区域可定义为一个最小不动点。Büchi 博弈的情形尤其值得关注，不仅因为其实际重要性，还因为它是固定点定义涉及最大不动点与最小不动点真正交替的最简单情形。我们证明，在精确的意义上，半环语义提供了关于所有吸收占优策略的信息——即以最小代价获胜的策略，并讨论了这些策略如何与位置策略以及更一般的持久策略相关联。这些信息使得诸如博弈综合或确定改变博弈结果所需的最小修改等应用成为可能。最后，我们讨论了该方法的局限性，并提出了半环语义无法立即回答的问题。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
