Vorträge im SoSe 2020 - Lehrstuhl für theoretische Informatik 8

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 (mailto:lutz.schroeder@informatik.uni-erlangen.de).

Voraussichtlicher Plan SoSe 2020

January 2025

Thursday, January 16

LICS'25 Abstract Deadline

AoE

Vorträge

Date	Speaker, Topic	Abstract
10-August	Pedro Nora, Hausdorff coalgebras [pdf-embedder url=”https://www8.cs.fau.de/ext/teaching/sose2020/oberseminar/nora-talk.pdf”]	As composites of constant, finite (co)product, identity, and powerset functors, Kripke polynomial functors form a relevant class of SET-functors 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 quantale-enriched categories. To assume the role of the powerset functor we consider “powerset-like” functors based on a quantale-enriched version of the Hausdorff metric. As a starting point, we show that for a lifting of a SET-functor 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 Cantor-like argument, we observe that Hausdorff functors on categories of quantale-enriched categories do not admit a terminal coalgebra. Finally, in order to overcome these “negative” results, we combine quantale-enriched categories and topology.
04-August	Daniel Hausmann, Harnessing LTL With Freeze Quantification [pdf-embedder url=”https://www8.cs.fau.de/ext/daniel/hausmann-mubar.pdf”]	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 [pdf-embedder url=”https://www8.cs.fau.de/ext/teaching/sose2020/oberseminar/welzenberg-talk.pdf”]	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.
23-June	Thorsten Wißmann, Reachability vs Bisimilarity Minimization [pdf-embedder url=”https://www8.cs.fau.de/ext/teaching/sose2020/oberseminar/wissmann-reach-vs-bisim.pdf”]	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 well-known automata minimization, where reachability is considered first, followed by bisimilarity minimization)
16-June	Sergey Goncharov, Towards Constructive Hybrid Semantics [pdf-embedder url=”https://www8.cs.fau.de/wp-content/uploads/media/sergey/sergey-talk-16-06-20.pdf”]	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 [pdf-embedder url=”https://www8.cs.fau.de/wp-content/uploads/2020/06/slides-deifel-ss20.pdf”]	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 [pdf-embedder url=”/wp-content/uploads/2020/06/wild.pdf”]	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 [pdf-embedder url=”/wp-content/uploads/media/ss20/ober/urbat.pdf”]	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 [pdf-embedder url=”/wp-content/uploads/media/ss20/ober/monotonemu20200428.pdf”]	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.