Vorträge im SoSe 2020

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in vorerst per Videokonferenz statt (Ein Zoom-Link findet sich im StudOn-Kurs). Es steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen. Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Nachfragen gerne per Mail an den Leiter des Lehrstuhls (

Voraussichtlicher Plan SoSe 2020

Bisherige Vorträge

Date Speaker, Topic Abstract
04-August Daniel Hausmann, Harnessing LTL With Freeze Quantification hausmann-mubar
Logics and automata models for languages over infinite alphabets serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, where names play the role of data. E.g. regular nondeterministic nominal automata (RNNA) are equivalent to a subclass of the standard register automata model, characterized by a lossiness condition referred to as name dropping. This subclass generally enjoys better computational properties than the full class of register automata, for which, e.g., inclusion checking is undecidable. We introduce a variant of Freeze LTL for finite words over an infinite alphabet, modelled as the set of names in a nominal setting, and show that the model checking problem over RNNA is elementary, in fact in parametrized ExpSpace, effectively with the number of registers as the parameter. Since RNNA can accept the universal language, this entails the same complexity bound for satisfiability checking.
21-July Paula Welzenbach, An Implementation of a Solver for Systems of Fixpoint Equations welzenberg-talk
In my Master’s thesis I implemented different versions of an approach that calculates the solution for systems of fixpoint equations. This approach generalizes parity game algorithms and combines them with universal graphs to tackle fixpoint equation systems with arbitrary monotone functions over finite powerset lattices. The talk will present the approach and set a focus on its implementation.
16-June Sergey Goncharov, Towards Constructive Hybrid Semantics sergey-talk-16-06-20
With hybrid systems becoming ever more pervasive, the underlying semantic challenges emerge in their entirety. The need for principled semantic foundations has been recognized previously in the case of discrete computation and discrete data, with subsequent implementations in programming languages and proof assistants. Hybrid systems, contrastingly, do not directly fit into the classical semantic paradigms due to the presence of quite specific “non-programmable” features, such as Zeno behaviour and the inherent indispensable reliance on a notion of continuous time. We analyze the phenomenon of hybrid semantics from a constructive viewpoint. In doing so, we propose a monad-based semantics, generic over a given ordered monoid representing the time domain, hence abstracting from the monoid of constructive reals. We implement our construction as a higher inductive-inductive type in the recent cubical extension of the Agda proof assistant, significantly using state-of-the-art advances of homotopy type theory. We show that classically, i.e. under the axiom of choice, our construction admits a charaterization in terms of directed sequence completion. [The talk is based on the recent joint work with Tim Lukas Diezel]
09-June Hans-Peter Deifel, The M in CoPaR – From Partition Refinement to Minimization slides-deifel-ss20
The Coalgebraic Partition Refiner (CoPaR) implements a partition refinement algorithm on coalgebraic generality. That is, it computes the coarsest partition on the state space of a coalgebra such that the resulting quotient map is a coalgebra homomorphism. That’s nice, but hasn’t exactly lead to market domination. In this talk I present ongoing work to add actual minimization to CoPaR. This requires to solve two separate tasks: Computing the (encoding of the) quotient coalgebra from a partition on the state space and removing unreachable states.
19-May Paul Wild, Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions wild
We revisit the topic of fuzzy lax extensions from a previous talk and show how the result characterizing all fuzzy lax extensions as instances of the Kantorovich lifting can be extended with a Hennessy-Milner theorem for such extensions by making use of a new nonexpansivity criterion. More precisely, we show that from any fuzzy lax extension we can extract a set of (fuzzy) predicate liftings such that the logical distance in the arising coalgebraic logic coincides with the behavioural distance induced by the lax extension. We also show that although the proof is based on finitary methods, the result also applies to certain not-quite-finitary functors such as the discrete distribution functor.
12-May Tadeusz Litak, Describable Nuclei, Negative Translations and Extension Stability What do soundness/completeness of negative translations of intutionistic modal logics, extension stability of preservativity/provability logics and the use of nuclei on Heyting Algebra Expansions (HAEs) to form other HAEs have in common? As it turns out, in all those cases one appears to deal with a certain kind of the subframe property for a given logic, i.e., the question whether the logic in question survives a transition to at least some types of substructures of its Kripke-style or neighourhood-style frames. The nucleic perspective on subframe logics has been introduced by Silvio Ghilardi and Guram Bezhanishvili (APAL 2007) for the purely superintuitionistic syntax (without modalities or other additional connectives). It has not been used so much in the modal setting, mostly because the focus in the field tends to be on modal logics with classical propositional base, and nuclei are a rather trivial notion in the boolean setting. However, things are very different intuitionistically. Since the 1970’s, nuclei have been studied in the context of point-free topologies (lattice-complete Heyting algebras), sheaves and Grothendieck topologies on toposes, and finally arbitrary Heyting algebras (Macnab 1981). Other communities may know them as lax modalities or (a somewhat degenerate case of) strong monads. We marry the nucleic view on subframe properties with the framework of describable operations introduced to study subframe logics in Frank Wolter’s PhD Thesis (1993). Wolter’s original setting was restricted to classical modal logics, but with minimal care his setup can be made to work intuitionistically and nuclei provide the missing ingredient to make it fruitful. From this perspective, we revisit the FSCD 2017 study (joint work with Miriam Polzer and Ulrich Rabenstein) of soundness and completeness of negative translations in modal logic and our present study of extension stability for preservativity logics based on constructive strict implication (jointly with Albert Visser). Various characterization and completeness results can be obtained in a generic way.
5-May Henning Urbat, Nominal Topology for Data Languages urbat
Regular languages can be understood from a topological point of view using profinite spaces (a.k.a. Stone spaces). In this talk, we discuss an extension of the profinite approach to the theory of data languages, i.e. languages over infinite alphabets: we introduce pro-orbit-finite topological spaces over nominal sets and show that regular data languages correspond uniquely to continuous predicates of the space of pro-orbit-finite words.
28-Apr Lutz Schröder, NP Reasoning in the Monotone mu-Calculus monotonemu20200428
Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic — the alternation-free monotone mu-calculus with the universal modality — contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes.