Vorträge im WS 2019
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).
Vorträge
| Date | Speaker, Topic | Abstract |
| 4-Feb | Florian Frank, Implementation and Analysis of an Algorithm for Computing Canonical Non-Deterministic Automata [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/florian-frank.pdf” ] | In this Bachelor Thesis, we look at a specific algorithm for constructing a canonical non-deterministic automaton, which is closely related to Brzozowski’s algorithm for DFA minimization. For this purpose, we use non-deterministic closure automata, since then this algorithm can construct a state-minimal NFA in some cases. We will present the resulting implementation, and statistically relevant test data the algorithm has produced. |
| 28-Jan | Chase Ford, First-order Logic on Infinite Trees [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/slides-ford.pdf” ] | This talk concerns matters arising at the interface of automata theory and mathematical logic. We will first explore some progress towards a characterization of those (unranked, serial) tree languages which are definable by formulas in first-order logic with an ancestor relation as a class of alternating parity automata. In particular, a first-order sandwich will be served: two closely related classes of automata will be introduced and shown to bound the expressive power of first-order logic over such structures. In turn, we will explore the bisimulation-invariant fragment of the lower-bound of this sandwich. Finally, a conjecture relating the bisimulation-invariant fragment of these automata and CTL will be formulated. This talk is based on my masters thesis, Investigations into the Expressiveness of First-order Logic and Weak Path Automata on Infinite Trees, written under the supervision of Yde Venema and Sam van Gool. |
| 21-Jan | Hans-Peter Deifel, Nominal Sets, Data Symmetries and OrdNom [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/slides-deifel.pdf” ] | I will give an introduction to the theory of nominal sets as formulated by Gabbay and Pitts, generalize this notion to Data Symmetries along the lines of BojaÅ„czyk et. al. and present various representation theorems. Finally, I will take a look at the category of Ordered Nominal Sets, where nominal sets have an especially convenient representation. |
| 14-Jan | Georg Struth, Verifying Hybrid Systems with Interactive Theorem Provers [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/struth-slides.pdf” ] | Hybrid systems integrate continuous dynamics and discrete control. A prominent approach is differential dynamic logic (dL), a modal logic for reasoning about ordinary differential equations and their solutions within hybrid programs. Over the last decade, a domain-specific sequent calculus for dL has been developed together with an intricate explicit substitution calculus for it. It has been integrated into the KeYmaera X tool and proved its worth in numerous case studies. This talk presents an algebraic reconstruction of this approach and the first verification and refinement components in an interactive proof assistant inspired by it. Our components are based on shallow embeddings in which the proof theory of dL is by and large replaced by semantic equational reasoning about orbits and trajectories of dynamical systems in combination with discrete state updates. We use algebras, in particular variants of Kleene algebras and predicate transformer algebras, for automatic verification condition generation. We currently support a component for reasoning with weakest liberal preconditions, a Hoare logic and a refinement calculus for hybrid programs. These allow us to verify hybrid programs in various ways: starting from hybrid program specifications based on ordinary differential equations, we can certify solutions of locally Lipschitz-continuous vector fields using the Picard-Lindelöf theorem and then reason explicitly about them. Alternatively we can represent solutions of continuous vector fields implicitly by invariant sets. Finally, we can analyse hybrid program that specify trajectories or orbits of hybrid systems directly. Apart from presenting the algebras used and their extension and instantiation to hybrid program semantics, I will present some examples, comment on the intricacies of formalising the approach within the Isabelle/HOL proof assistant, and outline some future directions for this line of work, time permitting. This work is joint with Jonathan Julián Huerta y Munive, and partially funded by CONACYT. |
| 7-Jan | Merlin Göttlinger, The Alternating-Time µ-Calculus With Disjunctive Explicit Strategies [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/goettlinger-slides.pdf” ] | I will talk about joint work with Lutz and Dirk where we generalise the ATL extension ATLES to the full µ-calculus and moreover introduce the notion of disjunctive strategies. We treat this extended logic in the framework of coalgebraic modal logic, reducing reasoning problems to the much simpler one-step fragment of our logic. |
| 17-Dec | Miriam Polzer, Local Local Reasoning: Separation Logic for Full Ground Store [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/polzer-slides.pdf” ] | We construct categorical semantics of a higher order logic over local store, i.e. a logic meant for programs with dynamic memory allocation and automatic garbage collection. Facilitating methods known from topos theory, the main result is an internally complete BI algebra which, contrary to existing generic approaches, does not arise from a monoid object. |
| 10-Dec | Mathias Zinner, NuSMV, CTL and Compassion | CTL does not support fairness statements and constraints. Several extensions have been proposed to solve this issue. Unfortunately, those that keep at most quadratic complexity of model checking tend to be unable to express strong fairness constraints, or at least not concisely so. Jointly with Hausmann, Litak and Rauch, we have investigated theoretically extensions of CTL which circumvent these problems. In this talk (based on the contents of my Master’s Thesis), I present an implementation of these extensions extending CTL model checking in a popular tool NuSMV. In particular, my implementation repairs the problem of the unsupported COMPASSION keyword. Furthermore, I discuss examples and benchmarks illustrating the correspondence between our compassionate NuSMV specifications and equivalent parity games, comparing the performance of the present implementation with various parity game solving tools. |
| 10-Dec | Christoph Rauch, Recursion for the Masses, [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/rauch-slides.pdf” ] | Many if not most tasks in actual programming require the use of tools like recursion or iteration; these tasks, however, differ a lot conceptually; you might want to tear down a data structure recursively, or build up another (possibly of infinite size); you might also like to perform a (monadic) computation iteratively. There is also a zoo of theoretical ideas on how to perform these tasks. We have initial algebras, final coalgebras, Elgot algebras, (very) recursive coalgebras, (guarded) iterative/Elgot monads, and more. I will give a brief overview of the connection between the tasks and the tools (and between the theoretical ideas themselves), and explore how recent developments on the theory side might help to solve even more types of problems more cleanly and idiomatically |
| 3-Dec | Grigory Olkhovikov, On Generalizations of the Modal Characterization Theorem | The Modal Characterization Theorem by J. van Benthem, which shows the basic modal logic to be exactly the bisimulation-invariant fragment of first-order logic, has become a template for many similar subsequent results. In this talk we will be mainly interested in the results that are related to fragments of first-order logic resembling the sets of standard translations of some intensional propositional logic. We will survey some of the existing results by other authors, but the main focus will be on our own generalization of Modal Characterization Theorem presented in [1]. This theorem depicts, in effect, a general algorithm allowing to compute the definition of bisimulation relation characterizing any given fragment of FOL which falls within a reasonably wide class of well-behaved fragments. We will discuss which of the earlier results are covered by the main result of [1] and what can be done to extend this theorem to cover some other known variants of the Modal Characterization Theorem |
| 26-Nov | Tim Lukas Diezel, Constructive Hybrid Semantics in Cubical Agda [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/slides_tim_lukas_diezel.pdf” ] | Recently, hybridness has been recognized as a computational effect laying the foundation for sematics of hybrid systems – systems consisting of both discrete and continuous behaviour. As more and more (discrete) computer programs interact with their physical (continuous) environment, cyber-physical modelling is an increasingly important field of research. In order to provide semantics for hybrid computations, a hybrid monad was developed together with a lightweight counterpart called duration monad. In my bachelor thesis I give a new definition of the duration monad in terms of a free algebraic structure, which is in contrast to the original definition constructive, and also more general. The results are then formalized in Cubical Agda, an extension of the proof assistant Agda with full support for homotopy type theory. My construction essentially relies on advanced features of Cubical Agda in particular higher inductive types. |
| 19-Nov | Johannes Kern, A web-based interface to the LOOP/WHILE interpreter and debugger [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/johannes_slides.pdf” ] | In this Master’s Project, we developed a web interface to the Loop/While Interpreter which is intended to be used in lectures like ThInfWiL. We will give a short overview of the software architecture, usage and the integrated tutorial. |
| 12-Nov | Paul Wild, A Characterization Theorem for Real-Valued Coalgebraic Modal Logic [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/wild-slides.pdf” ] | We consider a variant of coalgebraic modal logic where predicate liftings are defined in terms of the fuzzy powerset functor QX = (X -> [0,1]) and formulas thus take on real values between 0 and 1. A set of these predicate liftings gives rise to a notion of behavioural distance based on the Kantorovich lifting and we show that: i) every formula of real-valued coalgebraic ML is a non-expansive map with respect to this distance ii) every non-expansive map can be approximated by modal formulas. Finally, we show that for non-expansive formulas from a suitable first-order correspondence language (which we call real-valued CPL), the result can be strengthened by bounding the rank of approximating formulas, thus giving rise to a van Benthem theorem for real-valued coalgebraic logics. |
| 05-Nov | Thorsten Wißmann, A Coalgebraic View on Reachability [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/wissmann-slides.pdf” ] | We first introduce pointed coalgebras and discuss some examples. We then provide an iterative construction of the reachable part of a given pointed coalgebra that resembles the standard breadth-first search procedure to compute the reachable part of a graph. The construction assumes a factorization system and that the coalgebraic functor preserves wide intersections. We discuss both assumptions in different settings. While the assumptions are fulfilled easily in sets and similar categories, we see that among Kleisli categories only some have a factorization system. As a fix, we provide a reduction of the reachability in the Kleisli category to reachability in the base category. Thus, the reachable part of a pointed coalgebra in a Kleisli category can be computed in the base category. |
| 29-Oct | Daniel Hausmann, Quasipolynomial Computation of Nested Fixpoints [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/hausmann-slides.pdf” ] | In this talk, we will see how the main idea behind Calude et al.’s breakthrough quasipolynomial time algorithm for solving parity games extends to the computation of solutions of fixpoint equations involving arbitrary set-functions. We show that the recent concept of universal graphs can be used to transform the parity condition of equation systems to a safety condition encoded by a single greatest fixpoint, while increasing the size of the carrier sets only by a quasipolynomial factor. Furthermore we show that the problem of solving systems of fixpoint equations is contained in both NP and Co-NP. Time admitting, we will also see how Zielonka’s algorithm for parity games can be used to solve fixpoint equations of arbitrary set-functions. These results find application in solving generalized parity games as well as model checking and satisfiability checking for extensions of the mu-calculus (e.g. graded, probabilistic or alternating-time), and prospectively in the computation of fair bisimulations, synthesis for linear time logics and type checking for inductive-coinductive types. The main message of all this is that many results and algorithms for solving parity games naturally generalize to solving general fixpoint equations, pointing to a close relation between the two problems. |
| 22-Oct | Henning Urbat, Automata Learning: An Algebraic Approach [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/urbat-slides.pdf” ] | We propose a generic categorical framework for learning unknown formal languages of various types (e.g. finite or infinite words, trees, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of an automata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of automaton, which is achieved via a generalized version of Angluin’s L* algorithm. The algorithm is phrased in terms of categorically described extension steps; we provide for a generic termination and complexity analysis based on a dedicated notion of finiteness. Our framework applies to structures like tree languages or omega-regular languages that were not within the scope of existing categorical accounts of automata learning. In addition, it yields new generic learning algorithms for several types of languages for which no such algorithms were previously known at all, including sorted languages, nominal languages with name binding, and cost functions. |
| 15-Oct | Frederik Völkel, Coq Formalization of LOOP and WHILE Languages [pdf-embedder url=”/wp-content/uploads/media/ws19/ober/voelkel-slides.pdf” ] | In this thesis, we present a formalization of an extended version of the LOOP language in Coq. The language supports syntactic sugar for arithmetic operations and macro calls restricted to the use of no recursion. We provide semantics in the form of an evaluation function and give a proof that this language computes the primitive recursive functions such as normal LOOP does |