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

—

Bisherige Vorträge

Date Speaker, Topic Abstract
12-Feb Matthias Zinner, // Integrating CTLf into NuSMV // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/slideshandout.pdf”] The focus of the presentation is to give a short introduction to CTLf and explain its integration into NuSMV. In particular, the parsing process, model checking and trace generation implementation is discussed. Also, the relationship between existing fairness mechanics for CTL and CTLf is described.
12-Feb Tadeusz Litak, // Be fair to CTL // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/befairtoctl_feb2019.pdf”] I present an ongoing work on expressive power and model-checking aspects of CTLf, an extension of CTL with a binary “fairness” connective, proposed recently for model-theoretic reasons by Ghilardi & van Gool (LiCS 2016). I will recall fairness-capturing extensions of CTL proposed in 1980’s (ECTL, FCTL, GFCTL, ECTL+… ) and sketch how CTLf relates to (at least some of) them. Apart from highlighting CTLf model-checking advantages, I will also briefly discuss the possibility of using efficient parity-games for modal mu-calculi. This talk incorporates discussions with Christoph Rauch and Daniel Hausmann, and provides an introduction to the following presentation of Matthias Zinner’s master project.
5-Feb Miriam Polzer, // Towards Weakest Precondition Calculus for Local Store // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/polzer-slides.pdf”] Inspired by Hasuo’s approach to weakest precondition semantics, I will show how to obtain a predicate transformer that may provide a weakest precondition calculus for local store monads. We will recapitulate the presheaf structures admitting a notion of being ‘indifferent to privately allocated locations’ and then, starting from a full local store monad T, we will construct a submonad R that provides propositions suitable for allocation of new memory cells. Ultimately, we will see how postconditions that depend on newly allocated locations are naturally transformed into preconditions that only depend on already existing store. Along the way, we will also encounter the connection required to unify work on local store by Plotkin/Power and Kammar et al.
22-Jan Hans-Peter Deifel, // An Efficient Coalgebraic Partition Refinement Algorithm, Implemented // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/deifel-slides.pdf”] Partition refinement is an algorithmic schema used in well known algorithms such as Hopcroft’s DFA minimization, the Paige-Tarjan-Algorithm and Markov chain lumping. In this talk, I present the implementation of an efficient partition refinement algorithm in Haskell that unifies these algorithms on the level of coalgebras. The implementation is generic in the type functor and can be easily instantiated for different kinds of transition systems, (1) by implementing new type functors in Haskell and (2) by combining the implemented functors when running the implementation. The implementation is based on the algorithmic framework by Thorsten Wißmann, Ulrich Dorsch, Stefan Milius and Lutz Schröder. I will also highlight a new instance for weighted tree languages where this algorithm beats the running time complexity of competing algorithms.
22-Jan Michael Gebhard, // Development of a Programming Environment and Interpreter for LOOP and WHILE // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/gebhard-slides.pdf”] In this thesis, we provide an intuitive programming environment for the languages LOOP and WHILE. Our tool is designed for educational use in introductory lectures on theoretical computer science such as ThInfWiL at FAU. We define syntactic extensions to both languages (Section 2) in order to make them practically usable in programming exercises, in particular we introduce macros which allow a programmer to reuse code (Section A.6 and Subsection A.9.16) and arbitrary identifiers for storage locations (Section A.5). Then we build an interpreter for these extended languages (Section 3) along with a plugin for the integrated development environment IntelliJ IDEA (Section 4), in order to allow students to solve programming exercises in a familiar environment.
15-Jan Ulrich Dorsch, // Depth-1 Graded Monads and The Linear Time – Branching Time Spectrum // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/udorsch_ws18.pdf”] Graded monads can be used in a uniform and purely coalgebraic approach to capture various notions of equivalences on the linear time – branching time spectrum: completed traces, ready/failure traces, simulation semantics, etc. In particular we will present graded monads for that purpose that can be defined via (depth-1) graded theories.
8-Jan Merlin Göttlinger, // Trichotomic Argumentation Representation // [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/merlin-talk.pdf”] The Aristotelian trichotomy distinguishes three aspects of argumentation: Logos, Ethos, and Pathos. However, current argumentation frameworks are mostly focused on the Logos aspect. We present the Trichotomic Argument Interchange Format (T-AIF) to additionally capture the other two aspects when representing dialogical argumentation.

We will recap existing argumentation frameworks to see where we extend the capabilities of the status quo. We will then look at interesting properties definable on our structure as fuzzy formulas to profile the discussion participants.
11-Dec Paul Wild, Lax extensions for fuzzy relations [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/wild-slides.pdf”] In the theory of coalgebras, lax extensions provide a way to identify relation liftings for which the ensuing notion of bisimulation captures behavioural equivalence. A relation lifting takes relations on AxB to relations on the set TAxTB, where T is the set functor under consideration.

In this talk, we will establish a notion of lax extension for fuzzy relations, that is maps assigning to each pair of elements a degree of relatedness from the unit interval [0,1]. We will then investigate how some of the properties of the usual lax extensions hold up in the real-valued case and how this relates to the Kantorovich and Wasserstein liftings for pseudometrics presented in previous talks.
4-Dec Daniel Hausmann, Optimal Satisfiability Checking for the Coalgebraic μ-Calculus [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/hausmann.pdf”] Previous work on the coalgebraic mu-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded mu-calculus, or real-valued weights in combination with non-linear arithmetic. We prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying so-called one-step logic, roughly described as the nesting-free next-step fragment of the logic.

Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded mu-calculus with Presburger arithmetic, as well as an extension of the (two-valued) probabilistic mu-calculus with polynomial inequalities. As a side result, we moreover obtain a new upper bound O(((nk)!)((nk)!)) on model size for all coalgebraic mu-calculi, where n is the size of the formula and k its alternation depth.
27-Nov Frederik Haselmeier, Early and Late Transition Relations in the pi-Calculus and their Bisimulations [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/picalculus.pdf”] 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 [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/verighc_nov2018.pdf”] 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 [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/goncharov-talk.pdf”] 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 [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/neves-slides.pdf”] 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 [pdf-embedder url=”/wp-content/uploads/media/ws18/ober/wissmann-talk.pdf”] (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).