Document Open Access Logo

Minimal and Canonical Quotients for Simulation Equivalences

Authors Eduardo Costa Martins , Tim A. C. Willemse

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.26.pdf
  • Filesize: 0.95 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Problems, reductions and completeness
Keywords
  • Coupled Similarity
  • Weak Simulation
  • Minimisation

Metrics

Abstract

Quotients have only been studied for a handful of equivalences in the linear time-branching time spectrum, for which there are results pertaining to canonicity and minimality. We extend these results to weak simulation equivalence and coupled similarity, two closely related equivalences induced by simulation preorders. We describe abstract procedures for transforming an LTS into a unique representative of its equivalence class, and for transforming an LTS into an equivalent state- and transition-minimal LTS. Moreover, we show the minimisation problem is NP-complete.

Cite As Get BibTex

Eduardo Costa Martins and Tim A. C. Willemse. Minimal and Canonical Quotients for Simulation Equivalences. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.26

Author Details

Eduardo Costa Martins
  • Eindhoven University of Technology, The Netherlands
Tim A. C. Willemse
  • Eindhoven University of Technology, The Netherlands

Funding

The Cynergy4MIE project is supported by the Chips Joint Undertaking and its members, including the top-up funding by National Authorities under Grant Agreement No 101140226.

References

  1. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodríguez, and Anna Ingolfsdottir. Axiomatizing weak simulation semantics over BCCSP. Theoretical Computer Science, 537:42-71, June 2014. URL: https://doi.org/10.1016/j.tcs.2013.03.013.
  2. Benjamin Bisping and Luisa Montanari. Coupled similarity and contrasimilarity, and how to compute them. Arch. Formal Proofs, 2023, August 2023. URL: https://www.isa-afp.org/entries/Coupledsim_Contrasim.html.
  3. Benjamin Bisping and Uwe Nestmann. Computing Coupled Similarity. In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 244-261, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-17462-0_14.
  4. Tommaso Bolognesi and Scott A. Smolka. Fundamental results for the verification of observational equivalence: A survey. In Harry Rudin and Colin H. West, editors, Protocol Specification, Testing and Verification VII, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification, Zurich, Switzerland, 5-8 May, 1987, pages 165-179. North-Holland, January 1987. Pages: 179. Google Scholar
  5. Mark Bouwman, Maurice Laveaux, Bas Luttik, and Tim A. C. Willemse. Decompositional branching bisimulation minimisation of monolithic processes. In FACS, volume 13712 of Lecture Notes in Computer Science, pages 161-182. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-20872-0_10.
  6. Doron Bustan and Orna Grumberg. Simulation Based Minimization. In David McAllester, editor, Automated Deduction - CADE-17, pages 255-270, Berlin, Heidelberg, 2000. Springer. URL: https://doi.org/10.1007/10721959_20.
  7. Jaana Eloranta. Minimizing the number of transitions with respect to observation equivalence. BIT Numerical Mathematics, 31(4):576-590, December 1991. URL: https://doi.org/10.1007/BF01933173.
  8. Jaana Eloranta, Martti Tienari, and Antti Valmari. Essential transitions to bisimulation equivalences. Theoretical Computer Science, 179(1):397-419, June 1997. URL: https://doi.org/10.1016/S0304-3975(96)00281-2.
  9. Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf., 15(2):89-107, 2013. URL: https://doi.org/10.1007/S10009-012-0244-Z.
  10. Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, and A. W. Roscoe. FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf., 18(2):149-167, 2016. URL: https://doi.org/10.1007/S10009-015-0377-Y.
  11. David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, and Anton Wijs. An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 3-20, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-45237-7_1.
  12. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86(1):43-68, May 1990. URL: https://doi.org/10.1016/0890-5401(90)90025-D.
  13. Antonín Kucera and Richard Mayr. Simulation preorder on simple process algebras. In Jirí Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors, Automata, Languages and Programming, 26th International Colloquium, ICALP'99, Prague, Czech Republic, July 11-15, 1999, Proceedings, Lecture Notes in Computer Science, pages 503-512. Springer, 1999. URL: https://doi.org/10.1007/3-540-48523-6_47.
  14. Antonín Kučera. On finite representations of infinite-state behaviours. Information Processing Letters, 70(1):23-30, April 1999. URL: https://doi.org/10.1016/S0020-0190(99)00029-0.
  15. Antonín Kučera and Javier Esparza. A Logical Viewpoint on Process-algebraic Quotients. Journal of Logic and Computation, 13(6):863-880, December 2003. URL: https://doi.org/10.1093/logcom/13.6.863.
  16. Maurice Laveaux and Tim A. C. Willemse. Decomposing monolithic processes in a process algebra with multi-actions. J. Log. Algebraic Methods Program., 132:100858, 2023. URL: https://doi.org/10.1016/J.JLAMP.2023.100858.
  17. Eduardo Costa Martins and Tim Willemse. Minimal and canonical quotients for simulation equivalences. CoRR, abs/2606.21450, 2026. URL: https://doi.org/10.48550/arXiv.2606.21450.
  18. David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science, pages 167-183, Berlin, Heidelberg, 1981. Springer. URL: https://doi.org/10.1007/BFb0017309.
  19. Joachim Parrow and Peter Sjödin. The complete axiomatization of cs-congruence. In Patrice Enjalbert, Ernst W. Mayr, and Klaus W. Wagner, editors, STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, February 24-26, 1994, Proceedings, volume 775 of Lecture Notes in Computer Science, pages 557-568, Berlin, Heidelberg, 1994. Springer. URL: https://doi.org/10.1007/3-540-57785-8_171.
  20. Michel A. Reniers, Rob Schoren, and Tim A.C. Willemse. Results on Embeddings Between State-Based and Event-Based Systems. The Computer Journal, 57(1):73-92, January 2014. URL: https://doi.org/10.1093/comjnl/bxs156.
  21. Edd Turner, Michael Leuschel, Corinna Spermann, and Michael Butler. Symmetry reduced model checking for b. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), pages 25-34, 2007. URL: https://doi.org/10.1109/TASE.2007.50.
  22. Irek Ulidowski. Equivalences on observable processes. In [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pages 148-159, 1992. URL: https://doi.org/10.1109/LICS.1992.185529.
  23. Rob J. van Glabbeek. The linear time - Branching time spectrum. In J. C. M. Baeten and J. W. Klop, editors, CONCUR '90 Theories of Concurrency: Unification and Extension, pages 278-297, Berlin, Heidelberg, 1990. Springer. URL: https://doi.org/10.1007/BFb0039066.
  24. Rob J. van Glabbeek. The linear time - Branching time spectrum II. In Eike Best, editor, CONCUR'93, pages 66-81, Berlin, Heidelberg, 1993. Springer. URL: https://doi.org/10.1007/3-540-57208-2_6.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact