Solving First-Order Fixed-Point Logics via a Least-to-Greatest Transformation Based on Game Semantics

Jul 16, 2026

First-order fixed-point logics are used to reason about temporal properties of programs, and validity checking can be reduced via least-to-greatest (μ-to-ν) transformations. This work introduces game-semantic interpretations of μ-to-ν transformations, including a new parity-relation-based construction. Solving transformed fixed-point equation systems is characterized as finding winning strategies in games of the original systems. The framework interprets existing μ-to-ν transformations, relates another game formulation to the winning condition, and adds optimization techniques implemented in a fixed-point logic solver with experimental evaluation.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages34

Reading Time1 h 26 min

Introduction

Motivation and background on fixed-point logics

Validity checking via least-to-greatest transformations

Intuition through a termination example

arXiv :2607 . 10650v 1 [ cs .LO] 12 Jul 2026 Solving First-Order Fixed-Point Logics via a Least-to-Greatest Transformation Based on Game Semantics SATOSHI KURA, Waseda University, Japan HIROSHI UNNO, Tohoku University, Japan 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. Additional Key Words and Phrases: Fixed-point logics, Parity games, Game semantics 1 Introduction Fixed-point logics have been widely studied as a foundation for reasoning about temporal properties of programs. While much of the early work focused on finite-state systems, such as those captured by the modal 􀁠-calculus, recent research has addressed verification of infinite-state programs [Beyene et al. 2013; Bjørner et al. 2015; Cathcart Burn et al. 2018; De Angelis et al. 2022; Kobayashi et al. 2019, 2018; Nanjo et al. 2018; Unno et al. 2023, 2013, 2021] . For example, properties such as the weakest precondition and weakest liberal precondition of a loop can be characterized as the least and greatest fixed points, respectively, and are thus naturally expressible within a fixed-point logic [Blass and Gurevich 1987] . Numerous program verification methods have been developed through reductions to solving constrained Horn clauses (CHCs) [Beyene et al. 2013; Bjørner et al. 2015; Cathcart Burnet al. 2018; De Angelis et al. 2022; Unno et al. 2013], which can be seen as a fragment of a first-order fixed-point logic without 􀁠 and ∃ . Allowing alternation of least and greatest fixed points further increases the expressiveness of fixed-point logics. For instance, model checking of infinite-state while-programs against modal 􀁠-calculus specifications can be reduced to the validity checking problem for a first-order fixed-point logic with fixed-point alternation [Kobayashi et al. 2019] . Other applications of fixed-point logics include game solving and reactive synthesis [Heim and Dimitrova 2024, 2025a,b; Maderbacher and Bloem 2022; Samuel et al. 2021; Schmuck et al. 2024]; implementability of global protocols [Li et al. 2025a,b]; and semantics-guided synthesis [Murphy et al. 2025] . These various applications highlight the role of fixed-point logics as a powerful intermediate formalism for program verification and synthesis. Thus, efficient solvers for fixedpoint logics are a key component towards practical verification and synthesis tools. The validity checking problem of fixed-point logics can be solved by applying transformations from least fixed points to greatest fixed points [Kobayashi et al. 2019; Unno et al. 2023]. We call such transformations least-to-greatest fixed-point transformations or simply 􀁠-to-􀁡 transformation

FAQs

What problem does the paper address in fixed-point logics?

It addresses validity checking for first-order fixed-point logics used to reason about temporal program properties.

What is the main contribution regarding μ-to-ν transformations?

It introduces a game-semantic interpretation for μ-to-ν transformations and proposes a new parity-relation-based μ-to-ν transformation.

How are the transformed fixed-point systems related to games?

Solving the μ-to-ν-transformed fixed-point equation systems corresponds to finding winning strategies in the game semantics of the original equation systems.

Jul 16, 2026

Upload by Clementine