Oberseminar (SoSe 2024)

This 45-minutes-talk 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 Dempster-Shafer-belief 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. Non-commutative 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.

Deligne 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.

Trees 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 tree-like words incorporating data semantics, i.e. somehow manage an infinite alphabet, these mechanisms typically have undecidable or at least non-elementary 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.

While 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 alpha-equivalence.

During 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 finite-state 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 RNNA-recognisable bar languages, which are languages over an infinite alphabet where there is an alpha-equivalence 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 RNNA-recognisable bar languages.

A 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 Hennessy-Milner 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.

A 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 non-compactness but a restriction to first-order 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 first-order definable heaps.

Reasoning 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 small-step semantics for first-order languages. GSOS has been equipped with a categorical presentation and an abstract framework, but it does not support higher-order languages. A recent effort has solved this issue by inventing higher-order GSOS, and its abstract framework. Generally, besides small-step flavor of operational semantics there exists another variant named big-step operational semantics. HO-GSOS can be used for reasoning on the earlier. It is beneficial to have a rule format and its abstract framework that represents big-step 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.

This 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.

Im Rahmen der Präsentation wird die angefertigte Bachelorarbeit “Implementierung der Übersetzung von ATL* in den Alternating-Time µ-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.

Graded monads and their logics provide a framework for compositional logics for the linear time-branching 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 steady-state distribution of finite markov chains is connected to probabilistic graded fixpoint logics.

The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra 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 ordinal-indexed 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.

Certification of software in safety-critical domains is subject to strict legal requirements. This poses a challenge for open-source software, such as the Zephyr real-time 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 model-nased 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.

Automated 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 tableau-based automated theorem prover, and the main challenges it faces. These challenges include the implementation of a fair tableau-based proof search procedure in first-order logic, the handling of theory reasoning (equality, set theory, etc.), and the generation of machine-checkable proofs, i.e., proofs that can be verified by external tools (Coq, Lambdapi).

Finite 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 cutpoint-language 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 automata-theoretic 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.