References
Adler, R. (2022). Simulation fehlertoleranter
Konsensalgorithmen in Hash.ai [Bachelor's Thesis]. Technische
Universität Berlin.
Alshukairi, Z. (2022). Automatisierte Reduktion von
reaktiver zu starker Bisimilarität [Bachelor's
Thesis]. Technische Universität Berlin.
Babai, L. (2016). Graph isomorphism in quasipolynomial time [extended
abstract]. Proceedings of the Forty-Eighth Annual ACM Symposium on
Theory of Computing, 684–697. https://doi.org/10.1145/2897518.2897542
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
Bell, C. J. (2013). Certifiably sound parallelizing transformations. In
International conference on certified programs and proofs (pp.
227–242). Springer.
Bisping, B. (2018). Computing coupled similarity [Master’s
thesis, Technische Universität Berlin]. https://coupledsim.bbisping.de/bisping_computingCoupledSimilarity_thesis.pdf
Bisping, B. (2023a). 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. (2023b). Process equivalence problems as energy
games. 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.), 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.), Proceedings
Combined 31st International Workshop on expressiveness in
concurrency and 21st Workshop on structural
operational semantics, Calgary, Canada, 9th September
2024 (Vol. 412, pp. 71–88). Open Publishing Association. https://doi.org/10.4204/EPTCS.412.6
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.), Proceedings Combined 28th International Workshop
on expressiveness in concurrency and 18th
Workshop on structural operational semantics (Vol. 339, 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.), Tools and algorithms for the
construction and analysis of systems: TACAS (Vol.
11427, 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.), Tools and algorithms for the construction and
analysis of systems: TACAS (Vol. 12651, 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
Bulik, J. (2021). Statically analysing inter-process communication
in Elixir programs [Bachelor's Thesis, Technische
Universität Berlin]. https://gitlab.com/MrGreenTea/stille-post
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
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
Glabbeek, R. J. van. (1990). The linear time–branching time spectrum:
Extended abstract. In J. C. M. Baeten & J. W. Klop (Eds.),
CONCUR’90 (Vol. 458, pp. 278–297). Springer. https://doi.org/10.1007/BFb0039066
Glabbeek, R. J. van. (1993). The linear time–branching time spectrum
II: The semantics of sequential systems with silent moves;
extended abstract. In E. Best (Ed.), CONCUR’93 (Vol. 715, pp.
66–81). Springer. https://doi.org/10.1007/3-540-57208-2_6
Glabbeek, R. J. van. (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
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., & 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
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.),
Automata, languages and programming (Vol. 85, pp. 299–309).
Springer. https://doi.org/10.1007/3-540-10003-2_79
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
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.), Computer science logic: CSL (Vol. 1683, 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.), 33rd international
conference on concurrency theory (CONCUR 2022) (Vol. 243, 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.
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.
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
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
Milner, R. (1989). Communication and concurrency.
Prentice-Hall, Inc.
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.
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
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
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. (2012). Introduction to bisimulation and
coinduction. Cambridge University Press. https://doi.org/10.1017/CBO9780511777110
Stirling, C. (1996). Modal and temporal logics for processes. In F.
Moller & G. Birtwistle (Eds.), Logics for concurrency: Structure
versus automata (Vol. 1043, 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.
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
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
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). 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/https://doi.org/10.1016/S0304-3975(98)00009-7