Oberseminar WS2025/26
Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in Raum 00.131-128 (Cauerstraße 11) statt.
Das Oberseminar steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen.
Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Die Vortragstermine werden am ersten Termin in der Vorlesungszeit festgelegt.
Bei Nachfragen gerne per Mail an den Seminarleiter (Prof. Dr. Lutz Schröder), Anmeldung zur Mailingliste: TCS-Seminar Mailinglist
Vorträge
| Current Talks | |
| Tuesday, 09.12.2025 |
Generalized Kantorovich-Rubinstein Duality beyond Hausdorff and Kantorovich
AbstractThe classical Kantorovich-Rubinstein duality guarantees coincidence between metrics on the space of probability distributions defined on the one hand via transport plans (couplings) and on the other hand via price functions. Both constructions have been lifted to the level of generality of set functors, with the coupling-based construction referred to as the Wasserstein lifting, and the price-function-based construction as the Kantorovich lifting, both based on a choice of quantitative modalities for the given functor. It is known that every Wasserstein lifting can be expressed as a Kantorovich lifting; however, the latter in general needs to use additional modalities. We give an example showing that this cannot be avoided in general. We refer to cases in which the same modalities can be used as satisfying the generalized Kantorovich-Rubinstein duality. We establish the generalized Kantorovich-Rubinstein duality in this sense for two important cases: The Lévy-Prokhorov distance on distributions, which finds wide-spread applications in machine learning due to its favourable stability properties, and the standard metric on convex sets of distributions that arises by combining the Hausdorff and Wasserstein distances.
|
| Tuesday, 09.12.2025 |
Coalgebraic Methods for Continuous-Time Probabilistic Systems
AbstractSome classes of systems seem to be out of reach of the vanilla theory of universal coalgebra. In this talk, we look at continuous-time stochastic processes, like Brownian motion or continuous-time Markov chains, and cast them as instances of the novel concept of graded coalgebra, which consists of one carrier and a monoid-indexed class of morphisms, compatible with the structure of a graded monad. We define both branching-time and trace semantics for these coalgebras and link them to recent work by Chen et al. on Feller-Dynkin processes. We start developing the theory surrounding graded coalgebras, including results about the existence of a terminal coalgebra and characteristic logics for both types of process semantics.
|
| Upcoming Talks | |
| Tuesday, 16.12.2025 |
TBA
AbstractTBA
|
| Tuesday, 13.01.2025 |
TBA
AbstractTBA
|
| Tuesday, 20.01.2025 |
TBA
AbstractTBA
|
| Tuesday, 27.01.2025 |
TBA
AbstractTBA
|
| Tuesday, 03.02.2025 |
TBA
AbstractTBA
|
| Tuesday, 03.02.2025 |
TBA
AbstractTBA
|
| Previous Talks | |
| Tuesday, 21.10.2025 |
Basic Varieties of Quantitative Algebras
AbstractIt is well known that all c-basic varieties, studied by Mardare, Panangaden and Plotkin, are monadic categories over Met, the category of extended metric spaces. This opens the question of which monads correspond to those varieties. For c=ω, all enriched finitary monads have that property. But Urbat presented an example of an ω-basic variety yielding a non-finitary monad. We prove that a monad corresponds to an ω-basic variety iff it is a weighted colimit of finitary monads (in the category Mnd(Met) of enriched monads). Further, a monad corresponds to a c-basic variety for an uncountable cardinal c iff it is enriched and c-accessible. |
| Tuesday, 28.10.2025 |
DIREGA: Formalizing German Register Law
Slides
AbstractThe DIREGA project aims to create a formal, computable model of German commercial register law. This talk will delve into the methodological and technical hurdles faced during this formalization process. We will present key challenges for computational representation of the relevant regulations. Furthermore, we will critically analyze the different formalization techniques and modeling languages tested and the fundamental problems that necessitated shifts in our approach.
|
| Tuesday, 04.11.2025 |
Demystifying Codensity Monads via Duality
Slides
AbstractCodensity monads provide a universal method to generate complex monads from simple functors. Recently, a wide range of important monads in logic, denotational semantics, and probabilistic computation, such as several incarnations of the ultrafilter monad, the Vietoris monad, and the Giry monad, have been presented as codensity monads, using complex arguments. We propose a unifying categorical approach to codensity presentations of monads, based on the idea of relating the presenting functor to a dense functor via a suitable duality between categories. We prove a general presentation result applying to every such situation and demonstrate that most codensity presentations known in the literature emerge from this strikingly simple duality-based setup, drastically alleviating the complexity of their proofs and in many cases completely reducing them to standard duality results. Additionally, we derive a number of novel codensity presentations using our framework, including the first non-trivial codensity presentations for the filter monads on sets and topological spaces, the lower Vietoris monad on topological spaces, and the expectation monad on sets.
|
| Tuesday, 11.11.2025 |
Machine Learning in Theoretical Computer Science
Slides
AbstractMachine Learning, in particular the development of Large Language Models (LLMs) in the last half decade, has sculpted the landscape of computer science more than any other broader field of research in a mutual manner. Although our work might not immediately be automated, we already observe the effects of broadly available and fairly precise natural language reasoning in the exercises to our foundational lectures. In this talk, we give an overview on recent developments in automated processing of language, and suggest various options how to incorporate machine learning either as a subject to research or as a tool for auxiliary tasks in our work.
|
| Tuesday, 18.11.2025 |
Implementation of a Tableau Reasoner for Non-Expansive Fuzzy ALC
Slides
AbstractWe give an implementation of an on-the-fly tableau-based decision procedure for satisfiability checking in the description logic non-expansive fuzzy ALC. Besides a sequence of concept assertions, we accept a set of global assumptions – a general TBox – as input. The main part of the thesis, the program, is realized in the programming language OCaml. The EXPTIME algorithm is extended with some optimization techniques that can cut off the search space significantly. After discussing the details of the implementation, we present a benchmark series to point out some strengths of the optimizations and worst-case computation times.
|
| Tuesday, 18.11.2025 |
Coalgebraic Topological Sort
Slides
AbstractTopological sorting is a fundamental concept of graph theory and has widespread applications, ranging from task scheduling to dependency resolution in program compilation. Moreover, algorithms for topological sorting, such as Kahn’s algorithm, build the basis for solving other problems in graph theory. In this talk, we present a coalgebraic generalisation of Kahn’s algorithm and show that topological sorting of general F-coalgebras can be expressed as an adjoint functor.
|
| Tuesday, 25.11.2025 |
Runtime Monitoring of Object Detection Networks Using Register Automata
AbstractPerception systems in autonomous vehicles must correctly detect and track objects in complex, dynamic environments. Classical temporal logics are limited in expressing spatial or attribute-based relations in multi-object data streams, which motivated the development of Spatio-Temporal Perception Logic (STPL). Monitoring full STPL, however, is challenging due to constructs that require unbounded reasoning over symbolic object bindings. This thesis introduces a restricted fragment of STPL tailored to finite-memory runtime monitoring and develops alternating modified register automata (A-MRA) as a suitable computational model. The work establishes a translation from restricted STPL to A-MRA that preserves satisfaction semantics and enables sound, non-predictive monitoring over finite execution prefixes. The resulting approach integrates naturally with perception pipelines and provides three-valued verdicts indicating satisfaction, violation, or inconclusive outcomes.
|
| Tuesday, 25.11.2025 |
Explainability of Probabilistic Bisimilarity Distances for Labelled Markov Chains
Slides
AbstractLabelled Markov Chains are automata, where states have labels or „actions“ and transtitions have probabilities. These probabilities are determined by a probability distibution dependent only on the current state. As with classic automata, two states can be bisimilar, if both states can fully simulate the other. Due to the instability of probabilistic bisimilarity, probabilistic bisimilarity distances between 0 and 1 are used instead. To explain these distances the paper introduces formulas, that represent a set of label sequences and gives an interpretation, which can be understood as follows: Given a state s, the interpretation gets us the the probability that starting with s, one of those sequences defined in the formula will play out. As can be showm, the bisimilarity distances between states s and t can be explained by a series of such formulas. Rady and Breugel offer us a more concise way to construct those formulas, computable in polynomial time, by relying on auxiliary functions, that represent the dual interpretation of the Linear Programming transportation problem, on which the probabilistic bisimilarity distances rely. In my talk I will be going over the full process starting with defining probabilistic bisimilarity distances up to the proposed algorithm on how to compute these formulas. We will also touch on the necessary mathematical concepts used in the paper (Kleene fixpoint theorem, transportation problem, Kantorovich-Rubinstein duality). |