# Bachelor/Master Topics: Semantics of distributed systems. ([Benjamin Bisping](https://bbisping.de/)) If you are interested in doing a Bachelor's or Master's thesis on one of the topics (or a similar one), reach out to benjamin.bisping@telecom-sudparis.eu! (Please include information on your skill/experience background!) The precise topic usually is elaborated in a few rounds of communication, also taking into account your skill set, the direction in which you want to grow, and whether it is a Bachelor or Master topic. You can write in German or English. Many of the theses I previously advised can be found via https://bbisping.de/. ::: info As of 2025-11, I'm a member of Télécom SudParis / Institut Polytechnique de Paris. To some degree, it might still be possible to pursue topics mentioned here (if you get [Uwe Nestmann](https://www.tu.berlin/mtv/team/leitung/prof-dr-ing-uwe-nestmann) to supervise at TU Berlin) or through a “Master internship” in the French system (if you have some way of making use of this). ::: ## Games and Security ### Putting price tags on attacks in security protocols ::: success [This project can be pursued as a **paid internship for Master students** at Télécom SudParis / Institud de Polytechnique de Paris](https://institutminestelecom.recruitee.com/l/en/o/stagiaire-rs2m-securite-6-mois). ::: *Practical skills:* Functional programming, ProVerif, SAT solving *Theoretical knowledge:* Horn clauses, Energy games - **Background:** [ProVerif](https://bblanche.gitlabpages.inria.fr/proverif//publications/BlanchetFnTPS16.pdf) is an important tool to model the security of cryptographic protocols. However, it usually only allows yes/no-questions through reachability games, not taking into account quantitative questions about costs and capabilities an attacker might need. This can be changed by enriching the game model with attacker resources, in so-called [“energy games”](https://doi.org/10.4230/LIPIcs.CONCUR.2025.29). - **Task:** Adapt ProVerif such that attacks can have prices. For this, you modify its Horn clause backend to use energy games. These can either be solved by specialized game algorithms or through SAT solvers that support linear integer arithmetic. ### Presenting game-theoretical energy games as computer games *Practical skills:* Object-oriented programming, Game engines, UX *Theoretical knowledge:* Graph algorithms, Energy games - **Background:** [Multi-dimensional energy games](https://doi.org/10.4230/LIPIcs.CONCUR.2025.29) are a versatile model to describe strategic situations for instance in practical applications such as cyber security, but also in theoretical contexts such as program semantics. Also, they allow for intuitive presentations of problems from these domains—which are great for teaching and science communications. - **Task:** Develop a small computer game e.g. about cyber security or graph problems, which uses Galois energy games under the hood to model game mechanics. - *Examples:* Previous games about [weak process equivalences](https://www.concurrency-theory.org/rvg-game/) and [reactive bisimilarity](https://eloinoel.github.io/ReactiveBisimilarityGame/). ## Notions of equivalence ### The Weak Quantitative Linear-Time–Branching-Time Spectrum (Master) Practical skills: Proving / formalization Theory background: Game-theory, Quantitative behavioral equivalences - **Background:** There exists a quantitative version of the linear-time–branching-time spectrum of behavioral equivalences due to [[Fahrenberg et al. 2014](https://inria.hal.science/hal-01087368/document)] based on game characterizations. So far, it does not account for weak equivalences, which abstract internal behavior. For the non-quantitative version of the weak spectrum, I have come up with an [energy-game characterization](https://doi.org/10.4204/EPTCS.412.6), including an Isabelle/HOL formalization. - **Task:** Combine Fahrenberg's and Bisping's game characterizations to handle quantitative *weak* behavioral equivalences. Ideally, the work is accompanied by formalization in a proof assistant such as Isabelle/HOL. - Bachelor project version: It suffices to come up with a single energy game for a spectrum of (strong) quantitative behavioral equivalences. ### Checking Contrasimilarity in mCRL2 Practical skills: C++ programming, graph algorithms Theory background: Basic game theory - **Background:** Contrasimilarity is the weakest bisimulation-like notion of equivalence for systems with internal transitions. Up to now, no tool supports checking contrasimilarity. But this is in reach with a recent publication [[Bisping & Montanari 2021](https://doi.org/10.4204/EPTCS.339.5)]. - **Task:** Add the algorithm to the tool suite of [mCRL2](https://www.mcrl2.org/). Ideally, the thesis also extends and improves upon work from a prior bachelor's thesis, which has [added coupled similarity checking](https://github.com/mCRL2org/mCRL2/pull/1619). - For Master level: Also implement heavy optimizations and prove relevant parts of the implementation correctness. ### Equivalence Checking within a Computer Algebra System Practical skills: Programming (Scala/Python/JS/?), CAS familiarity (Sage, Matlab, Mathematica?) Theory background: Behavioral equivalences, linear-time–branching-time spectrum - **Background:** Computer algebra systems are mostly known for functional analysis and related math problems, but some also support directed graphs, where behavioral equivalences like bisimilarity, similarity, and trace equivalence might be interesting. - **Task:** Provide a nice way to specify processes and check them for various equivalences in a CAS, including meaningful visualization for witness relations and counterexamples of equivalences. - **For master level:** Also provide good ways to input and transform CCS/Pi processes. ## Counterfactuals and Modal Logics ### Modelling Counterfactual Conditionals in Isabelle/HOL Practical skills: Isabelle/HOL proving Theory background: Modal logics - **Background:** The [David Lewis' modal logic of counterfactual conditionals](https://plato.stanford.edu/entries/david-lewis/#3) has been hugely influential for analytical philosophy, in particular in the context of explaining causality. We have a [half-finished formalization of the 1973 monograph “Counterfactuals” in Isabelle/HOL](https://github.com/benkeks/counterfactuals-isabelle). - **Task:** Finish the formalization and maybe formalize / prove other interesting aspects from the literature on Counterfactuals and dispositions. - For Master level: Try to relate the counterfactual logic to a formalism from computer science. (E.g. Hennessy-Milner modal logics with timeouts, hyperproperties, stuttering-invariant temporal logics) ### Modal Logics from Expressiveness Coordinates Practical skills: Programming, web Theory background: Modal logics, equivalence notions - **Background:** In [my current work](https://arxiv.org/abs/2303.08904#), I usually characterize notions of equivalence through coordinates in a multi-dimensional space of “distinguishing capabilities.” These correspond to sublanguages of Hennessy–Milner modal logic. - **Task:** Write an algorithm to automatically generate grammars and interesting example formulas from the coordinates! ## Semantics and Encodings ### Relating Computer Games and Models of Computation Practical skills: Formal modelling and proving Theory background: Automata and rewriting models - **Background:** Since 2018, students have implemented [dozens of games inspired by formalisms of computation within my practical programming course “Modelle Dynamischer Systeme.”](https://pr.mtv.tu-berlin.de/) Some of the games align more closely with their formalisms than others... - **Task:** Pick some of the [games](https://pr.mtv.tu-berlin.de/) and rigorously relate and compare their mechanics to the formalism they ought to be based on! ### Higher-order Dynamic-causality Event Structures in Isabelle/HOL Practical skills: Isabelle/HOL proving (or Lean) Theory background: Event structures (or workflow languages, e.g. Petri nets) - **Background:** A [dissertation at MTV](http://dx.doi.org/10.14279/depositonce-6989) has explored a dynamic kind of event structures as a formalism that can be used as a workflow language. The dissertation contains some proofs where it would be nice to have a fully formal development of the proofs in an interactive proof assistant. - **Task:** Formalize relevant parts of the dissertation in Isabelle/HOL. - For Bachelor level: It's okay to focus only on a smaller part.