January 2021
Wednesday, January 20

LICS 2021 Abstract Submission Deadline
Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:1515:45 in vorerst per Videokonferenz statt (Ein ZoomLink findet sich im StudOnKurs). 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 (mailto:lutz.schroeder@informatik.unierlangen.de).
Date  Speaker, Topic  Abstract 
10August  Pedro Nora, Hausdorff coalgebras noratalk 
As composites of constant, finite (co)product, identity, and powerset functors, Kripke polynomial functors form a relevant class of SETfunctors in the theory of coalgebras. In this talk we expand the theory of limits in categories of coalgebras of Kripke polynomial functors to the context of quantaleenriched categories. To assume the role of the powerset functor we consider “powersetlike” functors based on a quantaleenriched version of the Hausdorff metric. As a starting point, we show that for a lifting of a SETfunctor to a topological category X over SET that commutes with the forgetful functor, the corresponding category of coalgebras over X is topological over the category of coalgebras over SET and, therefore, it is “as complete” but cannot be “more complete”. Secondly, based on a Cantorlike argument, we observe that Hausdorff functors on categories of quantaleenriched categories do not admit a terminal coalgebra. Finally, in order to overcome these “negative” results, we combine quantaleenriched categories and topology. 
04August  Daniel Hausmann, Harnessing LTL With Freeze Quantification hausmannmubar 
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. 
21July  Paula Welzenbach, An Implementation of a Solver for Systems of Fixpoint Equations welzenbergtalk 
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. 
23June  Thorsten Wißmann, Reachability vs Bisimilarity Minimization wissmannreachvsbisim 
For the minimization state based systems (i.e. the reduction of the number of states while retaining the system’s semantics), there are two obvious aspects: removing unnecessary states of the system and merging redundant states in the system. In the present talk, we compare the two aspects using the terminology of coalgebras and show that they are dual concepts by defining an abstract notion of minimality and minimization in a category. We will find criteria on the category that ensure uniqueness, existence, and functoriality of the minimization aspects, where the proofs instantiate to those for reachability and bisimilarity minimization in the standard coalgebra literature. Finally, we will see how the two aspects of minimization interact and under which criteria they can be sequenced in any order (e.g. in the wellknown automata minimization, where reachability is considered first, followed by bisimilarity minimization) 
16June  Sergey Goncharov, Towards Constructive Hybrid Semantics sergeytalk160620 
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 “nonprogrammable” 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 monadbased 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 inductiveinductive type in the recent cubical extension of the Agda proof assistant, significantly using stateoftheart 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] 
09June  HansPeter Deifel, The M in CoPaR – From Partition Refinement to Minimization slidesdeifelss20 
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. 
19May  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 HennessyMilner 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 notquitefinitary functors such as the discrete distribution functor. 
12May  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 Kripkestyle or neighourhoodstyle 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 pointfree topologies (latticecomplete 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. 
5May  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 proorbitfinite topological spaces over nominal sets and show that regular data languages correspond uniquely to continuous predicates of the space of proorbitfinite words. 
28Apr  Lutz Schröder, NP Reasoning in the Monotone muCalculus monotonemu20200428 
Satisfiability checking for monotone modal logic is known to be (only) NPcomplete. We show that this remains true when the logic is extended with alternationfree fixpoint operators as well as the universal modality; the resulting logic — the alternationfree monotone mucalculus with the universal modality — contains both concurrent propositional dynamic logic (CPDL) and the alternationfree 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. 