Oberseminar

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.

Nachfragen gerne per Mail an den Seminarleiter (Prof. Dr. Lutz Schröder).

Voraussichtlicher Plan WiSe 2020/21

Name	Date	Title/Abstract

Jonas Forster	10/26/2021
Sergey Goncharov	11/02/2021	Computational Adequacy and Choice: How Deep is the Rabbit Hole? Computational adequacy together with soundness are established yardsicks for operational semantics. One can regard inductive and coinductive semantics and the emerging structures, such as natural and conatural numbers, as means for providing sound and adequate semantics, which then can betransferred to various categorical models, such as topological and metric spaces, toposes, pretoposes and type-theoretic universes. While inductive and co-inductive types are well-studied and are described by the corresponding mutualy dual universal properties, the classical view of adequacy requires a different kind of structures, suitably representing a coarse-grained view of partiality. Here, we propose a generic categorical iteration-based notion of partiality, which is arguably the most basic one. Weshow that the emerging free structures, which we dub uniform-iteration algebras enjoy various desirable properties, in particular, yield an equational lifting monad. We then study the impact of classicality assumptionsand choice principles on this monad, in particular, we establish a suitable categorial formulation of the axiom of countable choice entailing that the monad is an Elgot monad. [Based on ICALP21: “Uniform Elgot Iteration in Foundations”]
Henning Urbat	11/09/2021	Towards an Algebraic Characterization of Quantum Automata Quantum automata are to classical automata what quantum computers are to classical computers. Since the introduction of the model by Kondacs and Watrous in 1997, the class of languages accepted by quantum automata has been studied by numerous authors. However, a precise characterization (e.g. algebraic or logical) and decidability remain open problems. In this talk, we propose an algebraic perspective on quantum automata. Building on a recent general result in algebraic language theory (joint work with Fabian Birkmann and Stefan Milius) we show that the corresponding language class admits an equational axiomatization in terms of profinite equations over reduced lattice bimodules. Moreover, we present several examples of such equations.
Pedro Nora	11/16/2021
Stelios Tsampas	11/23/2021	Reasoning about Programming Languages What do we mean by “reasoning
Bastian Kauschke/Oliver Grosch	11/30/2021	Implementation of Ontological Reasoning via One-Step Satisfiability Checking Coalgebraic fixpoint logics show an exceptional expressiveness as well as semantic genericity, with the coalgebraic µ-calculus being a well-known example for these logics. Formulas of the coalgebraic µ-calculus can be checked for satisfiability in exponential time if a well-behaved set of tableau rules is provided. As such rules are not provided for every case, Hausmann and Schröder provided a global caching algorithm utilizing one-step logic to provide a way of satisfiability checking in exponential time without the need of tableau rules. In this work, we implement this algorithm in COOL, a reasoner developed by FAU and the Australian National University. Furthermore, we compare it to the previous procedure utilizing tableau rules and analyse its runtime for example formulas inthe classical and the graded µ-calculus. Syntactic NFA Minimization via SAT solving Abstract: While nondeterministic finite automata can be a lot smaller than deterministic finite automata, computing a minimal nfais known to be PSPACE-complete and therefore tends to not be practically feasible. To avoid this issue, recent work by Mayers and Urbat focused onthe easier problem of computing minimal atomic and subatomic nfas, whichhas been shown to be NP-complete. We present a new approach using union nfas, generalizing the previous results and producing smaller certificates. We have implemented our algorithm as a Rust library. Using our approach, we are able to more easily verify the absence of minimal atomic and subatomic nfas for a given language. We have shown that for most simple regular languages, there exists a minimal nfa which is atomic and subatomic.
Paul Wild	12/07/2021	Locality Games in Modal Characterization Theorems This talk puts a spotlight on a construction that is at the heart of many recent results relating modal logics to their ambient first order logics. These modal characterization theorems or van Benthem theorems state that the modal logic is precisely as expressive as the bisimulation-invariant fragment of the respective ambient logic, and make this relationship more precise by providing bounds on the rank of the relevant formulae. In the proof of such a theorem, the locality game is used in the key step of establishingthat every bisimulation-invariant formula is also local, meaning that its truth value at any state only depends on the shape of the model in a bounded neighbourhood of that state. We will show how locality games are similar to Ehrenfeucht-Fraisse games, and how they are used to establish locality of formulae, as well as highlighting how the game changes dependent on the logic or system type under investigation.
Merlin Göttlinger	12/14/2021	Concept-Indexed Epistemic Logic Abstract: We will learn about further developments of concept-indexed epistemic logic (CIEL) as an extension of epistemic modal logic for groups of agents that allows arbitraryconcepts to be placed in the index of the modalities. We show that this logic is ExpTime-complete and present the current state of axiomatizing thelogic.
Stefan Milius	12/21/2021	The Initial Algebra Theorem by Trnkov\\’a et al.~states, undermild assumptions, that an endofunctor has an initial algebra provided ithas a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite)initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point $A$ of the functor, it uses Pataraia’s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of $A$. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as anequivalent condition, overall yielding a streamlined version of the original proof.
Chase Ford	01/11/2022	Graded Monads and Behavioural Equivalence Games Abstract: Graded monads have proven to be a fruitful tool for for the uniform analysisof a variety of phenomena surrounding the behavioural semantics of state-based systems, forming the core of so-called graded semantics (a coalgebraic framework of spectra of behavioural semantics á la van Glabbeek). Indeed, existing work has revealed applications of graded monads in (i) the modelling of behavioural equivalences and (ii) the extraction of characteristic modal logics from a given semantics (via graded algebras). More recently, graded semantics and their logics have been extended to preorders and metrics. Traditionally, behavioural semantics have also been described via Ehrenfeucht-Fraïssé style games in which a Duplicator aims toprove that a given pair of states are equivalent under the semantics at hand, whereas a Spoiler has the ambition of proving the opposite. In this talk, we will describe an approach to the extraction of behavioural equivalence games for graded behavioural equivalences on Set-based coalgebras based on the theory of graded algebras. Thus, we obtain a uniform game format for behavioural equivalences ranging from (probabilistic) trace equivalence on (probabilistic) LTS to neighborhood bisimulation on neighborhood frames, and beyond.
Fabian Birkmann	01/25/2022	The Nominal Reiterman Theorem Abstract: We provide a pro-equational method of axiomatization for pseudovarieties of nominal monoids in the style of a Reiterman Theorem. To this end, we extend the nominal topological dictionary to describe the pro-completion of support-bounded subcategories of the category of orbit-finite sets. This setting allows the construction of profinite nominal monoids as carriers for a nominal version of profinite equations. However, when compared to a similar recent result by Milius and Urbat, the pseudovarieties of nominal monoids axiomatizable by such nominal pro-equations admit closure under a rather weak notion of quotient.
Hans-Peter Deifel	02/01/2022	Computation in Nominal Sets – a survey The theory of nominal sets is an elegant formalism for dealing with names in computer science, e.g. bound names in programming languages or logic. Additionally, they provide a nice setting where certain infinite structures admit a finite representation. This fact has been used to describe and implement algorithms on infinite data as well as whole programming languages that facilitate programming over infinite data. In this talk, I will give an overview of different approaches for computation with nominal sets, evaluate their strengths and weaknesses and highlight specific challenges for designing algorithms on nominal sets.
David Wegmann/Tadeusz Litak	02/08/2022