Oberseminar WS2025/26

It 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.

The 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.

Codensity 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.

Machine 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.

We 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.

Topological 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.

Perception 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.

Labelled 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).

The 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.

Some 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.

Fuzzy coalgebraic logic combines fuzzy semantics with coalgebraic models for state-based systems, enabling reasoning about graded or uncertain behavior. The computational complexity of such logics strongly depends on the chosen fuzzy base and modal operators, ranging from highly expressive but costly Łukasiewicz-style logics to simpler Zadeh-based variants. To balance expressiveness and tractability, we study non-expansive fuzzy coalgebraic logics, where modal operators are non-expansive with respect to an underlying metric. Non-expansivity is known to yield favorable complexity properties, and previously, we introduced conditions under which satisfiability of formulas remains in PSPACE. Starting from this point, we investigate preliminary conditions under which reasoning with general TBoxes remains in EXPTIME. This work is ongoing and aims to clarify which semantic and structural restrictions allow expressive ontology-based reasoning without incurring prohibitive complexity.

Regular Alternating Nominal Automata (RANA) were introduced by Frank et al. as acceptance models for formal languages of finite words over infinite alphabets. RANA’s are equivalent to linear-time nominal temporal logic Bar-μTL, introduced by Hausmann et al., and their corresponding inclusion and non-emptiness problems are of elementary complexity.

In this talk, we present our ongoing research aimed at developing Nominal Alternating Parity Automata (NAPA’s), which accept formal languages of infinite words over infinite alphabets. Thus, NAPA’s can be considered an extension of RANAs for infinite words. We present a construction from Büchi regular nondeterministic nominal automata (Urbat et al.) to NAPA’s and discuss current challenges in development, such as the name-dropping modification of NAPA’s.

Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. In this talk we present the main results from the paper „Bisimilarity in Fresh-Register Automata“ by Murawski, Ramsay and Tzevelekos. We investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. For other classes we are going to see membership in PSPACE and also NP.