AI 中文总结
研究通过基于博弈语义的最小到最大变换求解一阶不动点逻辑，引入新变换并对现有变换进行博弈语义解释，提出优化技术，经实验验证其能有效求解不动点逻辑。
AI 中文摘要
不动点逻辑为推理程序的时间属性提供了一个具有表达力的中间框架。解决其有效性检查问题的关键方法之一是通过从最小不动点到最大不动点的变换（μ到ν变换）。本文引入了μ到ν变换的博弈语义解释。首先基于奇偶关系引入了一种新的μ到ν变换，表明求解μ到ν变换后的不动点方程组对应于在原始不动点方程组的博弈语义中找到获胜策略。还对现有的两种μ到ν变换进行了博弈语义解释。在实现方面，提出了有效求解新μ到ν变换的优化技术，并通过实验证明了其有效性。
英文摘要
Fixed-point logics provide an expressive intermediate framework for reasoning about temporal properties of programs. One of the key approaches to solving their validity checking problem is via transformations from least fixed points to greatest fixed points ($μ$-to-$ν$ transformations), which generalizes a reduction from termination verification to safety verification studied in binary reachability analysis. In this paper, we introduce game-semantic interpretations of $μ$-to-$ν$ transformations. We first introduce a new $μ$-to-$ν$ transformation based on parity relations. We show that solving $μ$-to-$ν$-transformed fixed-point equation systems corresponds to finding winning strategies in the game semantics of the original fixed-point equation systems. We apply the same game-semantic framework to interpret two existing $μ$-to-$ν$ transformations, one by Kobayashi et al.\ and the other by Unno et al, and show that they admit analogous game-semantic interpretations. Furthermore, we show that the game introduced by Tsukada et al.\ corresponds to an alternative characterization of the winning condition. On the implementation side, we propose optimization techniques for efficiently solving our new $μ$-to-$ν$ transformation. We implement these techniques in a fixed-point logic solver, compare our approach with existing solvers, and demonstrate the effectiveness of the proposed optimizations through experiments.
