% Encoding: UTF-8

@InProceedings{hhk1995simulations,
  author    = {Monika Rauch Henzinger and Thomas A. Henzinger and Peter W. Kopke},
  title     = {Computing Simulations on Finite and Infinite Graphs},
  booktitle = {36th Annual Symposium on Foundations of Computer Science, Milwaukee, Wisconsin},
  year      = {1995},
  pages     = {453--462},
  doi       = {10.1109/SFCS.1995.492576},
}

@InProceedings{bell2013certifiably,
  author       = {Bell, Christian J.},
  title        = {Certifiably sound parallelizing transformations},
  booktitle    = {International Conference on Certified Programs and Proofs},
  year         = {2013},
  pages        = {227--242},
  organization = {Springer},
}

@Article{brr2016,
  author    = {Boulgakov, Alexandre and Gibson-Robinson, Thomas and Roscoe, A.~W.},
  title     = {Computing maximal weak and other bisimulations},
  journal   = {Formal Aspects of Computing},
  year      = {2016},
  volume    = {28},
  number    = {3},
  pages     = {381--407},
  issn      = {1433-299X},
  abstract  = {We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.},
  doi       = {10.1007/s00165-016-0366-2},
  file      = {:algorithms/brr2016_computing-maximal-weak-and-other-bisimulations.pdf:PDF},
  timestamp = {2017.06.17},
}

@Article{ch1993,
  Title                    = {Testing equivalence as a bisimulation equivalence},
  Author                   = {Cleaveland, Rance and Hennessy, Matthew},
  Journal                  = {Formal Aspects of Computing},
  Year                     = {1993},
  Number                   = {1},
  Pages                    = {1--20},
  Volume                   = {5},
  Publisher                = {Springer}
}

@Article{dpp2004,
  author    = {Agostino Dovier and Carla Piazza and Alberto Policriti},
  title     = {An efficient algorithm for computing bisimulation equivalence},
  journal   = {Theoretical Computer Science},
  year      = {2004},
  volume    = {311},
  number    = {1},
  pages     = {221--256},
  issn      = {0304-3975},
  doi       = {10.1016/S0304-3975(03)00361-X},
  file      = {:algorithms/dpp2004_efficient-algorithm-bisimulation.pdf:PDF},
  keywords  = {Bisimulation},
  owner     = {ben},
  timestamp = {2017.06.19},
}

@InCollection{glabbeek2017,
author="van Glabbeek, Rob",
editor={Gibson-Robinson, Thomas
and Hopcroft, Philippa
and Lazi{\'{c}}, Ranko},
title={A Branching Time Model of {CSP}},
      bookTitle="Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday",
year="2017",
publisher="Springer International Publishing",
address="Cham",
pages={272--293},
isbn="978-3-319-51046-0",
doi={10.1007/978-3-319-51046-0\_14}
}



@Article{nestmann1996decoding,
  author    = {Nestmann, Uwe and Pierce, Benjamin C.},
  title     = {Decoding choice encodings},
  journal   = {Information and Computation},
  year      = {2000},
  volume    = {163},
  number    = {1},
  pages     = {1--59},
  publisher = {Elsevier},
  doi		= {10.1006/inco.2000.2868},
}

@InProceedings{parrow1992,
  Title                    = {Multiway synchronization verified with coupled simulation},
  Author                   = {Parrow, Joachim and Sj{\"o}din, Peter},
  Booktitle                = {CONCUR '92: Third International Conference on Concurrency Theory Stony Brook, NY, USA, August 24--27, 1992 Proceedings},
  Year                     = {1992},
  Editor                   = {Cleaveland, W.R.},
  Pages                    = {518--533},
  Publisher                = {Springer Berlin Heidelberg},

  Doi                      = {10.1007/BFb0084813},
  File                     = {:parrow1992_coupled-simulation.pdf:PDF},
  ISBN                     = {978-3-540-47293-3},
  Owner                    = {ben},
  Timestamp                = {2017.06.19}
}

@InProceedings{ps1994,
  Title                    = {The complete axiomatization of {Cs}-congruence},
  Author                   = {Parrow, Joachim and Sj{\"o}din, Peter},
  Booktitle                = {STACS 94: 11th Annual Symposium on Theoretical Aspects of Computer Science Caen, France, February 24--26, 1994 Proceedings},
  Year                     = {1994},
  Editor                   = {Enjalbert, Patrice and Mayr, Ernst W. and Wagner, Klaus W.},
  Pages                    = {555--568},
  Publisher                = {Springer Berlin Heidelberg},

  Doi                      = {10.1007/3-540-57785-8\_171},
  File                     = {:ps1994_complete-axiomatization-of-cs.pdf:PDF},
  ISBN                     = {978-3-540-48332-8},
  Owner                    = {ben},
  Timestamp                = {2017.06.19}
}

@Book{sangiorgi2012,
  Title                    = {Introduction to Bisimulation and Coinduction},
  Author                   = {Sangiorgi, Davide},
  Publisher                = {Cambridge University Press},
  Year                     = {2012},

  Address                  = {New York, NY, USA},

  ISBN                     = {1107003636, 9781107003637}
}

@Article{vm2001impossible,
  Title                    = {Impossible futures and determinism},
  Author                   = {Voorhoeve, Marc and Mauw, Sjouke},
  Journal                  = {Information Processing Letters},
  Year                     = {2001},
  Number                   = {1},
  Pages                    = {51--58},
  Volume                   = {80},
  doi					   = {10.1016/S0020-0190(01)00217-4},
  File                     = {:vm2000_impossible-futures-and-determinism.pdf:PDF},
  Publisher                = {Elsevier}
}

@InProceedings{km2002,
  author    = {Ku{\v{c}}era, Anton{\'i}n and Mayr, Richard},
  title     = {Why Is Simulation Harder than Bisimulation?},
  booktitle = {CONCUR 2002 --- Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20--23, 2002 Proceedings},
  year      = {2002},
  editor    = {Brim, Lubo{\v{s}} and K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r and Ku{\v{c}}era, Anton{\'i}n and Jan{\v{c}}ar, Petr},
  pages     = {594--609},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {Why is deciding simulation preorder (and simulation equivalence) computationally harder than deciding bisimulation equivalence on almost all known classes of processes? We try to answer this question by describing two general methods that can be used to construct direct one-to-one polynomial-time reductions from bisimulation equivalence to simulation preorder (and simulation equivalence). These methods can be applied to many classes of finitely generated transition systems, provided that they satisfy certain abstractly formulated conditions. Roughly speaking, our first method works for all classes of systems that can test for `non-enabledness' of actions, while our second method works for all classes of systems that are closed under synchronization.},
  doi       = {10.1007/3-540-45694-5\_39},
  file      = {:km2002_why-is-simulation-harder-than-bisimulation.pdf:PDF},
  isbn      = {978-3-540-45694-0},
}

@InProceedings{gs2013simulations,
  author       = {Gor{\'i}n, Daniel and Schr{\"o}der, Lutz},
  title        = {Simulations and bisimulations for coalgebraic modal logics},
  booktitle    = {International Conference on Algebra and Coalgebra in Computer Science},
  year         = {2013},
  pages        = {253--266},
  organization = {Springer},
  file         = {:gs2013_simulations_bisimulations_coalgebraic_modal_logics.pdf:PDF},
}

@InProceedings{gp15,
  author    = {Kirstin Peters and Rob J. van Glabbeek},
  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}},
  year      = {2015},
  pages     = {46--60},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/PetersG15},
  doi       = {10.4204/EPTCS.190.4},
  timestamp = {Wed, 03 May 2017 14:47:58 +0200},
}

@TechReport{vm2000impossibleReport,
  author      = {Voorhoeve, Marc and Mauw, Sjouke},
  title       = {Impossible futures and determinism},
  institution = {Technische Universiteit Eindhoven},
  year        = {2000},
  type        = {Computing science reports},
  number      = {Vol. 0014},
  address     = {Eindhoven},
  file        = {:vm2000_impossible-futures-and-determinism.pdf:PDF},
  journal     = {Computing science reports},
  volume      = {0014},
}

@Article{ks2006,
  author    = {Ku{\v{c}}era, Anton{\'\i}n and Schnoebelen, Philippe},
  title     = {A general approach to comparing infinite-state systems with their finite-state specifications},
  journal   = {Theoretical Computer Science},
  year      = {2006},
  volume    = {358},
  number    = {2-3},
  pages     = {315--333},
  publisher = {Elsevier},
}

@InProceedings{whhsb2006sigref,
  author    = {Wimmer, Ralf and Herbstritt, Marc and Hermanns, Holger and Strampp, Kelley and Becker, Bernd},
  title     = {Sigref: {A} Symbolic Bisimulation Tool Box},
  booktitle = {Automated Technology for Verification and Analysis: 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings},
  year      = {2006},
  editor    = {Graf, Susanne and Zhang, Wenhui},
  pages     = {477--492},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.},
  doi       = {10.1007/11901914\_35},
  isbn      = {978-3-540-47238-4},
}

@Article{Fournet2005,
  author    = {Fournet, C{\'e}dric and Gonthier, Georges},
  title     = {A hierarchy of equivalences for asynchronous calculi},
  journal   = {The Journal of Logic and Algebraic Programming},
  year      = {2005},
  volume    = {63},
  number    = {1},
  pages     = {131--173},
  publisher = {Elsevier},
}

@InProceedings{gp2008,
  author       = {van Glabbeek, Rob J. and Ploeger, Bas},
  title        = {Correcting a space-efficient simulation algorithm},
  booktitle    = {International Conference on Computer Aided Verification},
  year         = {2008},
  pages        = {517--529},
  organization = {Springer},
  file         = {:algorithms/gb2008_correcting-gpp2003.pdf:PDF},
}

@Article{gpp2003,
  author    = {Gentilini, Raffaella and Piazza, Carla and Policriti, Alberto},
  title     = {From bisimulation to simulation: Coarsest partition problems},
  journal   = {Journal of Automated Reasoning},
  year      = {2003},
  volume    = {31},
  number    = {1},
  pages     = {73--103},
  file      = {:algorithms/gpp2003_from-bisim-to-sim-coarsest-partition-problems.pdf:PDF},
  publisher = {Springer},
}

@InProceedings{glabbeek1993ltbt,
  author       = {Rob J. van Glabbeek},
  title        = {The linear time--branching time spectrum {II}},
  booktitle    = {International Conference on Concurrency Theory},
  year         = {1993},
  pages        = {66--81},
  organization = {Springer},
}

@Article{nc1994bisimulationGamesLogic,
  author    = {Nielsen, Mogens and Clausen, Christian},
  title     = {Bisimulation, games, and logic},
  journal   = {Results and trends in theoretical computer science},
  year      = {1994},
  pages     = {289--306},
  publisher = {Springer},
}

@TechReport{stirling1993modal,
  author       = {Stirling, Colin},
  title        = {Modal and temporal logics for processes},
  institution  = {Department of Computer Science, University of Edinburgh},
  year         = {1993},
  organization = {Citeseer},
}

@Article{kripke1963semanticalModal,
  author  = {Kripke, Saul A.},
  title   = {{Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi}},
  journal = {Mathematical Logic Quarterly},
  year    = {1963},
  volume  = {9},
  number  = {5-6},
  pages   = {67--96},
  file    = {:bib/kripke1963semanticalModal.pdf:PDF},
}

@Article{hennessy1985hml,
  author    = {Hennessy, Matthew and Milner, Robin},
  title     = {Algebraic laws for nondeterminism and concurrency},
  journal   = {Journal of the ACM (JACM)},
  year      = {1985},
  volume    = {32},
  number    = {1},
  pages     = {137--161},
  publisher = {ACM},
}

@InCollection{graedel2007finite,
  author    = {Erich Gr{\"a}del},
  title     = {Finite Model Theory and Descriptive Complexity},
  booktitle = {Finite Model Theory and Its Applications},
  publisher = {Springer Berlin Heidelberg},
  year      = {2007},
  editor    = {Gr{\"a}del, E. and Kolaitis, P.G. and Libkin, L. and Marx, M. and Spencer, J. and Vardi, M.Y. and Venema, Y. and Weinstein, S.},
  series    = {Texts in Theoretical Computer Science. An EATCS Series},
  pages     = {125--230},
  isbn      = {9783540688044},
  lccn      = {2007923182},
}

@InCollection{sepLogicGames,
  author       = {Hodges, Wilfrid},
  title        = {Logic and Games},
  booktitle    = {The Stanford Encyclopedia of Philosophy},
  publisher    = {Metaphysics Research Lab, Stanford University},
  year         = {2013},
  editor       = {Edward N. Zalta},
  edition      = {Spring 2013},
  howpublished = {\url{https://plato.stanford.edu/archives/spr2013/entries/logic-games/}},
}

@Unpublished{kreutzer2016,
  author = {Stephan Kreutzer},
  title  = {Logic, Games, Automata},
  note   = {Lecture notes},
  year   = {2016},
}

@InProceedings{ehstz2013quotients,
  author    = {Eisentraut, Christian and Hermanns, Holger and Schuster, Johann and Turrini, Andrea and Zhang, Lijun},
  title     = {The Quest for Minimal Quotients for Probabilistic Automata},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  year      = {2013},
  editor    = {Piterman, Nir and Smolka, Scott A.},
  pages     = {16--31},
  address   = {Berlin, Heidelberg},
  publisher = {Springer},
  abstract  = {One of the prevailing ideas in applied concurrency theory and verification is the concept of automata minimization with respect to strong or weak bisimilarity. The minimal automata can be seen as canonical representations of the behaviour modulo the bisimilarity considered. Together with congruence results wrt. process algebraic operators, this can be exploited to alleviate the notorious state space explosion problem. In this paper, we aim at identifying minimal automata and canonical representations for concurrent probabilistic models. We present minimality and canonicity results for probabilistic automata wrt. strong and weak bisimilarity, together with polynomial time minimization algorithms.},
  isbn      = {978-3-642-36742-7},
}

@PhdThesis{wimmer2011dissertation,
  author      = {Ralf Wimmer},
  title       = {{S}ymbolische {M}ethoden f{\"u}r die probabilistische {V}erifikation -- {Z}ustandsraumreduktion und {G}egenbeispiele},
  school      = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  year        = {2011},
  type        = {Dissertation},
  address     = {Freiburg im Breisgau, Germany},
  month       = jan,
  abstract    = {Discrete- and continuous-time Markov chains as well as interactive
	Markov chains are widely used model classes for the analysis of
	stochastic systems. A fundamental problem thereby is the number of
	states, which in general grows exponentially in the size of the
	corresponding high-level model.\par
	In this work we develop two methods to cope with this problem. The
	first one consists of the computation of a system with a minimal
	number of states and the same observable behavior as the original
	system. This allows us to carry out any analysis with well-known
	algorithms on the minimal system. Depending on the definition of
	observability we obtain different minimal systems. Our algorithm is
	able to handle a large number system types and minimization criteria
	which are considered practically relevant in the literature. Our
	method works with symbolic data structures and dedicated operations
	thereon whose runtime only depends on the size of the representation
	instead of the size of the represented system. The size of the
	symbolic representation of many real-world systems, however, is
	smaller by orders of magnitudes than the system itself. Experimental
	results prove the efficiency of our algorithm.\par
	The other method to handle large state spaces is to develop algorithms
	which are directly applicable to large systems. For the refutation of
	safety properties in digital circuits a method called Bounded Model
	Checking has been developed, which is nowadays successfully applied
	also in industry. We show how Bounded Model Checking can be adapted to
	compute counterexamples for discrete-time Markov chains if a given
	safety property is violated. By a number of optimization technique we
	can reduce not only the runtime but also the size of the
	counterexamples. The result is a method which is able to handle
	significantly larger systems than the previously available algorithms.},
  abstract_de = {Markow-Ketten mit diskreter und kontinuierlicher Zeit sowie interaktive Markow-Ketten sind weitverbreitete Modellklassen zur Analyse von stochastischen Systemen. Ein grundlegendes Problem bei ihrer Analyse ist die Anzahl der Zust{\"a}nde. Diese w{\"a}chst n{\"a}mlich im Allgemeinen exponentiell in der Gr{\"o}{\ss}e des zugeh{\"o}rigen Highlevel-Modells.\par Wir entwickeln in dieser Arbeit zwei Methoden, mit denen dieses Problem gel{\"o}st werden kann. Die erste besteht darin, zu jedem System dasjenige zu berechnen, das aus einer minimalen Anzahl von Zust{\"a}nden besteht und das dasselbe beobachtbare Verhalten wie das urspr{\"u}ngliche System aufweist. Danach kann die Analyse mit bekannten Algorithmen auf dem minimierten System durchgef{\"u}hrt werden. Abh{\"a}ngig von der Definition, welches Verhalten des Systems beobachtbar ist, erhalten wir verschiedene minimale Systeme. Unser Algorithmus ist in der Lage, eine ganze Reihe von Minimierungskriterien, die in der Literatur von Bedeutung sind, und Systemtypen zu ber{\"u}cksichtigen. Er arbeitet mit symbolischen Datenstrukturen und darauf angepassten Operationen, deren Laufzeit nur von der Gr{\"o}{\ss}e der Darstellung abh{\"a}ngt. F{\"u}r viele praktisch relevante Systeme ist diese um Gr{\"o}{\ss}enordnungen kleiner als die Gr{\"o}{\ss}e des dargestellten Systems. Experimentelle Ergebnisse belegen die Effzienz unseres Verfahrens.\par Die andere Methode, mit gro{\ss}en Zustandsr{\"a}umen umzugehen, ist, symbolische Algorithmen zur Analyse zu entwickeln, die direkt auf gro{\ss}e Systemen anwendbar sind. F{\"u}r die Fehlersuche in Schaltkreisen wird eine Methode namens Bounded Model Checking verwendet, die inzwischen auch industriell sehr erfolgreich eingesetzt wird. Wir zeigen, wie Bounded Model Checking zur Berechnung von Gegenbeispielen f{\"u}r Markow-Ketten eingesetzt werden kann, wenn diese eine vorgegebene Sicherheitseigenschaft verletzen. Durch eine Reihe von Optimierungen gelingt es uns, sowohl die Laufzeit zu reduzieren als auch die Gr{\"o}{\ss}e der Gegenbeispiele zu verringern. Das Resultat ist ein Verfahren, das deutlich gr{\"o}{\ss}ere Systeme als die bisher verf{\"u}gbaren expliziten Methoden handhaben kann.},
}

@Article{tarjan72stronglyconnected,
  author  = {Robert Tarjan},
  title   = {Depth-First Search and Linear Graph Algorithms},
  journal = {SIAM Journal on Computing},
  year    = {1972},
  volume  = {1},
  number  = {2},
  pages   = {146-160},
  doi     = {10.1137/0201010},
}

@Article{rt2008generalizingPT,
  author  = {Francesco Ranzato and Francesco Tapparo},
  title   = {Generalizing the {Paige--Tarjan} algorithm by abstract interpretation},
  journal = {Information and Computation},
  year    = {2008},
  volume  = {206},
  number  = {5},
  pages   = {620--651},
  issn    = {0890-5401},
  note    = {Special Issue: The 17th International Conference on Concurrency Theory (CONCUR 2006)},
  doi     = {https://doi.org/10.1016/j.ic.2008.01.001},
}

@Article{gjkw2017branching,
  author     = {Groote, Jan Friso and Jansen, David N. and Keiren, Jeroen J. A. and Wijs, Anton J.},
  title      = {An {$\bigo(m \log n)$} Algorithm for Computing Stuttering Equivalence and Branching Bisimulation},
  journal    = {ACM Transactions on Computational Logic (TOCL)},
  year       = {2017},
  volume     = {18},
  number     = {2},
  pages      = {13:1--13:34},
  issn       = {1529-3785},
  acmid      = {3060140},
  address    = {New York, NY, USA},
  articleno  = {13},
  doi        = {10.1145/3060140},
  issue_date = {June 2017},
  keywords   = {Branching bisimulation, algorithm},
  numpages   = {34},
  publisher  = {ACM},
}

@InProceedings{li2009weakbisim,
  author       = {Li, Weisong},
  title        = {Algorithms for computing weak bisimulation equivalence},
  booktitle    = {Theoretical Aspects of Software Engineering, 2009. TASE 2009. Third IEEE International Symposium on},
  year         = {2009},
  pages        = {241--248},
  organization = {IEEE},
}

@Book{milner1989comcon,
  title     = {Communication and Concurrency},
  publisher = {Prentice-Hall, Inc.},
  year      = {1989},
  author    = {Milner, Robin},
  address   = {Upper Saddle River, NJ, USA},
  isbn      = {0131149849},
}

@InProceedings{ph2015encodingCspCcs,
  author    = {Meike Hatzel and Christoph Wagner and Kirstin Peters and Uwe Nestmann},
  title     = {Encoding {CSP} into {CCS}},
  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}},
  year      = {2015},
  pages     = {61--75},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/bib/journals/corr/HatzelWPN15a},
  doi       = {10.4204/EPTCS.190.5},
  timestamp = {Wed, 03 May 2017 14:47:57 +0200},
}

@InProceedings{glabbeek1990ltbt1,
  author       = {Rob J. van Glabbeek},
  title        = {The linear time--branching time spectrum},
  booktitle    = {International Conference on Concurrency Theory},
  year         = {1990},
  pages        = {278--297},
  organization = {Springer},
}

@InCollection{ais2011algoBisim,
  pages      = {100--172},
  title      = {The algorithmics of bisimilarity},
  publisher  = {Cambridge University Press},
  year       = {2011},
  author     = {Aceto, Luca and Ingolfsdottir, Anna and Srba, Jiri},
  editor     = {Sangiorgi, Davide and Rutten, JanEditors},
  series     = {Cambridge Tracts in Theoretical Computer Science},
  booktitle  = {Advanced Topics in Bisimulation and Coinduction},
  collection = {Cambridge Tracts in Theoretical Computer Science},
  doi        = {10.1017/CBO9780511792588.004},
  place      = {Cambridge},
}

@Article{rt2010efficientSimulation,
  author    = {Ranzato, Francesco and Tapparo, Francesco},
  title     = {An efficient simulation algorithm based on abstract interpretation},
  journal   = {Information and Computation},
  year      = {2010},
  volume    = {208},
  number    = {1},
  pages     = {1--22},
  publisher = {Elsevier},
}

@Article{carbone2015flink,
  author    = {Carbone, Paris and Katsifodimos, Asterios and Ewen, Stephan and Markl, Volker and Haridi, Seif and Tzoumas, Kostas},
  title     = {Apache {F}link: Stream and batch processing in a single engine},
  journal   = {Bulletin of the IEEE Computer Society Technical Committee on Data Engineering},
  year      = {2015},
  volume    = {36},
  number    = {4},
  publisher = {IEEE Computer Society},
}

@Article{kalavri2018scatter-gather,
  author    = {Kalavri, Vasiliki and Vlassov, Vladimir and Haridi, Seif},
  title     = {High-Level Programming Abstractions for Distributed Graph Processing},
  journal   = {IEEE Transactions on Knowledge and Data Engineering},
  year      = {2018},
  volume    = {30},
  number    = {2},
  pages     = {305--324},
  publisher = {IEEE},
}

@Article{bo2003distBranchingSigref,
  author    = {Blom, Stefan and Orzan, Simona},
  title     = {Distributed branching bisimulation reduction of state spaces},
  journal   = {Electronic Notes in Theoretical Computer Science},
  year      = {2003},
  volume    = {89},
  number    = {1},
  pages     = {99--113},
  publisher = {Elsevier},
}

@InProceedings{luo2013bisimMapReduce,
  author       = {Luo, Yongming and de Lange, Yannick and Fletcher, George HL and De Bra, Paul and Hidders, Jan and Wu, Yuqing},
  title        = {Bisimulation reduction of big graphs on {MapReduce}},
  booktitle    = {British National Conference on Databases},
  year         = {2013},
  pages        = {189--203},
  organization = {Springer},
}

@InProceedings{rensink2000actionContraction,
  author = {Rensink, Arend},
  title = {Action Contraction},
  booktitle = {Proceedings of the 11th International Conference on Concurrency Theory},
  series = {CONCUR '00},
  year = {2000},
  isbn = {3-540-67897-2},
  pages = {290--304},
  numpages = {15},
  acmid = {701635},
  doi = {10.1007/3-540-44618-4\_22},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
}

@InCollection{pitts2011howesMehtod,
  author    = {Pitts, Andrew},
  title     = {Howe's method for higher-order languages},
  booktitle = {Advanced Topics in Bisimulation and Coinduction},
  publisher = {Cambridge University Press},
  year      = {2011},
  editor    = {Sangiorgi, Davide and Rutten, Jan},
  pages     = {197--232},
  doi       = {10.1017/CBO9780511792588.006},
  place     = {Cambridge},
}

@Article{gw1996branchingBisim,
  author    = {van Glabbeek, Rob J. and Weijland, W. Peter},
  title     = {Branching time and abstraction in bisimulation semantics},
  journal   = {Journal of the ACM (JACM)},
  year      = {1996},
  volume    = {43},
  number    = {3},
  pages     = {555--600},
  publisher = {ACM},
}

@InProceedings{dw2003csZrefinement,
  author       = {Derrick, John and Wehrheim, Heike},
  title        = {Using coupled simulations in non-atomic refinement},
  booktitle    = {International Conference of B and Z Users},
  year         = {2003},
  pages        = {127--147},
  address      = {Berlin, Heidelberg},
  organization = {Springer},
}

@Book{nnh2015popa,
  title     = {Principles of program analysis},
  publisher = {Springer},
  year      = {2015},
  author    = {Nielson, Flemming and Nielson, Hanne R. and Hankin, Chris},
}

@InProceedings{gpp2003bdd,
  author    = {Gentilini, Raffaella and Piazza, Carla and Policriti, Alberto},
  title     = {Computing strongly connected components in a linear number of symbolic steps.},
  booktitle = {SODA},
  year      = {2003},
  volume    = {3},
  pages     = {573--582},
}

@Misc{garavel2017vlts,
  author = {Garavel, Hubert},
  title  = {The {VLTS} Benchmark Suite},
  year   = {2017},
  note   = {Jointly created by CWI/SEN2 and INRIA/VASY as a CADP resource.},
  doi    = {10.18709/perscido.2017.11.ds100},
}

@Article{paigetarjan1987partitionrefinement,
  author        = {Paige, Robert and Tarjan, Robert E.},
  title         = {Three partition refinement algorithms},
  journal       = {SIAM Journal on Computing},
  year          = {1987},
  volume        = {16},
  number        = {6},
  pages         = {973--989},
  __markedentry = {[ben:]},
  publisher     = {SIAM},
}

@Article{bulychev2011gameSimulation,
  author        = {Bulychev, Peter E.},
  title         = {Game-theoretic simulation checking tool},
  journal       = {Programming and Computer Software},
  year          = {2011},
  volume        = {37},
  number        = {4},
  pages         = {200},
  __markedentry = {[ben:6]},
  publisher     = {Springer},
}

@Article{schulte2015deutsch,
  author    = {Schulte, Christiane},
  title     = {Der deutsch-deutsche {S}ch{\"a}ferhund -- {E}in {B}eitrag zur {G}ewaltgeschichte des {J}ahrhunderts der {E}xtreme},
  journal   = {Totalitarismus und Demokratie},
  year      = {2015},
  volume    = {12},
  number    = {2},
  pages     = {319--334},
  publisher = {Vandenhoeck \& Ruprecht GmbH \& Co. KG G{\"o}ttingen},
}

@InProceedings{kant2015ltsmin,
  author       = {Kant, Gijs and Laarman, Alfons and Meijer, Jeroen and van de Pol, Jaco and Blom, Stefan and van Dijk, Tom},
  title        = {{LTSmin}: {H}igh-performance language-independent model checking},
  booktitle    = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  year         = {2015},
  pages        = {692--707},
  organization = {Springer},
}

@InProceedings{grabr2014fdr,
  author    = {Gibson-Robinson, Thomas and Armstrong, Philip and Boulgakov, Alexandre and Roscoe, A.~W.},
  title     = {{FDR3}: {A} Modern Refinement Checker for {CSP}},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  year      = {2014},
  editor    = {{\'A}brah{\'a}m, Erika and Havelund, Klaus},
  pages     = {187--201},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {FDR3 is a complete rewrite of the CSP refinement checker FDR2, incorporating a significant number of enhancements. In this paper we describe the operation of FDR3 at a high level and then give a detailed description of several of its more important innovations. This includes the new multi-core refinement-checking algorithm that is able to achieve a near linear speed up as the number of cores increase. Further, we describe the new algorithm that FDR3 uses to construct its internal representation of CSP processes---this algorithm is more efficient than FDR2's, and is able to compile a large class of CSP processes to more efficient internal representations. We also present experimental results that compare FDR3 to related tools, which show it is unique (as far as we know) in being able to scale beyond the bounds of main memory.},
  isbn      = {978-3-642-54862-8},
}

@Article{garavel2013cadp,
  author    = {Garavel, Hubert and Lang, Fr{\'e}d{\'e}ric and Mateescu, Radu and Serwe, Wendelin},
  title     = {{CADP 2011}: {A} toolbox for the construction and analysis of distributed processes},
  journal   = {International Journal on Software Tools for Technology Transfer},
  year      = {2013},
  volume    = {15},
  number    = {2},
  pages     = {89--107},
  publisher = {Springer Berlin Heidelberg},
}

@MastersThesis{bisping2018coupledsim,
author = {Bisping, Benjamin},
title = {Computing Coupled Similarity},
school = {Tech\-ni\-sche Uni\-ver\-si\-t\"at Berlin},
year = {2018},
url = {https://coupledsim.bbisping.de/bisping_computingCoupledSimilarity_thesis.pdf}
}


@InProceedings{bn2019coupledsimTacas,
  author    = {Bisping, Benjamin and Nestmann, Uwe},
  title     = {Computing coupled similarity},
  booktitle = {Proceedings of {TACAS}},
  series    = {LNCS},
  publisher = {Springer},
  doi       = {10.1007/978-3-030-17462-0\_14},
  pages     = {244--261},
  year      = 2019,
}

@incollection{bm2021contrasimilarity,
  author= {Bisping, Benjamin and Montanari, Luisa},
  year= {2021},
  title= {A Game Characterization for Contrasimilarity},
  editor= {Dardha, Ornela and Castiglioni, Valentina},
  booktitle= {{Proceedings Combined 28th International Workshop on} Expressiveness in Concurrency {and 18th Workshop on} Structural Operational Semantics},
  series= {Electronic Proceedings in Theoretical Computer Science},
  volume= {339},
  publisher= {Open Publishing Association},
  pages= {27--42},
  doi= {10.4204/EPTCS.339.5}
}

@article{Encodability_Process_Calculi-AFP,
  author  = {Kirstin Peters and Rob J. van Glabbeek},
  title   = {Analysing and Comparing Encodability Criteria for Process Calculi},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Encodability_Process_Calculi.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{bnp2020coupledsim32,
  author    = {Benjamin Bisping and
               Uwe Nestmann and
               Kirstin Peters},
  title     = {Coupled similarity: the first 32 years},
  journal   = {Acta Informatica},
  volume    = {57},
  number    = {3--5},
  pages     = {439--463},
  year      = {2020},
  doi       = {10.1007/s00236-019-00356-4},
}

@misc{bj2023ltbtsSilentSteps,
  title={Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps}, 
  author={Benjamin Bisping and David N. Jansen},
  year={2023},
  eprint={2305.17671},
  archivePrefix={arXiv},
  primaryClass={cs.LO},
  doi={s10.48550/arXiv.2305.17671}
}


@MastersThesis{pohlmann2021reactivebisim,
author = {Pohlmann, Maximilian},
title = {Reducing Reactive to Strong Bisimilarity},
school = {Tech\-ni\-sche Uni\-ver\-si\-t\"at Berlin},
year = {2021},
type={Bachelor's Thesis},
url = {https://maxpohlmann.github.io/Reducing-Reactive-to-Strong-Bisimilarity/}
}

@Comment{jabref-meta: databaseType:bibtex;}
