# 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@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. Many of the theses I previously advised can be found via https://bbisping.de/. :::warning As of 2024-09, I can't mentor new thesis projects. ::: ## Notions of equivalence :::spoiler Checking Contrasimilarity in mCRL2 (taken) ### 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. ::: :::spoiler Equivalence Checking using WebGPU and Energy Games (taken) ::: :::spoiler Proving Correctness of Spectroscopy Algorithm in Isabelle/HOL (blocked) ### 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, Jansen & Nestmann 2022](https://doi.org/10.46298/lmcs-18(3:19)2022) introduce an algorithm to find the finest notion of equivalence equating/ordering two processes, and prove its correctness. - **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. ::: ### 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. :::spoiler Linear-time–Branching-time Spectroscopy in CAAL (taken) ### Linear-time–Branching-time Spectroscopy in CAAL https://caal.cs.aau.dk/ ::: ## Counterfactuals and Modal Logics :::spoiler Modelling Counterfactual Conditionals in Isabelle/HOL (taken) ### 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) ::: :::spoiler Model-checking Process Equivalences through Polyadic Modal Logics (taken) ### Model-checking Process Equivalences through Polyadic Modal Logics Practical skills: Scala programming Theory background: Modal logics - **Background:** The [higher-order polyadic μ-calculus](https://www.sciencedirect.com/science/article/pii/S0304397514006574)^[Quite a mouthful!] can be used to describe behavioral equivalences by modal formulas. Ben is currently developing a tool to work with a lot of equivalences in one unified setting. - **Task:** Implement a checker for the modal formulas usable within Ben's tool and employ it to check various equivalences! - For Master level: Extend the approach to weak equivalences, and/or implement a massively parallelized and reasonably efficient checker. ::: ### 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.