Oberseminar (SoSe 2024)
Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:1515:45 in Raum 00.131128 (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.
Bei Nachfragen gerne per Mail an den Seminarleiter (Prof. Dr. Lutz Schröder), Anmeldung zur Mailingliste: TCSSeminar Mailinglist
Vorträge
Previous Talks  
Tuesday, 27/08/2024 
Towards Generalizing Probability Monads
Slides
AbstractThis 45minutestalk will cover some probability monads, and generalizations. In the first section, we will encounter some classical probability monads. This will lead us to weakened products and the framework of Markov categories. As a short demonstration of this formalism, we will consider (a categorical version of) de Finetti’s theorem.
The second part then addresses generalizations: imprecise probabilities, such as DempsterShaferbelief functions, model situations with insufficient knowledge. Do they fit into the framework of Markov categories? Do they even have probability monads? This is still an open question. Noncommutative probability is another way of generalization; I will shortly show how this is formulated in terms of C*algebras, and point to recent results on involutive / quantum Markov categories. 
Tuesday, 09/07/2024 
Enveloping tensor categories
AbstractDeligne constructed in 2004 a tensor category (= abelian, symmetric, monoidal category) Rep S_t, depending on a complex parameter t$, which interpolates the categories of representations of the symmetric groups S_n, n>=0. Subsequently, I found an intrinsic construction of this category which applies to many more situations. Roughly, one starts with a regular category and deforms its category of relations. The main results are: A simple criterion for this deformed category to be semisimple and, if this is the case, a formula for the tensor product multiplicities and dimensions of simple objects.

Tuesday, 02/07/2024 
Nominal Tree Automata with Name Binding
AbstractTrees as datastructures are an omnipresent concept in computer science, no matter if in description languages, process communication, data storage and access or descicion making algorithms. While there are automata model that handle treelike words incorporating data semantics, i.e. somehow manage an infinite alphabet, these mechanisms typically have undecidable or at least nonelementary decision problems if not resticted. Our newly introduced automaton model, Regular Nominal Tree Automata, is designed to recognise tree languages over an infinite alphabet, offering elementary complexity for relevant decision problems while retaining a useful level of expressiveness.
Since the results presented in this talk are subject of our recently accepted CONCUR paper extending the results of my masters thesis, we will briefly recall its central fundamentals and further have a look at our main result, decidability of language inclusion for RNTA, garnished with some illustrative examples. 
Tuesday, 02/07/2024 
Deallocation Sequences
AbstractWhile most name binding mechanisms in formal languages like the mu calculus adhere to scopes of properly nested parentheses, in programming languages with explicit memory allocation and deallocation commands like C we are well used to interleaving scopes of allocated memory in the run of a programme. Bar Languages as data languages only offer allocation operations for names, where the implicit deallocation is taking place as soon as a name is not expected to be seen again. In Dynamic Sequences the deallocation of names is made explicit by adding closing brackets for prior bound names. We are going to have a look at the aforementioned notion of explicit memory deallocation and a comparable, but not identical notion of name allocation and deallocation, naturally extended from the functorial description of bar languages, before we have a look at its properties and notions of alphaequivalence.

Tuesday, 25/06/2024 
Learning Bar Languages like Angluin
AbstractDuring this talk, I will present research results from my cooperation with Jurriaan Rot in Nijmegen. Active automata learning is a technique for inferring the behaviour of unknown finitestate machines through iterative interaction with a “helpful” source of examples. These algorithms construct accurate models with minimal assumptions by systematically generating and analysing queries. First introduced by Dana Angluin (1987), I will briefly introduce general active automata learning before presenting a generalised active learning algorithm for RNNArecognisable bar languages, which are languages over an infinite alphabet where there is an alphaequivalence on words. Schröder, Kozen, Milius, and Wißmann introduced regular nondeterministic nominal automata (RNNA) in their FOSSACS ’17 paper and provided a finite representation using NFAs. The presented generalised learning algorithm will make apt use of this equivalence by transforming any active learning algorithm for regular languages into a learning algorithm for RNNArecognisable bar languages.

Tuesday, 18/06/2024 
Fibrations, Topological Categories, and Behaviour with Structure
AbstractA series of recent papers on quantitative semantics in coalgebra successfully employed certain fibrations, corresponding roughly to topological categories, to equip the semantics of coalgebras with a fairly abstract notion of structure. In this talk, we give an overview of the fundamental definitions and discuss several recent results in this area, including a general construction of lifting functors to the relevant categories and properties of these liftings, modal logics and HennessyMilner theorems, as well as game theoretic characterizations of the induced semantics. Along the way, we highlight where the increased level of abstraction sacrifices the strength of results compared to more concrete instantiations. We conclude by discussing how to incorporate the above concepts with graded semantics.

Tuesday, 11/06/2024 
New Semantics for Separation Logic
AbstractA recent thesis by Hiep shows that separation logic does not have the compactness property and hence no effective, sound and complete axiomatisation exists. Following a paper by de Boer, Hiep and de Gouw I will present a new semantics of separation logic with infinite heaps. We will see that arbitrary infinite heaps also lead to noncompactness but a restriction to firstorder definable heaps yields a proof theory that has the compactness property. Finally, I will show a sound and complete sequent calculus for separation logic restricted to firstorder definable heaps.

Tuesday, 04/06/2024 
Towards a BigStep HigherOrder Mathematical Operational Semantics
Slides
AbstractReasoning on operational semantics is generally a challenging and laborious task. Fortunately, different styles and formats of operational semantics allow one to rigorously classify language features, and reason about them abstractly. One of these rule formats is GSOS that covers smallstep semantics for firstorder languages. GSOS has been equipped with a categorical presentation and an abstract framework, but it does not support higherorder languages. A recent effort has solved this issue by inventing higherorder GSOS, and its abstract framework. Generally, besides smallstep flavor of operational semantics there exists another variant named bigstep operational semantics. HOGSOS can be used for reasoning on the earlier. It is beneficial to have a rule format and its abstract framework that represents bigstep operational semantics, and the main purpose of this talk is to reach to the starting point of this problem, where one has gained motivation to go further.

Tuesday, 28/05/2024 
Labeled Tableaux for Łukasiewicz Fuzzy Description Logic with Inverses
AbstractThis bachelor thesis presents an extension of the labeled tableau calculus rules for the Attributive Language with general Complement and Łukasiewicz fuzzy interpretation. Derivation rules are introduced that offer the ability to prove satisfiability for inverses of atomic roles. Soundness and completeness of the calculus is shown to be preserved after introducing the (L) and (R)rules. Lastly, we give also a short insight into that calculus’s computational complexity bound.

Tuesday, 28/05/2024 
Implementierung der Übersetzung von ATL* in den AlternatingTime µKalkül
AbstractIm Rahmen der Präsentation wird die angefertigte Bachelorarbeit “Implementierung der Übersetzung von ATL* in den AlternatingTime µKalkül” vorgestellt. Nach der Einführung der beteiligten Logiken ATL* und AMC sowie des zentralen Übersetzungsalgorithmus werden dessen Teilschritte anhand konkreter Beispiele verständlich gemacht. Stellvertretend für die gesamte Implementierung wird anschließend eine eingebaute Optimierung erläutert. Am Ende bietet sich die Möglichkeit, die Implementierung anhand eines konkreten Beispiels nachzuvollziehen.

Tuesday, 14/05/2024 
A SteadyState Operator for Probabilistic Graded Fixpoint Logics
AbstractGraded monads and their logics provide a framework for compositional logics for the linear timebranching time spectrum. Compositionality of graded logics however requires homomorphy of all operations in grade 0 of the monad. In probabilistic trace logics in particular, this results in a rather unsatisfying logical extension for the classical extremal fixpoints μ and ν. In this setting, the notion of stationary distributions is of great interest and at first glance appears to be a fixpoint of some sort. In this talk we explore how the steadystate distribution of finite markov chains is connected to probabilistic graded fixpoint logics.

Tuesday, 07/05/2024 
Initial Algebras Unchained – A Novel Initial Algebra Construction Formalized in Agda
Agda Formalization Slides
AbstractThe initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initialalgebra construction by Adámek (1974) starts with the initial object (e.g. the empty set) and successively applies the functor until a fixed point is reached, an idea inspired by Kleene’s fixed point theorem. Depending on the functor of interest, this may require transfinitely many steps indexed by ordinal numbers until termination.We provide a new initial algebra construction which is not based on an ordinalindexed chain. Instead, our construction is loosely inspired by Pataraia’s fixed point theorem and forms the colimit of all finite recursive coalgebras. This is reminiscent of the construction of the rational fixed point of an endofunctor that forms the colimit of all finite coalgebras. For our main correctness theorem, we assume the given endofunctor is accessible on a (weak form of) locally presentable category. Our proofs are constructive and fully formalized in Agda. Accepted for publication in LICS 2024.

Tuesday, 07/05/2024 
Test Case Generation for Zephyr RTOS Semaphores from PlusCal Specifications
AbstractCertification of software in safetycritical domains is subject to strict legal requirements. This poses a challenge for opensource software, such as the Zephyr realtime operating system. In comparison to proprietary software, the lack of standardized processes during development makes proving compliance with the requirements more difficult. To approach this issue, we propose to apply modelnased testing with model checkers to Zephyr. Based on the existing implementation in Zephyr, we create a formal specification of semaphores in the PlusCal language. We then use the model checker TLC to produce counterexamples, which represent traces through the system model. From these, runnable test cases in C are generated.

Tuesday, 30/04/2024 
Design of a TableauBased Automated Theorem Prover and Output of MachineCheckable Proofs
AbstractAutomated deduction is the use of computer programs to automatically prove mathematical theorems. It can be used to detect bugs in critical systems, or to help demonstrate mathematical proofs. This talk focuses on the presentation of Goéland, a concurrent tableaubased automated theorem prover, and the main challenges it faces. These challenges include the implementation of a fair tableaubased proof search procedure in firstorder logic, the handling of theory reasoning (equality, set theory, etc.), and the generation of machinecheckable proofs, i.e., proofs that can be verified by external tools (Coq, Lambdapi).

Tuesday, 23/04/2024 
Towards an Algebraic Theory for Stochastic Languages
AbstractFinite Probabilistic Automata (FPA), as introduced by Rabin in 1963, are a generalization of finite automata to the probabilistic setting. Even though FPA are generally more powerful acceptors than DFA, Rabin showed that the connection is tight: The cutpointlanguage accepted by an FPA is regular if the cutpoint is isolated; furthermore, similarly to regular languages, stochastic languages enjoy a number of algebraic closure properties. But while the automatatheoretic perspective on stochastic languages has constructed a deep and fruitful theory, almost no algebraic theory of stochastic languages has been developed since their introduction. In this talk we make first steps towards such an algebraic perspective on stochastic languages based on (monoids of) convex sets. We recall the basic algebraic and categorical foundations of convex sets (also known as barycentric algebras) and work our way towards a suitable algebraic acceptor model. Finally, we show some first result on expressivity and discuss some drawbacks of this approach with respect to canonicity.
