pith. sign in

arxiv: 2605.26698 · v1 · pith:BEHNAE5Snew · submitted 2026-05-26 · 💻 cs.LO · cs.FL

Almost Fair Simulations

Arthur Correnson , Iona Kuhn , Bernd Finkbeiner This is my paper

Pith reviewed 2026-07-01 16:39 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords fair simulationBüchi fairnesstrace inclusiondeductive systemsliveness propertiesinteractive verificationfinite-state systemsRocq
0
0 comments X

The pith

Almost fair simulations with controlled fixed-point alternations suffice to prove fair trace inclusion for many finite-state systems.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper claims that full fair simulations are often overkill because their complex nestings of inductive and coinductive relations make them hard to apply in interactive verification. Stronger relations called almost fair simulations, which restrict the alternations of fixed points, turn out to be sufficient in many practical cases while admitting much simpler reasoning rules. These rules form deductive systems that let users prove fair trace inclusion between Büchi-fair transition systems without resorting to the full machinery. The authors construct a family of such relations, prove their soundness, and mechanize everything in Rocq, showing concrete examples of use. A reader would care because this lowers the barrier to using simulation-based arguments for liveness properties in manual or semi-automated proofs.

Core claim

Starting from known fair simulation techniques, we progressively build up a family of almost fair simulation relations for transition systems equipped with a Büchi fairness condition. The simulation relations we present can all be equipped with intuitive reasoning rules, leading to elegant deductive systems to prove fair trace inclusion.

What carries the argument

Almost fair simulation relations, built by progressively restricting the alternations of fixed points in standard fair simulations, together with associated deductive systems that directly establish fair trace inclusion.

If this is right

  • Fair trace inclusion between Büchi-fair systems can be established using the presented deductive systems without handling arbitrary nestings of fixed points.
  • The relations support intuitive, rule-based reasoning that fits naturally into interactive proof assistants.
  • Soundness of the entire family has been formally established inside Rocq.
  • The approach applies directly to existing finite-state verification tasks that rely on simulation for liveness.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Interactive verification tools could adopt these relations as a default for liveness arguments, reducing the need for full fair-simulation algorithms.
  • The controlled-alternation pattern might generalize to other fairness notions such as Streett or parity conditions.
  • The deductive systems could be combined with automated tactics to further lower the manual effort in proving trace inclusion.

Load-bearing premise

Applications in interactive verification of finite-state systems only require these controlled-alternation almost fair simulations rather than full fair simulation relations with their more complex nestings.

What would settle it

A concrete pair of finite-state systems with Büchi fairness where fair trace inclusion holds and is provable by a full fair simulation, yet no almost fair simulation relation exists between them.

Figures

Figures reproduced from arXiv: 2605.26698 by Arthur Correnson, Bernd Finkbeiner, Iona Kuhn.

Figure 1
Figure 1. Figure 1: Rules for fsimdirect and Final if the current left-state is rejecting (𝑠1 ∉ F1) or if the current right-state is accepting (𝑠2 ∈ F2). Additionally, we note that making progress via Step or Final always releases the guard. The remaining rules Cycle, Guard and Invariant are for handling the parameter 𝐻. Cycle allows to conclude a proof whenever 𝐻 is unguarded and already contains the targeted pair of states.… view at source ↗
Figure 2
Figure 2. Figure 2: Basic rules for fsimdelay The rules L-to-R, L-Step, R-Delay and R-Final are immediately obtained by unfolding the definition of fsimR delay and by instantiating the Step rule of parameterized coinduction with fsimFL delay as the underlying monotone functor. We note that without further assumptions, the context 𝐻 can only be exploited and modified (via the rules L-Cycle, L-Guard, and L-Invariant) when the g… view at source ↗
Figure 3
Figure 3. Figure 3: Selection of proof rules for fsimrdelay We showcase the use of fsimrdelay by applying the rules of [PITH_FULL_IMAGE:figures/full_fig_p021_3.png] view at source ↗
read the original abstract

It is well known that liveness properties cannot be proven using standard simulation arguments. This issue has been mitigated by extending standard notions of simulation for transition systems to fairness-preserving simulations for systems equipped with an additional fairness condition modeling liveness assumptions and/or liveness requirements. In the context of automated verification of finite-state systems, proofs by simulation are an appealing method as there exist efficient algorithms to find a simulation between two systems. However, applications of fair simulation to interactive verification have been much less studied. Perhaps one reason is that the definitions of fair simulation relations typically involve non-trivial nestings of inductive and coinductive relations, making them particularly difficult to use and to reason about. In this paper, we argue that in many cases, stronger notions of fair simulation involving more controlled alternations of fixed points are sufficient. Starting from known fair simulation techniques, we progressively build up a family of almost fair simulation relations for transition systems equipped with a Buechi fairness condition. The simulation relations we present can all be equipped with intuitive reasoning rules, leading to elegant deductive systems to prove fair trace inclusion. We mechanized our simulation relations and their associated deductive systems in the Rocq proof assistant, proved their soundness, and we demonstrate their use through a selection of examples.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims that stronger notions of fair simulation with more controlled alternations of fixed points are sufficient in many cases for proving fair trace inclusion on Büchi-fair transition systems. Starting from known fair simulation techniques, it progressively defines a family of almost fair simulation relations, equips each with intuitive reasoning rules that yield elegant deductive systems, mechanizes the relations and systems in Rocq, proves their soundness, and illustrates their use on examples for interactive verification of finite-state systems.

Significance. If the mechanized soundness proofs hold, the work supplies practical, human-readable deductive systems for fairness-preserving simulation that are easier to apply than full fair simulations with complex nestings. The Rocq mechanization, explicit soundness proofs, and progressive construction from prior techniques are clear strengths that support reproducibility and usability in interactive verification settings.

major comments (1)
  1. [Abstract] Abstract (paragraph beginning 'In this paper, we argue that in many cases'): the central claim that almost fair simulations suffice for the targeted interactive-verification applications rests on the assumption that controlled-alternation variants are adequate in practice; however, the manuscript provides only positive examples and does not supply a counter-example or characterization showing when the full nesting of fixed points becomes necessary, which is load-bearing for the sufficiency argument.
minor comments (2)
  1. The spelling 'Buechi' appears throughout; standardize to 'Büchi' with the correct diacritic.
  2. [Abstract] No commit hash, repository link, or artifact identifier is given for the Rocq development despite the soundness claims; adding this would allow independent checking of the mechanized proofs.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and the recommendation of minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract (paragraph beginning 'In this paper, we argue that in many cases'): the central claim that almost fair simulations suffice for the targeted interactive-verification applications rests on the assumption that controlled-alternation variants are adequate in practice; however, the manuscript provides only positive examples and does not supply a counter-example or characterization showing when the full nesting of fixed points becomes necessary, which is load-bearing for the sufficiency argument.

    Authors: We agree that the manuscript supports the claim of sufficiency primarily through positive examples and does not include counter-examples or a characterization of cases requiring full fixed-point nesting. The paper focuses on developing practical, easier-to-use relations for interactive verification rather than exhaustively delineating the boundary with full fair simulation. In the revised manuscript we will qualify the abstract claim to refer specifically to the examples and applications considered, and add a brief note in the conclusions acknowledging that full nesting may be needed in other scenarios. This clarifies the scope without altering the core contribution. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper introduces newly defined almost fair simulation relations with controlled fixed-point alternations, equips them with reasoning rules, and establishes soundness via mechanized proofs in Rocq. No derivation step reduces a prediction or central claim to a fitted input, self-citation, or prior ansatz by construction; the relations are presented as stronger but usable variants of known fair simulations, with independent formal verification supporting the claims rather than circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard mathematical definitions of inductive and coinductive relations over transition systems and Büchi fairness conditions; no free parameters, invented entities, or ad-hoc axioms are introduced beyond the new simulation definitions themselves.

axioms (2)
  • standard math Standard properties of least and greatest fixed points for inductive and coinductive definitions on relations
    Invoked when defining the simulation relations and their reasoning rules.
  • domain assumption Büchi fairness conditions correctly model the relevant liveness assumptions and requirements
    Used throughout as the fairness model for the transition systems.

pith-pipeline@v0.9.1-grok · 5744 in / 1261 out tokens · 29652 ms · 2026-07-01T16:39:30.801080+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

20 extracted references · 12 canonical work pages

  1. [1]

    Martin Abadi and Leslie Lamport. 1991. The existence of refinement mappings.Theoretical Computer Science82, 2 (1991), 253–284. doi:10.1016/0304-3975(91)90224-P

    work page doi:10.1016/0304-3975(91)90224-p 1991

  2. [2]

    Brayton, and Alberto L

    Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. 1994. Equiva- lences for fair Kripke structures. InAutomata, Languages and Programming, Serge Abiteboul and Eli Shamir (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 364–375

    1994

  3. [3]

    2008.Principles of model checking

    Christel Baier and Joost-Pieter Katoen. 2008.Principles of model checking. MIT Press, 249–253

    2008

  4. [4]

    Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, and Derek Dreyer. 2023. Stuttering for Free.Proc. ACM Program. Lang.7, OOPSLA2, Article 281 (Oct. 2023), 28 pages. doi:10.1145/3622857

    work page doi:10.1145/3622857 2023

  5. [5]

    Lorenzo Clemente. 2011. Büchi automata can have smaller quotients. InInternational Colloquium on Automata, Languages, and Programming. Springer, 258–270

    2011

  6. [6]

    Arthur Correnson and Bernd Finkbeiner. 2025. Coinductive Proofs for Temporal Hyperliveness.Proc. ACM Program. Lang.9, POPL, Article 53 (Jan. 2025), 28 pages. doi:10.1145/3704889

    work page doi:10.1145/3704889 2025

  7. [7]

    2025.Artifact for Almost Fair Simulations

    Arthur Correnson and Iona Kuhn. 2025.Artifact for Almost Fair Simulations. doi:10.5281/zenodo.15658187

    work page doi:10.5281/zenodo.15658187 2025

  8. [8]

    Schuller

    Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. 2001. Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata. InAutomata, Languages and Programming, Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 694–707

    2001

  9. [9]

    Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations.Proc. ACM Program. Lang.6, POPL, Article 28 (Jan. 2022), 31 pages. doi:10.1145/3498689

    work page doi:10.1145/3498689 2022

  10. [10]

    Orna Grumberg and David E. Long. 1994. Model checking and modular verification.ACM Trans. Program. Lang. Syst. 16, 3 (May 1994), 843–871. doi:10.1145/177492.177725

    work page doi:10.1145/177492.177725 1994

  11. [11]

    Henzinger, Orna Kupferman, and Sriram K

    Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. 1997. Fair simulation. InCONCUR ’97: Concurrency Theory, Antoni Mazurkiewicz and Józef Winkowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 273–287

    1997

  12. [12]

    Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. 2013. The power of parameterization in coinductive proof. InProceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy)(POPL ’13). Association for Computing Machinery, New York, NY, USA, 193–206. doi:10.1145/2429069. 2429093

    work page doi:10.1145/2429069 2013

  13. [13]

    Milka Hutagalung, Martin Lange, and Etienne Lozes. 2013. Revealing vs. Concealing: More Simulation Games for Büchi Inclusion. InLanguage and Automata Theory and Applications, Adrian-Horia Dediu, Carlos Martín-Vide, and Bianca Truthe (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 347–358

    2013

  14. [14]

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.SIGPLAN Not.50, 1 (Jan. 2015), 637–650. doi:10.1145/2775051.2676980

    work page doi:10.1145/2775051.2676980 2015

  15. [15]

    Leslie Lamport and Stephan Merz. 2022. Prophecy Made Simple.ACM Trans. Program. Lang. Syst.44, 2, Article 6 (April 2022), 27 pages. doi:10.1145/3492545

    work page doi:10.1145/3492545 2022

  16. [16]

    Dongjae Lee, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, and Chung-Kil Hur. 2023. Fair Operational Semantics.Proc. ACM Program. Lang.7, PLDI, Article 139 (June 2023), 24 pages. doi:10.1145/3591253

    work page doi:10.1145/3591253 2023

  17. [17]

    Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. (1955)

    1955

  18. [18]

    Pierce, and Steve Zdancewic

    Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic

  19. [19]

    ACM Program

    Interaction trees: representing recursive and impure programs in Coq.Proc. ACM Program. Lang.4, POPL, Article 51 (Dec. 2019), 32 pages. doi:10.1145/3371119

    work page doi:10.1145/3371119 2019

  20. [20]

    Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. 2020. An equational theory for weak bisimulation via generalized parameterized coinduction. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs(New Orleans, LA, USA)(CPP 2020). Association for Computing Machinery, New York, NY, USA, 71–84. doi:10.1145...

    work page doi:10.1145/3372885.3373813 2020