DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.20

Completing Almost Fair Simulations

Authors: Arthur Correnson, Iona Kuhn, and Bernd Finkbeiner

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

The paper Almost Fair Simulations recently introduced a collection of deductive systems for interactive proofs of language inclusion between Büchi automata. These deductive systems enable intuitive proofs via cyclic reasoning principles, but are unfortunately incomplete for fair similarity, a standard notion of refinement for Büchi automata. In this paper, we address this shortcoming by presenting a new deductive system for language inclusion of Büchi automata that preserves the simplicity of 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 nested parameterized coinduction, an adaptation of Hur’s et al. parameterized coinduction for the difficult case of proofs by coinduction-induction-coinduction.

Cite as

Arthur Correnson, Iona Kuhn, and Bernd Finkbeiner. Completing Almost Fair Simulations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{correnson_et_al:LIPIcs.ITP.2026.20,
  author =	{Correnson, Arthur and Kuhn, Iona and Finkbeiner, Bernd},
  title =	{{Completing Almost Fair Simulations}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.20},
  URN =		{urn:nbn:de:0030-drops-269944},
  doi =		{10.4230/LIPIcs.ITP.2026.20},
  annote =	{Keywords: Fair Simulation, Deductive Systems, Interactive Proof Assistants, Coinduction, Language Containment}
}

Search Results

Documents authored by Correnson, Arthur

Completing Almost Fair Simulations

Abstract

Cite as

Thanks for your feedback!

Could not send message