Completing Almost Fair Simulations

Zusammenfassung

The paper \emph{Almost Fair Simulations} recently introduced a collection of deductive systems for interactive proofs of language inclusion between B\"uchi automata. These deductive systems enable intuitive proofs via cyclic reasoning principles, but are unfortunately incomplete for \emph{fair similarity}, a standard notion of refinement for B\"uchi automata. In this paper, we address this shortcoming by presenting a new deductive system for language inclusion of B\"uchi automata that preserves the simplicity of \emph{Almost Fair Simulations}, with the additional benefit of being complete for fair similarity. We mechanized the soundness and the completeness proofs of our new system in the Rocq proof assistant. The proofs rely on a new technique we call \emph{nested parameterized coinduction}, an adaptation of Hur's et al. \emph{parameterized coinduction} for the difficult case of proofs by coinduction-induction-coinduction.