If you have any questions, please get in touch with the named contact persons (also without obligation). Other topics can be arranged in personal consultation with the department's teaching staff.

Bachelor's and Master's theses are assigned and supervised individually by arrangement. Timely information and expression of interest are advantageous. Please contact Prof Olderog (during office hours) or his staff.

• Optimisation Techniques for Reachability Analysis of Bounded Petri Nets
• Safe overtaking on motorways despite imperfect knowledge
• Undecidability of the Duration Calculus in Continuous Time
• Forgetful Petri Games - Synthesising Distributed Systems with Partially Observable Casual Memory
• Implementation of a tool for the transformation of MLSLS into SMTLib
• Graphical editor for traffic situations
• Safe overtaking in oncoming traffic despite imperfect knowledge
  Conversion from MLSL to QdL formulas
• Existence graphs: tool-supported application of inference rules
• Graphical editor for constraint diagrams and translation to PLC automata
• Regular model checking for parameterised phase-event automata by means of widening
• Implementation of a diagram editor for shape diagrams in Eclipse
• Extension of the transformation of duration calculus into phase event automata with integrators

• Finite-Memory Strategies for Petri Games
• A Multi-Lane Distance Controller for a Spatial Logic
• Transformational Semantics of the Combination π-OZ for Mobile Processes with Data
• Decidability of Petri Games with 2 Environment and 2 System Players
• Moving Hazards - Communicating about Human Drivers in Autonomous Traffic
• Development of a verification environment for a dynamically typed programming language
• Petri games: Extension of safety winning conditions to markers
• Development of an editor for the creation of PLC automata in Eclipse with support of the theorem prover Z3
• Refinement of PI-calculus processes
• Semantics of controllers for safe vehicle manoeuvres