@inproceedings(bctbc2008cfpPda,
 author       = {J.~C.~M. Baeten and P.~J.~L. Cuijpers and P.~J.~A. van Tilburg},
 year         = {2008},
 title        = {A Context-Free Process as a Pushdown Automaton},
 editor       = {Franck van Breugel and Marsha Chechik},
 booktitle    = {CONCUR 2008 - Concurrency Theory},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {98--113},
 doi          = {10.1007/978-3-540-85361-9\_11},
)
@incollection(bell_certifiably_2013,
 author       = {Christian~J. Bell},
 year         = {2013},
 title        = {Certifiably sound parallelizing transformations},
 editor       = {Georges Gonthier and Michael Norrish},
 booktitle    = {Certified Programs and Proofs},
 volume       = {8307},
 publisher    = {Springer International Publishing},
 pages        = {227--242},
 doi          = {10.1007/978-3-319-03545-1\_15},
)
@misc(bisping2019isabelle,
 author       = {Benjamin Bisping},
 year         = {2019},
 title        = {Isabelle/HOL proof and Apache Flink program for TACAS 2019 paper: Computing Coupled Similarity},
 doi          = {10.6084/m9.figshare.7831382.v1},
)
@inproceedings(bn2019coupledsimTacas,
 author       = {Benjamin Bisping and Uwe Nestmann},
 year         = {2019},
 title        = {Computing coupled similarity},
 booktitle    = {Proceedings of {TACAS}},
 series       = {LNCS},
 publisher    = {Springer},
 pages        = {244--261},
 doi          = {10.1007/978-3-030-17462-0\_14},
)
@inproceedings(bn2021ltbtspectroscope,
 author       = {Benjamin Bisping and Uwe Nestmann},
 year         = {2021},
 title        = {A Game for Linear-time--Branching-time Spectroscopy},
 editor       = {Jan~Friso Groote and Kim~Guldstrand Larsen},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {3--19},
 doi          = {10.1007/978-3-030-72016-2\_1},
)
@article(bisping2020coupled32,
 author       = {Benjamin Bisping and Uwe Nestmann and Kirstin Peters},
 year         = {2020},
 title        = {Coupled similarity: the first 32 years},
 journal      = {Acta Informatica},
 volume       = {57},
 number       = {3},
 pages        = {439--463},
 doi          = {10.1007/s00236-019-00356-4},
)
@incollection(ramalingam_game_2008,
 author       = {Xin Chen and Yuxin Deng},
 year         = {2008},
 title        = {Game characterizations of process equivalences},
 editor       = {G.~Ramalingam},
 booktitle    = {Programming Languages and Systems},
 volume       = {5356},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {107--121},
 doi          = {10.1007/978-3-540-89330-1\_8},
)
@article(escrig_games_2017,
 author       = {David De~Frutos Escrig and Jeroen J.~A. Keiren and Tim A.~C. Willemse},
 year         = {2017},
 title        = {Games for bisimulations and abstraction},
 journal      = {Logical Methods in Computer Science},
 volume       = {13},
 number       = {4},
 pages        = {1--40},
 doi          = {10.23638/LMCS-13(4:15)2017},
)
@article(fg2005hierarchy,
 author       = {C{\'e}dric Fournet and Georges Gonthier},
 year         = {2005},
 title        = {A hierarchy of equivalences for asynchronous calculi},
 journal      = {The Journal of Logic and Algebraic Programming},
 volume       = {63},
 number       = {1},
 pages        = {131--173},
 doi          = {10.1016/j.jlap.2004.01.006},
)
@inproceedings(van1993linear,
 author       = {Rob~J. van Glabbeek},
 year         = {1993},
 title        = {The linear time--branching time spectrum II},
 booktitle    = {International Conference on Concurrency Theory},
 organization = {Springer},
 pages        = {66--81},
 doi          = {10.1007/3-540-57208-2\_6},
)
@incollection(van2001linear,
 author       = {Rob~J. van Glabbeek},
 year         = {2001},
 title        = {The linear time--branching time spectrum I. The semantics of concrete, sequential processes},
 booktitle    = {Handbook of Process Algebra},
 publisher    = {Elsevier},
 pages        = {3--99},
 doi          = {10.1016/B978-044482830-9/50019-9},
)
@incollection(graedel2007finite,
 author       = {Gr\IeC{\"a}del, Erich},
 year         = {2007},
 title        = {Finite model theory and descriptive complexity},
 booktitle    = {Finite Model Theory and its Applications},
 publisher    = {Springer},
 pages        = {125--230},
 doi          = {10.1007/3-540-68804-8\_3},
)
@mastersthesis(deHoop2017cfpPdp,
 author       = {Zeno de~Hoop},
 year         = {2017},
 title        = {Context-Free Processes and Push-Down Processes},
 school       = {Universiteit van Amsterdam},
 url          = {https://eprints.illc.uva.nl/id/eprint/1561},
)
@article(hs1996complexityEquivalences,
 author       = {H\IeC{\"u}ttel, Hans and Sandeep Shukla},
 year         = {1996},
 title        = {On the Complexity of Deciding Behavioural Equivalences and Preorders. A Survey},
 journal      = {BRICS Report Series},
 volume       = {3},
 number       = {39},
 doi          = {10.7146/brics.v3i39.20021},
)
@book(milner1989communication,
 author       = {Robin Milner},
 year         = {1989},
 title        = {Communication and Concurrency},
 series       = {{PHI} Series in computer science},
 publisher    = {Prentice Hall Englewood Cliffs},
)
@inproceedings(parrow1994complete,
 author       = {Joachim Parrow and Peter Sj{\"o}din},
 year         = {1994},
 title        = {The complete axiomatization of Cs-congruence},
 booktitle    = {Annual Symposium on Theoretical Aspects of Computer Science},
 organization = {Springer},
 pages        = {555--568},
 doi          = {10.1007/3-540-57785-8\_171},
)
@inproceedings(pg15encodability,
 author       = {Kirstin Peters and Rob~J. van Glabbeek},
 year         = {2015},
 title        = {Analysing and Comparing Encodability Criteria},
 booktitle    = {Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, and 12th Workshop on Structural Operational Semantics, {EXPRESS/SOS}},
 pages        = {46--60},
 doi          = {10.4204/EPTCS.190.4},
)
@article(pg15afp,
 author       = {Kirstin Peters and Rob~J. van Glabbeek},
 year         = {2015},
 title        = {Analysing and Comparing Encodability Criteria for Process Calculi},
 journal      = {Archive of Formal Proofs},
 note         = {\url{https://isa-afp.org/entries/Encodability_Process_Calculi.html}, Formal proof development},
)
@article(stirling1999bisimulation,
 author       = {Colin Stirling},
 year         = {1999},
 title        = {Bisimulation, modal logic and model checking games},
 journal      = {Logic Journal of IGPL},
 volume       = {7},
 number       = {1},
 pages        = {103--124},
 doi          = {10.1093/jigpal/7.1.103},
)
@article(voorhoeve_impossible_2001,
 author       = {Marc Voorhoeve and Sjouke Mauw},
 year         = {2001},
 title        = {Impossible futures and determinism},
 journal      = {Information Processing Letters},
 volume       = {80},
 number       = {1},
 pages        = {51--58},
 doi          = {10.1016/S0020-0190(01)00217-4},
)
@misc(wenzel2004isabelle,
 author       = {Makarius Wenzel},
 year         = {2021},
 title        = {The Isabelle/Isar Reference Manual},
 url          = {https://isabelle.in.tum.de/doc/isar-ref.pdf},
)