# Bachelor/Master Topics: Semantics of distributed systems. (Benjamin Bisping)
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@tu-berlin.de! (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.
:::danger
As of 2022-03-24, my capacities for mentoring final theses are totally booked out for the foreseeable future!^[The only kind of exception I could make would be for people who are proficient in our field to a degree where they don't need much support. A typical indicator of this would be having finished Reactive Systems, Isabelle Lab, Lambda-Calculus-and-Type-Systems, or Logic-Games-Automata with outstanding grades (1.0 or 1.3).]
:::
## Notions of equivalence
### 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)].
- **The 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.
### Proving Correctness of Spectroscopy Algorithm in Isabelle/HOL
Practical skills: Isabelle/HOL (or Lean)
Theory background: Linear-time–branching-time spectrum, basic game theory
- **Background:** [Bisping & Nestmann 2021](https://arxiv.org/abs/2109.15295) introduce an algorithm to find the finest notion of equivalence equating/ordering two processes. But the proof is incomplete (and parts of the algorithm will need to be corrected in an upcomming publication).
- **Task:** Create a machine-checkable version of the correctnes proof in Isabelle/HOL (or Lean).
- For Bachelor level: It's okay if the proof does not span the whole algorithm, and only considers finitary subsets of Hennessy-Milner logic.
- For Master level: The proof should be complete and ideally also cover the question in which situations partially constructed formulas can be pruned. Also, it would be nice to unify the Isabelle theory with theories from prior student projects.
### Recharting the Weak Linear-time–Branching-time Spectrum
Practical skills: Isabelle/HOL (or Lean, or really strong pen-and-paper proof skills)
Theory background: Linear-time–branching-time spectrum, Hennessy-Milner logic
- **Background:** [Bisping & Nestmann 2021](https://arxiv.org/abs/2109.15295) characterize the linear-time–branching-time spectrum without internal moves by counting the expressive features used in Hennessy-Milner formulas. This cannot easily be extended to HML with internal behavior.
- **Task:** Define a special version of HML and the spectrum such that their relationship can be nicely characterized in a similar way to the one in the existing publication.
- For Bachelor level: It would already suffice to proof the correctness of the claims regarding the metric from [Bisping & Nestmann 2021](https://arxiv.org/abs/2109.15295) (and provide corrections).
- For Master level: There should be a complete proof that the sub-logics and the expressiveness metric correspond.
### Minimization and Characteristic Formulas for all Equivalences
Practical skills: Scala.js programming, graph algorithms
Theory background: Linear-time–branching-time spectrum, Hennessy-Milner logic
- **Background:** A (locally) characteristic formula for a state in a transition system tells the state apart from every other non-equivalent state in the transition system. The algorithm from [Bisping & Nestmann 2021](https://arxiv.org/abs/2109.15295) explores the equivalence structure of a system.
- **Task:** Extend the prototype tool of [Bisping & Nestmann 2021](https://arxiv.org/abs/2109.15295) such that it uses the algorithm output to support the minimization of transition systems with respect to any equivalence and to supply locally characteristic formulas for their states.
- For Master level: Also explore the formal properties of the characterization languages. What happens in case of infinite transition systems?
## Counterfactual 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 “Countercatuals” 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)
:::spoiler Implementing a Computer Game on Counterfactuals (taken)
### Implementing a Computer Game on Counterfactuals
Practical skills: Browser game programming (e.g. Phaser/TypeScript), game design
Theory background: Modal logics / counterfactuals
- **Background:** Proving [counterfactuals](https://plato.stanford.edu/entries/david-lewis/#3) can be used to tell possible worlds apart, much as Hennessy-Milner modal logic can be used to distinguish states in transition systems. A previous student project has implemented a [game about this mechanism in Hennessy-Milner logic](https://concurrency-theory.org/ltbt-game/).
- **Task:** Implement a similar game about distinguishing formulas in David Lewis's Counterfactual logic.
- For Master level: Provide proper proofs that your computer game corresponds to a theoretical game that matches the Counterfactual semantics.
:::
:::spoiler Checking Reactive Bisimilarity in mCRL2 (taken)
### Checking Reactive Bisimilarity
Practical skills: C++ or Scala programming, graph algorithms
Theory background: (Reactive) Bisimulation semantics
- **Background:** Up to now, there is no tool capable of checking processes for [equivalence with respect to van Glabbeeks' reactive bisimulation semantics from 2020](https://arxiv.org/abs/2008.11499). A previous [Bachelor project](https://github.com/maxpohlmann/Reducing-Reactive-to-Strong-Bisimilarity) has formalized a reduction to conventional strong bisimulation, which opens an easy path for implementing a reactive bisimulation checker.
- **Task:** Develop and implement an algorithm to check for reactive bisimilarity on processes. (You should build on existing tools, albeit a part of the problem will be to provide meaningful example transition systems for the semantics at all in the first place.)
- For Master level: Provide proofs (or at least really comprehensive tests) that your algorithm/implementation does what it's supposed to do. Also, try to make the checking actually feasible. (The existing reduction will create gigantic transition systems.)
:::
:::spoiler Implementing a Computer Game about Reactive Bisimilarity (taken)
### Implementing a Computer Game about Reactive Bisimilarity
Practical skills: Browser game programming (e.g. Phaser/TypeScript), game design
Theory background: (Reactive) Bisimulation semantics
- **Background:** Some Bachelor's theses implemented computer games about process equivalences, such as <https://www.concurrency-theory.org/rvg-game/>. There is no such game for [van Glabbeeks' reactive bisimulation semantics](https://arxiv.org/abs/2008.11499).
- **Task:** Implement a computer game about reactive bisimulation, which can be run in the browser.
- For Master level: Provide proper proofs that your computer game corresponds to a theoretical game that matches reactive bisimulation semantics.
:::
## Semantics and Encodings
### Encoding Lambda Terms as HASH.ai-Agents
Practical skills: JavaScript, HASH.ai agent simulations, Compiler construction
Theory background: Lamba calculus / cube, Agents
- **Background:** [HASH.ai](https://hash.ai/) is a platform for implementing simulations based around agents, which communicate in synchronous message rounds. The Lambda calculus is one of the simplest foundations of computing.
- **Task:** Implement a way to translate Lambda calculus terms into a dynamic network of communicating HASH.ai agents that can simulate the concurrent (!) execution of the term.
- For Master level: Option A) Support untyped and typed Lambda, possibly extending to the whole Lambda cube / Calculus of Constructions. Option B) Provide a proper encoding from the Lambda calculus into a calculus of agents / communicating automata that matches your model, and prove the correctness of the encoding.
### 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.