Büchi对策的半环起源：吸收多项式策略分析
Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials
摘要：
本文给出了一个应用不动点公式的半环语义分析Büchi对策策略的案例研究。半环语义通过允许某些半环具有多个真值来推广经典布尔语义。在一个适当的多项式半环中，对定义给定博弈中获胜区域的定点公式进行求值，不仅可以提供关于谁获胜的布尔信息，还可以告诉我们他们如何获胜以及他们可能使用哪些策略。这对于可达性游戏来说是很好理解的，其中获胜区域可定义为最小固定点。Bchi博弈的情况特别有趣，不仅因为它们的实际重要性，而且因为它是最简单的情况，其中定点定义涉及最大和最小不动点的真正交替。我们表明，在一个精确的意义上，半环语义提供的信息，所有的吸收占主导地位的战略，以最小的努力赢得，我们讨论了这些与位置和更一般的持久性战略。这些信息支持游戏合成或确定改变游戏结果所需的最小修改等应用。
英文摘要：
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 Bchi 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
