References

Aceto, L., Fokkink, W., van Glabbeek, R., & Ingólfsdóttir, A. (2004). Nested semantics over finite trees are equationally hard. Information and Computation, 191(2), 203–232. https://doi.org/10.1016/j.ic.2004.02.001

Aceto, L., Ingólfsdóttir, A., Larsen, K. G., & Srba, J. (2007). Reactive systems: Modelling, specification and verification (pp. 142–158). Cambridge University Press. https://doi.org/10.1017/CBO9780511814105.008

Adler, R. (2022). Simulation fehlertoleranter Konsensalgorithmen in Hash.ai [Bachelor's thesis]. Technische Universität Berlin.

Allaire, J. J., Teague, C., Scheidegger, C., Xie, Y., Dervieux, C., & Woodhull, G. (2025). Quarto (Version 1.7) [Computer software]. https://doi.org/10.5281/zenodo.5960048

Alshukairi, Z. (2022). Automatisierte Reduktion von reaktiver zu starker Bisimilarität [Bachelor's thesis]. Technische Universität Berlin.

Andersen, J. R., Andersen, N., Enevoldsen, S., Hansen, M. M., Larsen, K. G., Olesen, S. R., Srba, J., & Wortmann, J. K. (2015). CAAL: Concurrency workbench, aalborg edition. In M. Leucker, C. Rueda, & F. D. Valencia (Eds.), Theoretical aspects of computing — ICTAC 2015 (pp. 573–582). Springer International Publishing. https://doi.org/10.1007/978-3-319-25150-9_33

Andersen, J. R., Hansen, M. M., & Andersen, N. (2015). CAAL 2.0 – equivalences, preorders and games for CCS and TCCS (Vol. DES104F15) [Student project supervised by Jiří Srba and Kim Guldstrand Larsen]. Aalborg University. https://caal.cs.aau.dk/docs/CAAL2_EPG.pdf

Babai, L. (2016). Graph isomorphism in quasipolynomial time [extended abstract]. STOC ’16, 684–697. https://doi.org/10.1145/2897518.2897542

Baier, C., D’Argenio, P. R., & Hermanns, H. (2020). On the probabilistic bisimulation spectrum with silent moves. Acta Informatica, 57(3), 465–512. https://doi.org/10.1007/s00236-020-00379-2

Baker, A., Derin, M. O., Neto, D., Maxfield, M. C., & Sinclair, D. (Eds.). (2025). WebGPU shading language (Version W3C Recommendation Draft). World Wide Web Consortium. https://www.w3.org/TR/WGSL/

Balcázar, J., Gabarro, J., & Santha, M. (1992). Deciding bisimilarity is P-complete. Formal Aspects of Computing, 4, 638–648. https://doi.org/10.1007/BF03180566

Barthel, L. A., Bisping, B., Hübner, L. M., Lemke, C., Mattes, K. P. P., & Mollenkopf, L. (2025). A weak spectroscopy game to characterize behavioral equivalences [Isabelle/HOL formalization]. https://equivio.github.io/silent-step-spectroscopy/AFP/Weak_Spectroscopy.

Barwell, A. D., Ferreira, F., & Yoshida, N. (2022). CONCUR test-of-time award for the period 1994–97 interview with Uwe Nestmann and Benjamin C. Pierce. Journal of Logical and Algebraic Methods in Programming, 125, 100744. https://doi.org/10.1016/j.jlamp.2021.100744

Basten, T. (1996). Branching bisimilarity is an equivalence indeed! Information Processing Letters, 58(3), 141–147. https://doi.org/10.1016/0020-0190(96)00034-8

Bell, C. J. (2013). Certifiably sound parallelizing transformations. In International conference on certified programs and proofs (pp. 227–242). Springer. https://doi.org/10.1007/978-3-319-03545-1_15

Bell, C. J. (2014). A proof theory for loop-parallelizing transformations [PhD thesis, Princeton University]. https://people.csail.mit.edu/cj/thesis/thesis.pdf

Beohar, H., Gurke, S., König, B., & Messing, K. (2023). Hennessy-Milner Theorems via Galois Connections. In B. Klin & E. Pimentel (Eds.), LIPIcs: Vol. 252. 31st EACSL annual conference on computer science logic (CSL 2023) (pp. 12:1–12:18). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2023.12

Bernardo, M., & Esposito, A. (2023). Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities. EPTCS, 390, 67–81. https://doi.org/10.4204/eptcs.390.5

Bian, G., & Abate, A. (2017). On the relationship between bisimulation and trace equivalence in an approximate probabilistic context. In J. Esparza & A. S. Murawski (Eds.), Foundations of software science and computation structures (pp. 321–337). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-54458-7_19

Bisping, B. (2018). Computing coupled similarity [Master’s thesis, Technische Universität Berlin]. https://coupledsim.bbisping.de/bisping_computingCoupledSimilarity_thesis.pdf

Bisping, B. (2021). Linear-time–branching-time spectroscope: TACAS 2021 edition [Artifact archived on Zenodo]. Zenodo. https://doi.org/10.5281/zenodo.4475878

Bisping, B. (2023a). Linear-time–branching-time spectroscope v0.3.0 (Version v0.3.0) [Artifact archived on Zenodo]. Zenodo. https://doi.org/10.5281/zenodo.7870252

Bisping, B. (2023b). Process equivalence problems as energy games. In C. Enea & A. Lal (Eds.), Computer aided verification (pp. 85–106). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-37706-8_5

Bisping, B. (2023c). Process equivalence problems as energy games [Technical Report]. Technische Universität Berlin. https://doi.org/10.48550/arXiv.2303.08904

Bisping, B., Brodmann, P.-D., Jungnickel, T., Rickmann, C., Seidler, H., Stüber, A., Wilhelm-Weidner, A., Peters, K., & Nestmann, U. (2016). Mechanical verification of a constructive proof for FLP. In J. C. Blanchette & S. Merz (Eds.), LNCS: Vol. 9807. Interactive theorem proving (pp. 107–122). Springer International Publishing. https://doi.org/10.1007/978-3-319-43144-4_7

Bisping, B., & Jansen, D. N. (2024). One energy game for the spectrum between branching bisimilarity and weak trace semantics. In G. Caltais & C. Di Giusto (Eds.), EPTCS: Vol. 412. Proceedings Combined 31st International Workshop on expressiveness in concurrency and 21st Workshop on structural operational semantics, Calgary, Canada, 9th September 2024 (pp. 71–88). Open Publishing Association. https://doi.org/10.4204/EPTCS.412.6

Bisping, B., & Jansen, D. N. (2025). Deciding all behavioral equivalences at once II: The silent-step spectrum [Preprint]. https://code.keks.in/papers/2025/silent-step-spectroscopy_journal.pdf

Bisping, B., Jansen, D. N., & Nestmann, U. (2022). Deciding all behavioral equivalences at once: A game for linear-time–branching-time spectroscopy. Logical Methods in Computer Science, 18(3). https://doi.org/10.46298/lmcs-18(3:19)2022

Bisping, B., & Montanari, L. (2021). A game characterization for contrasimilarity. In O. Dardha & V. Castiglioni (Eds.), EPTCS: Vol. 339. Proceedings Combined 28th International Workshop on expressiveness in concurrency and 18th Workshop on structural operational semantics (pp. 27–42). Open Publishing Association. https://doi.org/10.4204/EPTCS.339.5

Bisping, B., & Montanari, L. (2023). Coupled similarity and contrasimilarity, and how to compute them. Arch. Formal Proofs, 2023. https://www.isa-afp.org/entries/Coupledsim_Contrasim.html

Bisping, B., & Montanari, L. (2024). Characterizing contrasimilarity through games, modal logic, and complexity. Inf. Comput., 300, 105191. https://doi.org/10.1016/J.IC.2024.105191

Bisping, B., & Nestmann, U. (2019). Computing coupled similarity. In T. Vojnar & L. Zhang (Eds.), LNCS: Vol. 11427. Tools and algorithms for the construction and analysis of systems: TACAS (pp. 244–261). Springer. https://doi.org/10.1007/978-3-030-17462-0_14

Bisping, B., & Nestmann, U. (2021). A game for linear-time–branching-time spectroscopy. In J. F. Groote & K. G. Larsen (Eds.), LNCS: Vol. 12651. Tools and algorithms for the construction and analysis of systems: TACAS (pp. 3–19). Springer. https://doi.org/10.1007/978-3-030-72016-2_1

Bisping, B., Nestmann, U., & Peters, K. (2020). Coupled similarity: The first 32 years. Acta Informatica, 57(3–5), 439–463. https://doi.org/10.1007/s00236-019-00356-4

Bouali, A. (1992). Weak and branching bisimulation in FCTOOL. INRIA. https://inria.hal.science/inria-00074985

Brookes, S. D., Hoare, C. A. R., & Roscoe, A. W. (1984). A theory of communicating sequential processes. J. ACM, 31(3), 560–599. https://doi.org/10.1145/828.833

Bulik, J. (2021). Statically analysing inter-process communication in Elixir programs [Bachelor's thesis, Technische Universität Berlin]. https://gitlab.com/MrGreenTea/stille-post

Bulychev, P. E. (2011). Game-theoretic simulation checking tool. Programming and Computer Software, 37(4), 200. https://doi.org/10.1134/S0361768811040013

Bunte, O., Groote, J. F., Keiren, J. J. A., Laveaux, M., Neele, T., Vink, E. P. de, Wesselink, W., Wijs, A., & Willemse, T. A. C. (2019). The mCRL2 toolset for analysing concurrent systems. In T. Vojnar & L. Zhang (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 21–39). Springer International Publishing. https://doi.org/10.1007/978-3-030-17465-1_2

Čerāns, K. (1993). Decidability of bisimulation equivalences for parallel timer processes. In G. von Bochmann & D. K. Probst (Eds.), Computer aided verification (pp. 302–315). Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-56496-9_24

Chen, X., & Deng, Y. (2008). Game characterizations of process equivalences. In G. Ramalingam (Ed.), LNCS: Vol. 5356. Programming languages and systems: APLAS (pp. 107–121). Springer. https://doi.org/10.1007/978-3-540-89330-1_8

Chistikov, D. (2024). An Introduction to the Theory of Linear Integer Arithmetic. In S. Barman & S. Lasota (Eds.), LIPIcs: Vol. 323. 44th IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2024) (pp. 1:1–1:36). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2024.1

Cleaveland, R. (1991). On automatically explaining bisimulation inequivalence. In E. M. Clarke & R. P. Kurshan (Eds.), LNCS: Vol. 531. Computer-aided verification: CAV’90 (pp. 364–372). Springer. https://doi.org/10.1007/BFb0023750

Cleaveland, R., & Hennessy, M. (1993). Testing equivalence as a bisimulation equivalence. Formal Aspects of Computing, 5(1), 1–20. https://doi.org/10.1007/BF01211314

Cleaveland, R., Parrow, J., & Steffen, B. (1990). The concurrency workbench. In J. Sifakis (Ed.), Automatic verification methods for finite state systems (pp. 24–37). Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-52148-8_3

Cleaveland, R., & Sims, S. (1996). The NCSU concurrency workbench. In R. Alur & T. A. Henzinger (Eds.), Computer aided verification (pp. 394–397). Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-61474-5_87

Cleaveland, R., & Sokolsky, O. (2001). Equivalence and preorder checking for finite-state systems. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra (pp. 391–424). Elsevier Science. https://doi.org/10.1016/B978-044482830-9/50024-2

De Nicola, R., & Vaandrager, F. (1995). Three logics for branching bisimulation. J. ACM, 42(2), 458–487. https://doi.org/10.1145/201019.201032

Deifel, H.-P., Milius, S., Schröder, L., & Wißmann, T. (2019). Generic partition refinement and weighted tree automata. In M. H. ter Beek, A. McIver, & J. N. Oliveira (Eds.), Formal methods – the next 30 years (pp. 280–297). Springer International Publishing. https://doi.org/10.1007/978-3-030-30942-8_18

Delzanno, G., & Raskin, J.-F. (2000). Symbolic representation of upward-closed sets. In S. Graf & M. Schwartzbach (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 426–441). Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-46419-0_29

Duong, T. M. (2022). Developing an educational tool for linear-time–branching-time spectroscopy [Bachelor's thesis]. Technische Universität Berlin.

England, J. (2021). HML synthesis of distinguished processes [Bachelor's thesis]. Technische Universität Berlin.

Erné, M., Koslowski, J., Melton, A., & Strecker, G. E. (1993). A primer on Galois connections. Annals of the New York Academy of Sciences, 704(1), 103–125. https://doi.org/10.1111/j.1749-6632.1993.tb52513.x

Ésik, Z., Fahrenberg, U., Legay, A., & Quaas, K. (2013). Kleene algebras and semimodules for energy problems. In D. Van Hung & M. Ogawa (Eds.), Automated technology for verification and analysis (pp. 102–117). Springer International Publishing. https://doi.org/10.1007/978-3-319-02444-8_9

Fahrenberg, U., Juhl, L., Larsen, K. G., & Srba, J. (2011). Energy games in multiweighted automata. In A. Cerone & P. Pihlajasaari (Eds.), Theoretical aspects of computing – ICTAC 2011 (pp. 95–115). Springer. https://doi.org/10.1007/978-3-642-23283-1_9

Fahrenberg, U., & Legay, A. (2014). The quantitative linear-time–branching-time spectrum. Theoretical Computer Science, 538, 54–69. https://doi.org/10.1016/j.tcs.2013.07.030

Fokkink, W., van Glabbeek, R., & Luttik, B. (2019). Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence. Information and Computation, 268, 104435. https://doi.org/10.1016/j.ic.2019.104435

Ford, C., Milius, S., & Schröder, L. (2021). Behavioural preorders via graded monads. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–13. https://doi.org/10.1109/LICS52264.2021.9470517

Forster, J., Schröder, L., Wild, P., Beohar, H., Gurke, S., & Messing, K. (2024). Graded semantics and graded logics for eilenberg-moore coalgebras. In B. König & H. Urbat (Eds.), Coalgebraic methods in computer science (pp. 114–134). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-66438-0_6

Fournet, C., & Gonthier, G. (2005). A hierarchy of equivalences for asynchronous calculi. The Journal of Logic and Algebraic Programming, 63(1), 131–173. https://doi.org/j.jlap.2004.01.006

Frutos Escrig, D. de, Gregorio Rodríguez, C., Palomino, M., & Romero Hernández, D. (2013). Unifying the Linear Time-Branching Time Spectrum of Strong Process Semantics. Logical Methods in Computer Science, 9(2:11), 1–74. https://doi.org/10.2168/LMCS-9(2:11)2013

Frutos Escrig, D. de, Keiren, J. J. A., & Willemse, T. A. C. (2017). Games for bisimulations and abstraction. Logical Methods in Computer Science, 13(4:15), 1–40. https://doi.org/10.23638/LMCS-13(4:15)2017

Gale, D., & Stewart, F. M. (1953). Infinite games with perfect information. In H. W. Kuhn & A. W. Tucker (Eds.), Contributions to the theory of games, volume II (pp. 245–266). Princeton University Press. https://doi.org/10.1515/9781400881970-014

Garavel, H. (2017). The VLTS benchmark suite. https://doi.org/10.18709/perscido.2017.11.ds100

Garavel, H. (2023). What is wrong with process calculi – and how to recover? [Talk]. Open problems in concurrency theory (OPCT 2023), University of Urbino, Italy. http://www.sti.uniurb.it/events/opct2023/SLIDES/garavel.pdf

Garavel, H., & Lang, F. (2022). Equivalence checking 40 years after: A review of bisimulation tools. In N. Jansen, M. Stoelinga, & P. van den Bos (Eds.), LNCS: Vol. 13560. A journey from process algebra via timed automata to model learning: Essays dedicated to Frits Vaandrager on the occasion of his 60th birthday (pp. 213–265). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-15629-8_13

Garavel, H., Lang, F., Mateescu, R., & Serwe, W. (2013). CADP 2011: A toolbox for the construction and analysis of distributed processes. International Journal on Software Tools for Technology Transfer, 15(2), 89–107. https://doi.org/10.1007/s10009-012-0244-z

Gazda, M., Fokkink, W., & Massaro, V. (2020). Congruence from the operator’s point of view: Syntactic requirements on modal characterizations. Acta Informatica, 57(3–5), 329–351. https://doi.org/10.1007/s00236-019-00355-5

Geuvers, H. (2022). Apartness and distinguishing formulas in Hennessy–Milner logic. In N. Jansen, M. Stoelinga, & P. van den Bos (Eds.), LNCS: Vol. 13560. A journey from process algebra via timed automata to model learning: Essays dedicated to Frits Vaandrager on the occasion of his 60th birthday (pp. 266–282). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-15629-8_14

Geuvers, H., & Golov, A. (2023). Positive Hennessy-Milner logic for branching bisimulation. https://arxiv.org/abs/2210.07380

Geuvers, H., & Jacobs, B. (2021). Relating apartness and bisimulation. Logical Methods in Computer Science, 17(3). https://doi.org/10.46298/LMCS-17(3:15)2021

Gibson-Robinson, T., Armstrong, P., Boulgakov, A., & Roscoe, A. W. (2014). FDR3: A modern refinement checker for CSP. In E. Ábrahám & K. Havelund (Eds.), International conference on tools and algorithms for the construction and analysis of systems (pp. 187–201). Springer. https://doi.org/10.1007/978-3-642-54862-8_13

Göthel, T. (2012). Mechanical verification of parameterized real-time systems [PhD thesis, Berlin Institute of Technology]. https://doi.org/10.14279/depositonce-3248

Groote, J. F., Jansen, D. N., Keiren, J. J. A., & Wijs, A. J. (2017). An O(mlog n) algorithm for computing stuttering equivalence and branching bisimulation. ACM Transactions on Computational Logic (TOCL), 18(2), 13:1–13:34. https://doi.org/10.1145/3060140

Groote, J. F., & Martens, J. (2024). A quadratic lower bound for simulation. https://doi.org/10.48550/arXiv.2411.14067

Groote, J. F., Martens, J., & Vink, Erik. P. de. (2023). Lowerbounds for bisimulation by partition refinement. Logical Methods in Computer Science, Volume 19, Issue 2. https://doi.org/10.46298/lmcs-19(2:10)2023

Groote, J. F., & Mousavi, M. R. (2014). Modelling and analysis of communicating systems. MIT Press. https://doi.org/10.7551/mitpress/9946.001.0001

Hauschild, J. (2023). Nonlinear counterfactuals in Isabelle/HOL [Bachelor's thesis, Technische Universität Berlin]. https://github.com/johanneshauschild/NonlinearCounterfactuals

Hennessy, M., & Milner, R. (1980). On observing nondeterminism and concurrency. In J. W. de Bakker & J. van Leeuwen (Eds.), LNCS: Vol. 85. Automata, languages and programming (pp. 299–309). Springer. https://doi.org/10.1007/3-540-10003-2_79

Hoare, C. A. R. (1985). Communicating sequential processes. Prentice-Hall, Inc.

Hoare, C. A. R. (2006). Why ever CSP? Electronic Notes in Theoretical Computer Science, 162, 209–215. https://doi.org/10.1016/j.entcs.2006.01.031

Horne, R., Mauw, S., & Yurkov, S. (2023). When privacy fails, a formula describes an attack: A complete and compositional verification method for the applied π-calculus. Theoretical Computer Science, 959, 113842. https://doi.org/10.1016/j.tcs.2023.113842

Hülsbusch, M., König, B., Küpper, S., & Stoltenow, L. (2020). Conditional Bisimilarity for Reactive Systems. In Z. M. Ariola (Ed.), LIPIcs: Vol. 167. 5th international conference on formal structures for computation and deduction (FSCD 2020) (pp. 10:1–10:19). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSCD.2020.10

Hüttel, H., & Shukla, S. (1996). On the complexity of deciding behavioural equivalences and preorders. A survey (BRICS RS-96-39H). University of Aarhus. https://doi.org/10.7146/brics.v3i39.20021

Kanellakis, P. C., & Smolka, S. A. (1983). CCS expressions, finite state processes, and three problems of equivalence. PODC ’83, 228–240. https://doi.org/10.1145/800221.806724

Keiren, J. J. A., & Willemse, T. A. C. (2024). It’s all a game. In V. Capretta, R. Krebbers, & F. Wiedijk (Eds.), Logics and type systems in theory and practice: Essays dedicated to Herman Geuvers on the occasion of his 60th birthday (pp. 150–167). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-61716-4_10

König, B., Mika-Michalski, C., & Schröder, L. (2020). Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In D. Petrişan & J. Rot (Eds.), LNCS: Vol. 12094. Coalgebraic methods in computer science: CMCS (pp. 133–154). Springer. https://doi.org/10.1007/978-3-030-57201-3_8

Kruskal, J. B. (1972). The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3), 297–305. https://doi.org/10.1016/0097-3165(72)90063-5

Kučera, A., & Esparza, J. (1999). A logical viewpoint on process-algebraic quotients. In J. Flum & M. Rodriguez-Artalejo (Eds.), LNCS: Vol. 1683. Computer science logic: CSL (pp. 499–514). Springer. https://doi.org/10.1007/3-540-48168-0_35

Kupferman, O., & Shamash Halevy, N. (2022). Energy Games with Resource-Bounded Environments. In B. Klin, S. Lasota, & A. Muscholl (Eds.), LIPIcs: Vol. 243. 33rd international conference on concurrency theory (CONCUR 2022) (pp. 19:1–19:23). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.19

Kurzan, T. (2024). Implementierung eines Contrasimilarity-Checkers für mCRL2 [Bachelor's thesis]. Technische Universität Berlin.

Lange, M., Lozes, E., & Vargas Guzmán, M. (2014). Model-checking process equivalences. Theoretical Computer Science, 560(3), 326–347. https://doi.org/10.1016/j.tcs.2014.08.020

Lê, H. N. (2020). Implementing coupled similarity as an automated checker for mCRL2 [Bachelor's thesis]. Technische Universität Berlin.

Lemke, C. (2024). A formal proof of decidability of multi-weighted declining energy games [Master’s thesis, Technische Universität Berlin]. https://github.com/crmrtz/galois-energy-games/blob/main/master-thesis/masters_thesis.pdf

Lönne, B. (2023). An educational computer game about counterfactual truth conditions [Bachelor's thesis, Technische Universität Berlin]. https://github.com/Brunololos/counterfactuals-demo

Martens, J., & Groote, J. F. (2023). Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. In G. A. Pérez & J.-F. Raskin (Eds.), LIPIcs: Vol. 279. 34th international conference on concurrency theory (CONCUR 2023) (pp. 32:1–32:17). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.32

Martens, J., & Groote, J. F. (2024). Minimal depth distinguishing formulas without until for branching bisimulation. In V. Capretta, R. Krebbers, & F. Wiedijk (Eds.), Logics and type systems in theory and practice: Essays dedicated to Herman Geuvers on the occasion of his 60th birthday (pp. 188–202). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-61716-4_12

Mattes, K. P. P. (2024). Measuring expressive power of HML formulas in Isabelle/HOL [Bachelor's thesis, Technische Universität Berlin]. https://github.com/ekeln/BA_formula_prices/raw/main/output/outline.pdf

Mayr, R. (2000). Process rewrite systems. Information and Computation, 156(1), 264–286. https://doi.org/10.1006/inco.1999.2826

Milner, R. (1980). LNCS: Vol. 92. A calculus of communicating systems. Springer. https://doi.org/10.1007/3-540-10235-3

Milner, R. (1989). Communication and concurrency. Prentice-Hall, Inc.

Mohri, M. (2002). Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics, 7(3), 321–350. https://doi.org/10.25596/jalc-2002-321

Montanari, L. (2021). Kontrasimulation als Spiel [Bachelor's thesis, Technische Universität Berlin]. https://github.com/luisamontanari/ContrasimGame

Nestmann, U., & Pierce, B. C. (2000). Decoding choice encodings. Information and Computation, 163(1), 1–59. https://doi.org/10.1006/inco.2000.2868

Ozegowski, F. (2023). Integration eines generischen Äquivalenzprüfers in CAAL [Bachelor's thesis, Technische Universität Berlin]. https://github.com/Fabian-O01/CAAL

Paige, R., & Tarjan, R. E. (1987). Three partition refinement algorithms. SIAM Journal on Computing, 16(6), 973–989. https://doi.org/10.1137/0216062

Parrow, J., & Sjödin, P. (1992). Multiway synchronization verified with coupled simulation. In W. R. Cleaveland (Ed.), CONCUR ’92: Third international conference on concurrency theory stony brook, NY, USA, august 24–27, 1992 proceedings (pp. 518–533). Springer. https://doi.org/10.1007/BFb0084813

Peacock, D. A. (2020). Process equivalences as a video game [Bachelor's thesis, Technische Universität Berlin]. https://drive.google.com/drive/folders/19YuOCXI_7CEB4p9fgr6kDKCTbFwx2VU9

Peterson, G. L. (1981). Myths about the mutual exclusion problem. Inf. Process. Lett., 12, 115–116. https://doi.org/10.1016/0020-0190(81)90106-X

Pohlmann, M. (2021). Reducing strong reactive bisimilarity to strong bisimilarity [Bachelor's thesis, Technische Universität Berlin]. https://maxpohlmann.github.io/Reducing-Reactive-to-Strong-Bisimilarity/thesis.pdf

Ranzato, F., & Tapparo, F. (2010). An efficient simulation algorithm based on abstract interpretation. Information and Computation, 208(1), 1–22. https://doi.org/10.1016/j.ic.2009.06.002

Reed, J. N., Roscoe, A. W., & Sinclair, J. E. (2007). Responsiveness and stable revivals. Formal Aspects of Computing, 19, 303–319. https://doi.org/10.1007/s00165-007-0032-9

Reichert, J. M. (2020). Visualising and model checking counterfactuals [Bachelor's thesis]. Technische Universität Berlin.

Roscoe, A. W. (2009). Revivals, stuckness and the hierarchy of CSP models. Journal of Logic and Algebraic Programming, 78(3), 163–190. https://doi.org/10.1016/j.jlap.2008.10.002

Sandt, E. (2022). A video game about reactive bisimilarity [Bachelor's thesis, Technische Universität Berlin]. https://github.com/eloinoel/ReactiveBisimilarityGame

Sangiorgi, D. (1996). A theory of bisimulation for the π-calculus. Acta Informatica, 33(1), 69–97. https://doi.org/10.1007/s002360050036

Sangiorgi, D. (2012). Introduction to bisimulation and coinduction. Cambridge University Press. https://doi.org/10.1017/CBO9780511777110

Shukla, S. K., Hunt III, H. B., & Rosenkrantz, D. J. (1996). HORNSAT, model checking, verification and games: Extended abstract. In R. Alur & T. A. Henzinger (Eds.), LNCS: Vol. 1102. Computer aided verification: CAV (pp. 99–110). Springer. https://doi.org/10.1007/3-540-61474-5_61

Spork, T., Baier, C., Katoen, J.-P., Piribauer, J., & Quatmann, T. (2024). A Spectrum of Approximate Probabilistic Bisimulations. In R. Majumdar & A. Silva (Eds.), LIPIcs: Vol. 311. 35th international conference on concurrency theory (CONCUR 2024) (pp. 37:1–37:19). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2024.37

Steffen, B. (1989). Characteristic formulae. In G. Ausiello, M. Dezani-Ciancaglini, & S. R. Della Rocca (Eds.), Automata, languages and programming (pp. 723–732). Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0035794

Stirling, C. (1996). Modal and temporal logics for processes. In F. Moller & G. Birtwistle (Eds.), LNCS: Vol. 1043. Logics for concurrency: Structure versus automata (pp. 149–237). Springer. https://doi.org/10.1007/3-540-60915-6_5

Stöcker, V. (2024). Higher-order diadic µ-calculus—an efficient framework for checking process equivalences? [Bachelor's thesis]. Technische Universität Berlin.

Straßnick, T., & Ozegowski, F. (2024). Integration of the weak spectroscopy into CAAL. Technische Universität Berlin. https://github.com/equivio/CAAL/blob/spectroscopy/docs/CAAL_weak_Spectroscopy.pdf

Tan, L. (2002a). An abstract schema for equivalence-checking games. In A. Cortesi (Ed.), LNCS: Vol. 2294. Verification, model checking, and abstract interpretation, third international workshop, VMCAI 2002, venice, italy, january 21-22, 2002, revised papers (pp. 65–78). Springer. https://doi.org/10.1007/3-540-47813-2_5

Tan, L. (2002b). Evidence-based verification. State University of New York at Stony Brook. https://www.researchgate.net/publication/277283542_Evidence-Based_Verification

Trzeciakiewicz, M. (2021). Linear-time–branching-time spectroscopy as an educational web browser game [Bachelor's thesis, Technische Universität Berlin]. https://github.com/Marii19/the-spectroscopy-invaders

Valmari, A. (2009). Bisimilarity minimization in o(m logn) time. In G. Franceschinis & K. Wolf (Eds.), Applications and theory of petri nets (pp. 123–142). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-02424-5_9

Valmari, A. (2020). All congruences below stability-preserving fair testing or CFFD. Acta Informatica, 57(3), 353–383. https://doi.org/10.1007/s00236-019-00364-4

van Glabbeek, R. J. (1990). The linear time–branching time spectrum: Extended abstract. In J. C. M. Baeten & J. W. Klop (Eds.), LNCS: Vol. 458. CONCUR’90 (pp. 278–297). Springer. https://doi.org/10.1007/BFb0039066

van Glabbeek, R. J. (1993). The linear time–branching time spectrum II: The semantics of sequential systems with silent moves; extended abstract. In E. Best (Ed.), LNCS: Vol. 715. CONCUR’93 (pp. 66–81). Springer. https://doi.org/10.1007/3-540-57208-2_6

van Glabbeek, R. J. (2001). The linear time–branching time spectrum I: The semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra (pp. 3–99). Elsevier. https://doi.org/10.1016/B978-044482830-9/50019-9

van Glabbeek, R. J. (2023). Modelling mutual exclusion in a process algebra with time-outs. Information and Computation, 294, 105079. https://doi.org/10.1016/j.ic.2023.105079

van Glabbeek, R. J., & Weijland, W. P. (1996). Branching time and abstraction in bisimulation semantics. Journal of the ACM (JACM), 43(3), 555–600. https://doi.org/10.1145/233551.233556

Vogel, G. (2024). Accelerating process equivalence energy games using WebGPU [Bachelor's thesis, Technische Universität Berlin]. https://github.com/Gobbel2000/gpuequiv

Voorhoeve, M., & Mauw, S. (2001). Impossible futures and determinism. Information Processing Letters, 80(1), 51–58. https://doi.org/10.1016/S0020-0190(01)00217-4

Wenzel, M. (2025). The Isabelle/Isar reference manual. https://isabelle.in.tum.de/dist/Isabelle2025/doc/isar-ref.pdf

Wimmer, R. (2011). Symbolische Methoden für die probabilistische Verifikation – Zustandsraumreduktion und Gegenbeispiele [Dissertation, Albert-Ludwigs-Universität Freiburg]. https://freidok.uni-freiburg.de/data/7932

Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., & Becker, B. (2006). Sigref: A symbolic bisimulation tool box. In S. Graf & W. Zhang (Eds.), Automated technology for verification and analysis: 4th international symposium, ATVA 2006, beijing, china, october 23-26, 2006. proceedings (pp. 477–492). Springer. https://doi.org/10.1007/11901914_35

Wißmann, T., Milius, S., & Schröder, L. (2021). Explaining Behavioural Inequivalence Generically in Quasilinear Time. In S. Haddad & D. Varacca (Eds.), LIPIcs: Vol. 203. 32nd international conference on concurrency theory (CONCUR 2021) (pp. 32:1–32:18). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2021.32

Wittig, T. (2020). Charting the jungle of process calculi encodings [Bachelor's thesis, Technische Universität Berlin]. https://concurrency-theory.org/process-jungle/

Wortmann, J. K., Olesen, S. R., & Enevoldsen, S. (2015). CAAL 2.0 – recursive HML, distinguishing formulae, equivalence collapses and parallel fixed-point computations (Vol. DES103F15) [Student project supervised by Jiří Srba and Kim Guldstrand Larsen]. Aalborg University. https://caal.cs.aau.dk/docs/CAAL2_RDEP.pdf

Wrusch, M. (2020). Ein Computerspiel zum Erlernen von Verhaltensäquivalenzen [Bachelor's thesis]. Technische Universität Berlin.

Zielonka, W. (1998). Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1), 135–183. https://doi.org/10.1016/S0304-3975(98)00009-7