# 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-01, I'm mostly booked out for the foreseeable future.^[Exceptions might be possible for students who can work mostly on their own. This would be indicated by having finished Reactive-Systems, Isabelle-Lab, Lambda-Calculus-and-Type-Systems, Algebraic-Process-Calculi, Theory-of-Distributed-Algorithms or Logic-Games-Automata with outstanding grades.] ::: ## 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. ::: ### 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 prove 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. ### 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! ### 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.