{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:10:41Z","timestamp":1784196641297,"version":"3.55.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101055412"],"award-info":[{"award-number":["101055412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>\n                    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\n                    <jats:italic toggle=\"yes\">fairness-preserving simulations<\/jats:italic>\n                    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\n                    <jats:italic toggle=\"yes\">almost fair<\/jats:italic>\n                    simulation relations for transition systems equipped with a B\u00fcchi 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.\n                  <\/jats:p>","DOI":"10.1145\/3747512","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"222-245","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Almost Fair Simulations"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2307-2296","authenticated-orcid":false,"given":"Arthur","family":"Correnson","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4109-6092","authenticated-orcid":false,"given":"Iona","family":"Kuhn","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"Adnan Aziz Vigyan Singhal Felice Balarin Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli. 1994. Equivalences for fair Kripke structures. In Automata Languages and Programming Serge Abiteboul and Eli Shamir (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 364\u2013375.","DOI":"10.1007\/3-540-58201-0_82"},{"key":"e_1_3_2_4_2","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press 249\u2013253."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","unstructured":"Lorenzo Clemente. 2011. B\u00fcchi automata can have smaller quotients. In International Colloquium on Automata Languages and Programming. Springer 258\u2013270.","DOI":"10.1007\/978-3-642-22012-8_20"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704889"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Arthur Correnson and Iona Kuhn. 2025. Artifact for Almost Fair Simulations. doi:10.5281\/zenodo.15658187","DOI":"10.5281\/zenodo.15658187"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","unstructured":"Kousha Etessami Thomas Wilke and Rebecca A. Schuller. 2001. Fair Simulation Relations Parity Games and State Space Reduction for B\u00fcchi Automata. In Automata Languages and Programming Fernando Orejas Paul G. Spirakis and Jan van Leeuwen (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 694\u2013707.","DOI":"10.1007\/3-540-48224-5_57"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger Orna Kupferman and Sriram K. Rajamani. 1997. Fair simulation. In CONCUR '97: Concurrency Theory Antoni Mazurkiewicz and J\u00f3zef Winkowski (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 273\u2013287.","DOI":"10.1007\/3-540-63141-0_19"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Chung-Kil Hur Georg Neis Derek Dreyer and Viktor Vafeiadis. 2013. The power of parameterization in coinductive proof. In Proceedings 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\u2013206. doi:10.1145\/2429069.2429093","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_3_2_14_2","doi-asserted-by":"crossref","unstructured":"Milka Hutagalung Martin Lange and Etienne Lozes. 2013. Revealing vs. Concealing: More Simulation Games for B\u00fcchi Inclusion. In Language and Automata Theory and Applications Adrian-Horia Dediu Carlos Mart\u00edn-Vide and Bianca Truthe (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 347\u2013358.","DOI":"10.1007\/978-3-642-37064-9_31"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3492545"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591253"},{"key":"e_1_3_2_18_2","doi-asserted-by":"crossref","unstructured":"Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. (1955).","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Yannick Zakowski Paul He Chung-Kil Hur and Steve Zdancewic. 2020. An equational theory for weak bisimulation via generalized parameterized coinduction. In Proceedings 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\u201384. doi:10.1145\/3372885.3373813","DOI":"10.1145\/3372885.3373813"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747512","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:00:28Z","timestamp":1784196028000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747512"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":19,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747512"],"URL":"https:\/\/doi.org\/10.1145\/3747512","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}