Theoretische Informatik

Vorträge im WS 2018

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15–15:45 in Raum Raum 00.131, Cauerstraße 11 statt. 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 für WS 2018

Date Speaker Room Topic, Abstract
11-Dec Paul Wild 00.131-128
08-Jan Christoph Rauch 00.131-128
08-Jan Ulrich Dorsch 00.131-128
15-Jan Merlin Göttlinger 00.131-128
22-Jan Hans-Peter Deifel 00.131-128
22-Jan Michael Gebhard 00.131-128
29-Jan Fabian, Fabian 00.131-128
05-Feb Miriam Polzer 00.131-128
12-Feb Tadeusz Litak 00.131-128

Bisherige Vorträge

Date Speaker, Topic Abstract
27-Nov Frederik Haselmeier, Early and Late Transition Relations in the pi-Calculus and their Bisimulations [slides] The pi-calculus is a theoretical framework for modelling communicating processes. It is an extension of the calculus of communicating systems (CCS), which among several other changes adds name passing to the system. Passing names involves instantiating a name in the receiving process by substituting a placeholder with the received name. There exist two different variants of the pi-calculus' transition relations that instantiate names at different times. The early relations instantiate names as soon as the input can be inferred, while the late relations push instantiation down to rules that infer the interactions between processes. In my presentation we will take a close look at the early and late version of the transition relations as well as what kinds of bisimulations can be defined for them. Additionally, it will be shown that these bisimilarities do not form congruences, but that they can be made into congruences by requiring one additional condition.
20-Nov Peter Trommler, Separation Logic for GHC's Cmm Language [slides] Cmm is the intermediate language in the Glasgow Haskell Compiler (GHC) that is the basis for GHC's backends. I will present a small-step semantics for Cmm statements in continuation-passing style and a Separation Logic also in continuation-passing style. A formalisation in Coq will be based on CompCert by Xavier Leroy et.al. and the Verified Software Toolchain by Andrew Appel et. al.
13-Nov Sergey Goncharov, From Delay Monad to Duration Monad: An Excursion into Non-Inductive Semantics [slides] Classical approaches to semantics include operational, denotational and logical aspects whose presence and mutual formal connections are highly valued as witnesses of complete, robust and well-founded design, suitable for implementation, maintenance and analysis. The connections between operational and denotational semantics are regulated by soundness and adequacy theorems, in conjunction with the postulates of classical domain theory leading to an inductive style of semantics, i.e. the one where, on the one hand, operational semantic judgements are derived by structural induction and, on the other hand, fixpoints are denotationally interpreted as least fixpoints. In my talk I focus on an instructive case of non-inductive semantics carried by Capretta's delay monad, and present a monad, called the duration monad, closely related to the latter. I demonstrate the use of the duration monad as a lightweight semantic domain for a while-language for hybrid programming recently developed in collaboration with R. Neves. This is further justified by small-step and big-step operational semantics and the corresponding adequacy theorem.
6-Nov Renato Neves, A Uniform Theory of Hybrid Automata [slides] Able to naturally encode discrete and continuous transitions at the same time, hybrid automata are the standard formalism for hybrid systems. Thus not surprisingly, they have a very rich theory which includes notions of bisimulation, decidability results, and extensions for accommodating new types of behaviour.

In this talk we will visit hybrid automata from a coalgebraic point of view. We will see that such a perspective promotes a generic theory of hybrid automata that addresses variability in their underlying definition and corresponding notions. In practice, this makes possible to study and develop different types of hybrid automata in a completely uniform manner.

We will also see that the coalgebraic perspective provides, almost for free, a rich palette of definitions and results that were not previously considered in hybrid automata literature. This includes notions of bisimulation and behaviour, state minimisation techniques, and regular expression languages.
30-Okt Lutz Schröder, Expressive Trace Logics via Graded Monads (Joint work with Ulrich Dorsch and Stefan Milius)

In earlier work we have introduced a generic notion of trace semantics for coalgebras based on mapping the type functor into a graded monad. Graded monads correspond to a notion of graded algebraic theory where operations come with assigned depths and equations are required to be of uniform depth. For graded monads that are depth-1, i.e. presented by operations and equations of depth at most 1, we have a compositional notion of graded algebras, which then serve as formulas of a trace logic, with evaluation induced by the free algebra property of the graded monad. Here, we refine this notion of trace logic with a systematic treatment of propositional operators, and complement the previous invariance result with a generic criterion for expressiveness of such logics, a result that simultaneously subsumes expressiveness of the standard logic for trace semantics of LTS and the coalgebraic Hennessy-Milner theorem.
23-Okt Thorsten Wißmann, Path Categories for free for coalgebras with non-determinism [slides] (Joint work with Jérémy Dubut, Shin-ya Katsumata, Ichiro Hasuo) Abstract: There are different categorical approaches to (variations of) transition systems and their bisimulations. One approach is coalgebra for an endofunctor F, where a bisimulation is defined to be a span of F-coalgebra homomorphism. Another one is in terms of path categories and open morphisms, where a bisimulation is defined to be a span of open morphisms.

This similarity is no coincidence, and Lasota has already shown how every open morphism situation induces a functor F such that the open morphisms become coalgebra homomorphisms. In this talk, we introduce the converse direction: given an endofunctor F, fulfilling certain conditions, we look at the pointed F-coalgebras and lax F-coalgebra homomorphisms, in order to define a path-category such that the open morphisms turn out to be precisely the (proper) F-coalgebra homomorphisms.

The above construction provides path categories for free for different flavours of transition systems:

(1) non-deterministic tree automata, including ordinary labelled transition systems

(2) multisorted transition systems, which are the target domain of Lasota's construction for arbitrary open morphism situations. So our work covers essentially all systems that can be modelled by open morphisms.

(3) regular nondeterministic nominal automata (RNNA), an expressive automata notion living in nominal sets. Here, the induced path category turns out to be the partial order of so-called 'bar strings' (in prefix order).