Oberseminar Vorträge im WS 2012

Vorträge im WS 2012/13

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet Dienstags von 14:00-16:00 in Raum Übung 3/01.252-128 in der Cauerstr. 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 (lutz.schroeder@informatik.uni-erlangen.de).

Date Speaker Topic Abstract
5 Feb Facundo Cerreiro An automata-theoretic view on logics and vice-versa Automata theoretic tools for modal and classical logics have proved to be very useful. For example, they were used by Rabin to prove the decidability of MSO over trees, and by others to give complexity bounds for logics such as PDL. Moreover, Janin and Walukiewicz used automata-theoretic characterizations to prove that the modal mu-calculus is the bisimulation invariant fragment of monadic second order logic. In this talk I will give an introduction to this area and, time permitting, I will explain how to prove the Janin-Walukiewicz theorem and connections to coalgebraic (fixpoint) logics.
29 Jan Volker Strehl Let me count the ways …. or Complex Analysis meets Complexity Analysis (part 2) In the second part of this talk I will discuss in particular aspects of the enumeration of trees by dealing with instances of the following problems: — What is the average-case complexity of typical term rewrite algorithms? How can the speedup due to sharing of subtrees be quantified? — Height and pathlength are important parameters of trees. What can be said about their average-case behaviour and how are they related? — Balancing is a severe restriction on the shape of trees. How does it affect the counting generating functions?
22 Jan Rolf Hennicker Component Interfaces with Contracts on Ports We show how the abstract concept of an interface theory introduced by De Alfaro and Henzinger can be extended to an abstract theory for component interfaces with ports. The resulting component framework satisfies itself the general laws of an interface theory concerning compositionality of refinement and interaction compatibility. The ports of a component interface represent the interaction points of a component. Each port is equipped with a contract specifying the assumptions on and the guarantees for the environment of a component. As a particular instance we consider modal component interfaces since the modal approach – in the sense of Larsen and Thomsen – is particularly useful to specify loose environment assumption. In this context component behaviors and the assume and guarantee behaviors of ports are given in terms of modal I/O-transition systems with weak modal refinement and with a weak modal compatibility notion.
8 Jan Baltasar Trancón y Widemann Pointer Coalgebra – Mathematics of Low-Level (Functional) Programming The heap space of a running program assigns to every live cell address its content, which may contain one or more pointers to other addresses. Thus a heap space state is naturally a coalgebra, with the working set as its carrier and dereferencing as its operation. The use of standard coalgebraic machinery is explored in this context in three ways: 1.) Referential transparency of heap manipulations can be phrased in terms of subcoalgebra inequations. 2.) The notions of behavioural equivalence and rational fixpoints give rise to an elegant coalgebraic data model for functional programming on top of arbitrary, cyclic pointer structures. 3.) The associated universal morphisms encode an effective pattern for recursive functions on cyclic data.
18 Dec Volker Strehl Let me count the ways …. or Complex Analysis meets Complexity Analysis This will be a talk of tutorial character in which I will show how tools of complex analysis can be made instrumental for solving counting problems (sometimes exactly, mostly asymptotically), and how this methodology can be used for the average-case analysis of data structures and algorithms. Since trees of various kind are familiar objects for every computer scientist I will mostly concentrate on these objects.
11 Dec Tadeusz Litak Coalgebraic Predicate Logic We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. This includes such diverse structures as Kripke frames, neighbourhood frames, topological spaces, discrete Markov chains, conditional frames, multigraphs or game frames for coaliton/alternating time logics. We discuss axiomatization and completeness results for two natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, contrasting it with both coalgebraic modal logic and existing first-order proposals for special classes of Set-coalgebras (apart for relational structures, also neighbourhood frames and topological spaces). The semantic characterization of expressivity is based on the fact that our language inherits a coalgebraic variant of the Van Benthem-Rosen Theorem. Basic model-theoretic constructions and results, in particular ultraproducts, obtain for the two classes which allow completeness—and in some cases beyond that. We also provide some early results on cut-free sequent systems. I will also discuss the relationship with alternative formalisms, for example those based on coalgebraic hybrid/description logics.
4 Dec Christoph Rauch Monads and the Curry-Howard Isomorphism Modern functional programming languages make heavy use of monads, a concept derived from Category Theory and proposed as a means to model effectful computations by Eugenio Moggi in the early 90s. The Curry-Howard isomorphism provides a way to look at computational calculi from a logical point of view. I will describe the connection between Moggi’s monadic lambda calculus and modal logic, starting by looking at Intuitionistic Propositional Logic through the lens of the Curry-Howard isomorphism and enriching the resulting lambda calculus with a monadic operation. The updated calculus is then translated back, which yields an intuitionistic modal logic providing a motivation for the types of monad unit and multiplication. Similarly, I will describe how, following an idea by Conor McBride, monads over indexed datatypes are related to Hoare Triples.
27 Nov Manuel Schmitt Particle Swarm Optimization Particle swarm optimization (PSO) is a popular meta-heuristic for solving black-box optimization problems on a continuous domain, inspired by swarm behaviour occurring in nature. Its advantages are that it can be implemented very easily and that experiments show good results after comparably small time. Although this technique is widely used, up to now only some partial aspects of the method have been formally investigated. An analysis on how to choose the parameters of the algorithm in order to guarantee convergence to one point in the search space will be presented. Afterwards, the capability of the swarm to find a local optimum for a very general class of functions will be shown.
20 Nov Daniel Hausmann Flat coalgebraic fixed point logics The framework of coalgebraic logic allows for the uniform definition of wide ranges of logics. The (efficient) decision of the satisfiability / provability problem is of particular interest in this context. Various generic algorithms have been recently proposed to this end; in pratice, algorithms which employ the technique of global caching have proven to be particularly efficient. As a first contribution, we propose an improvement of the propagation part of global caching algorithms, replacing the computation of the greatest fixed point of so-called proof transitionals by a series of least fixed point computations. Subsequently we introduce (flat) fixed point operators to coalgebraic logics and present a correct global caching algorithm for the obtained flat coalgebraic fixed point logics. This algorithm is built upon a set of so-called focusing sequent rules and makes use of a more intricate instance of the above-mentioned adapted propagation. As a byproduct of the proof of the correctness of this algorithm, we obtain a new small model lemma which improves upon previously known results.
13 Nov Thorsten Wißmann Consistency Checking of Description Logics with I and me There are many description logics, each with different expressiveness. At first the basic description logics ALC, ALCHIQ and its extension with bounded self-reference ALCQme2 are introduced. Then some reasoning tasks for consistency checking of ontologies are shown. Finally a reduction of consistency checking of ontologies with ALCQme2 formulas to the corresponding problem for OWL ontologies (which is already solved by many different reasoning programs) is explained.
6 Nov Mihai Codescu Integrating VSE’s Refinement in Hets In this talk we present the Heterogeneous Tool Set (HETS), a tool for parsing, static-analysis and proof management for heterogenous multi-logic specification. Heterogeneity is achieved here in a formal way using the theory of institutions, a categorical formalization of the notion of logical system. As an example, we describe the integration of the refinement method of the Verification Support Environment VSE into Hets. The interesting aspect is that this is realized by encoding VSE’s refinement as an institution comorphism, and thus the logic-independent machinery of Hets can be employed as such, without introducing a new dedicated concept to support it.
30 Oct Sergey Goncharov A Relatively Complete Hoare Logic for Order-Enriched Effects We continue exploration of the Hoare logic for order-enriched effects. In particular, we present a relative completeness result based on the classical idea of weakest preconditions. The completeness theorem amounted to non-trivial conditions about definability of weakest preconditions and their properties. We present an initial study of these conditions and outline some future work and challenges related to applicability of our developments to important partial cases such as probabilistic computations, local stores, etc.