Vorträge im WS 2014

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 vorläufig in Raum 06 in der Wetterkreuz 13 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 2014

—

Bisherige Vorträge

Date Speaker, Topic Abstract
24-Mar Dominik Paulus, Reasoning über unscharfe Beschreibungslogiken Fuzzy-Beschreibungslogiken sind eine Familie von Logiken, in denen statt der klassischen Wahrheitswerte (“wahr”/“falsch”) Wahrheitsgrade, üblicherweise aus dem Intervall [0,1], zur Anwendung kommen. Ich stelle verschiedene Ansätze für fuzzy-Varianten von ALC, entsprechende Tableau-basierte Reasoner sowie meine Implementierung eines Reasoners für fuzzy ALC mit Łukasiewicz-Semantik vor.
3-Mar Dexter Kozen, Completeness and Incompleteness in Nominal Kleene Algebra [pdf-embedder url=”/wp-content/uploads/media/ws14/ober/kozen.pdf” ] (joint work with Konstantinos Mamouras and Alexandra Silva)
Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra (KA) as a framework for reasoning equationally about imperative programs with statically scoped allocation and deallocation of resources. The system consists of KA augmented with a binding operator that binds a named resource within a local scope. They gave an axiomatization that captures the behavior of the scoping operator and its interaction with the KA operators and proved soundness over a class of nominal languages. I will show in this talk that the axioms are not complete for their proposed semantics, but they are sound and complete for a slight extension. If time, I will touch on recent work (with the above coauthors and Daniela Petrisan) on nominal Kleene coalgebra.
4-Feb Fatemeh Seifan, Uniform Interpolation for Coalgebraic Fixpoint Logic (Joint work with Yde Venema and Johannes Marti)
We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e.; functors with quasi-functorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.
27-Jan Ulrich Dorsch, Generic Expressions from Predicate Liftings [pdf-embedder url=”/wp-content/uploads/media/ws14/ober/dorsch.pdf” ] I will present an overview of what has been done on the COAX (Coinduction Meets Algebra for the Axiomatization of System Equivalences) project. Starting with some groundwork information on expressions, Kleene theorem and the rational fixed point, I will cover some previous work on more general Kleene theorems (for more than regular languages/det. automata). I will conclude with our work (Lutz Schröder, Stefan Milius) on bringing predicate liftings (known from coalgebraic logic) to the table in order to build a generic expression calculus.
20-Jan Miriam Polzer, Formalizing Equivalence between Monotonic Relational Expressions Since the 1970’s, decision procedures for query equivalence and containment have been a major research subject in database theory due to their relevance for query optimization. Query equivalence is undecidable for the full relational algebra, but one can restrict the set of operations to achieve decidability. In this talk, I will present my ongoing work on Coq formalization of equivalence and containment results obtained by Sagiv and Yannakakis [1]. Their approach had two specific features: first, while most of the standard references and monographs in presenting positive results focus on so-called conjunctive queries, Sagiv and Yannakakis allowed the presence of union. Second, they made so-called universal relation assumption, fashionable in early period of database theory and recently enjoying a modest renaissance for rather surprising reasons, allowing more provable equivalences at the expense of additional design constraints on database instances under consideration. The foundation of our formalization is a recent ESOP paper [2], which included formalization of equivalence for simple conjunctive queries.

[1] Y Sagiv, M Yannakakis. Equivalence Among Relational Expressions with the Union and Difference Operators.
[2] V Benzaken, Ã Contejean, S Dumbrava. A Coq Formalization of the Relational Data Model.
13-Jan Daniel Hausmann, From the flat to the alternation free coalgebraic mu-calculus [pdf-embedder url=”/wp-content/uploads/media/ws14/ober/hausmann.pdf” ] The extension of basic coalgebraic modal logic by fixed point operators leads to the so-called coalgebraic mu-calculus [1], generalizing the well-known (propositional) mu-caculus. We have previously considered the satisfiability problem of the flat (i.e. single variable) fragment of the coalgebraic mu-calculus. In order to decide this problem, we introduced a global caching algorithm (generalizing ideas from [2] and [3]) which employs a non-trivial process of so-called propagation, keeping track of least fixed point literals (referred to as eventualities) in order to ensure their eventual satisfaction. As our algorithm operates over subsets of the ordinary Fischer-Ladner closure of the target formula, the model construction in the accompanying completeness proof yields filtered models of size at most 2n where n denotes the size of the satisfiable target formula – in particular improving upon previously known lower bounds on model size for CTL (n*2n) and ATL (2O(n*log n)).
Subsequently, we are ready to extend our attention to the alternation free fragment of the coalgebraic mu-calculus; we obtain an adjusted version of our algorithm that decides the according satisfiability problem and the completeness proof again encompasses the construction of filtered models – for satisfiable formulas of the alternation free (coalgebraic) mu-calculus.[1] C. Cirstea, C. Kupke, and D. Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus.
[2] M. Lange, C. Stirling. Focus games for satisfiability and completeness of temporal logic.
[3] R. Goré, C. Kupke, D. Pattinson, L. Schröder. Global Caching for Coalgebraic Description Logics.
16-Dec Tadeusz Litak, Idioms, Arrows and Modal Logic Every now and then, programmers find themselves dealing with an abstract notion of computation whose structure comes somewhat close to being a strong monad — but for some reason, one should not or cannot require the “multiplication” or “bind” law in its full power. This may happen, e.g., when dealing with composition of two monads… or with guarded (co-)recursion… or with stream processors… or even when designing an efficient parser. More precisely, as analyzed by Lindley, Wadler and Yallop, monads are really necessary when results of previously executed operations may influence not only a) values passed to subsequent operations but even b) the choice what operations to run next. When postulate b) is dropped, one can use the “arrow” interface proposed by John Hughes. When both a) and b) can be dropped, one gets to meet “idioms” or “applicative functors” of McBride and Paterson. “Arrows” are binary, implication-like type constructors, whereas “applicative functors”, as the name indicates, are more familiar-looking beasts. Lindley, Wadler and Yallop (2008) proposed “arrow calculus” with an explicit goal to provide a generalization of Moggi’s computational metalanguage for arrows; curiously enough, I am not aware of an analogous work for much simpler-looking idioms.

In this talk, I am going to show that once again modal logic provides a nice set of glasses to stare at the problem. Arrows, in particular, turn out to be an instance of the oldest conceivable modal setup in modern formal logic, older than the box itself. We happened to reinvent them recently with Albert Visser when working on uniform interpolation for strong Loeb calculi and this is how I came to be interested in this material. More importantly, modal proof theory provides us with a ready-made computational metalanguage for idioms, where one can derive all the laws of McBride and Paterson in exactly the same way as Lindley et al. derived Hughes’ arrow laws in their calculus.
09-Dec Sergey Goncharov, Coalgebraic Weak Bisimulation from Recursive Equations over Monads [pdf-embedder url=”/wp-content/uploads/media/ws14/ober/goncharov.pdf” ] Strong bisimulation (equivalence) for labelled transition systems is one of the most fundamental concepts in process algebra, and has been generalised to numerous classes of systems that exhibit richer transition behaviour. Nearly all of the ensuing notions are instances of the more general notion of coalgebraic bisimulation. Weak (bisimulation) equivalences, however, have so far been much less amenable to a coalgebraic treatment. Here we attempt to close this gap by giving a coalgebraic treatment of (parametrized) weak equivalences. Our analysis requires that the functor defining the transition type of the system is based on a suitable monad supporting a fix-point operator, which allows us to capture weak equivalences by least fixpoints of recursive equations. Our notion is in agreement with existing notions of weak bisimulations for labelled transition systems, probabilistic and weighted systems, and simple Segala systems.
02-Dec Christoph Rauch, //(Co)algebraic Foundations for Recursive Handling of Effects // [pdf-embedder url=”/wp-content/uploads/media/ws14/ober/christoph.pdf” ] Large portions of current programming theory and practice are based on monadic notions of effect. The monadic approach has been recently complemented by the paradigm of effect handling as embodied in the eff programming language. We develop novel semantic foundations for effect handling in the presence of iteration, based on cofree extensions of monads, which are characterized by a universal property. In this talk, I explain how effect handling is implemented in terms of certain monad morphisms between Elgot monads (characterized by having parametrized uniform iteration operators in the sense of Simpson and Plotkin), show how we can express iteration and recursion through handling and briefly compare our framework to related work.
25-Nov Maryam Sanati, SMT-based Verification of SCADE models Errors in safety-critical systems may have dramatic consequences involving human lives and huge costs. The synchronous approach helps the development of the safety-critical systems. SCADE modeling language belongs to synchronous language family. It is a data flow language that supports both textual and graphical programming. It is a mixture of LUSTRE language and safe state machines. The correctness of the SCADE models can be checked with an SMT-based verification engine. To bridge the gap between the complex concepts of SCADE language and the encoding as a set of formulas that can be delivered to an SMT-solver an intermediate language, LAMA, was developed. In this verification method, the complex SCADE models are translated to LAMA and the LAMA program will be transformed to SMT instances [1]

[1] Basold, Henning, et al. “An Open Alternative for SMT-Based Verification of Scade Models.” Formal Methods for Industrial Critical Systems. Springer International Publishing, 2014. 124-139.
18-Nov Stefan Milius, Uniform Eilenberg Theorem: Syntactic Algebras For Free This talk continues on the topics that I presented in my previous seminar presentation. We investigate the duality between algebraic and coalgebraic recognition of languages to derive a generalization of Eilenberg’s theorem. The classical Eilenberg theorem states that the lattice of all boolean algebras of regular languages closed under derivatives and preimages of homomorphisms is isomorphic to the lattice of all pseudovarieties monoids. By applying our method to different categories, we obtain several previously known Eilenberg-type theorems as special instances: one due to Pin weakens boolean algebras to distributive lattices, a result by Polák concerning join-semilattices and one by Reutenauer on vector space algebras. We are also able to give a uniform account of the syntactic algebra, i.e. the canonical algebraic acceptor of a given regular language, as dual to the minimal machine accepting that language. And we also have uniform proofs for local versions of Eilenberg-type theorems, e.g. one due to Gehrke, Grigorieff and Pin for distributive lattices. The two corresponding results for join-semilattices and vector space algebras are new.
3-Nov Andreas Doering, Contexts, Bi-Heyting Algebras and a New Logic for Quantum Systems [pdf-embedder url=”/wp-content/uploads/media/ws14/ober/doering.pdf” ] Traditional Birkhoff-von Neumann quantum logic is based on the orthomodular lattice of projections on a Hilbert space. As a logical system, this is a rather poor structure. In recent years, a new and much better-behaved logic for quantum systems has been developed by Isham, me, and others as a part of the topos approach to quantum theory. This approach connects noncommutative operator algebras with topos theory and naturally leads to complete Heyting algebras of propositions about the quantum world. If the algebra of observables is a von Neumann algebra, one even obtains a complete bi-Heyting algebra. In this talk, I will introduce the necessary background and present the main constructions and results.
27-Oct Ulrich Rabenstein, Ontology-supported classification of ad hoc disclosures The publication of ad hoc disclosures significantly influences stock value. We will discuss a tool for the classification of ad hoc disclosures according to their content. It is based on natural language processing and supported by ontologies. This can be used to examine the relation between the effect on the stock value and the content of the disclosure.
21-Oct Dmitry Traytel, Formalized Decision Procedures within the Logic-Automaton Connection Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (e.g. automata). This talk presents two decision procedures for MSO formulas that were formalized in Isabelle. The first one is not based on automata but on regular expressions. Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. Inspired by Brzozowski derivatives, we devise a notion of derivatives that operate directly on formulas. Using formula derivatives, we obtain a second decision procedure for MSO that does not require a translation of the input formula into automata.
14-Oct Thorsten Wißmann, The rational fixed point in nominal sets and its application to infinitary lambda-calculus [pdf-embedder url=”/wp-content/uploads/media/ws14/project-wissmann-talk.pdf” ] We start recalling nominal sets — an approach to deal with binding signatures such as the λ-calculus modulo α-equivalence. We will discuss many properties of nominal sets, especially of orbit-finites, the finitely presentable objects in the category of nominal sets. With that we will describe the rational fixed point in nominal sets; at first generally as the subcoalgebra of the final coalgebra induced by orbit-finite coalgebras. Secondly, we will see that the rational fixed point of the endofunctor corresponding to the binding signature of λ-calculus precisely contains the rational λ-trees modulo α-equivalence — possibly infinite λ-terms with only finitely many subtrees. Here, we obtain a corecursion principle, with which we are able to define substitution on rational λ-trees as a total function.
7-Oct Hans-Peter Deifel, Using subtyping to program with fixpoint datatypes We introduce a small functional programming language with a type system that allows to restrict algebraic data types to a subset of their constructors. This concept makes it possible for functions to be defined on types such as “List consisting only of Cons constructors” or “Expression without division”. The type system also incorporates an intuitive subtype relation on such constrained types and a special typing rule for case expressions that admits function types like “given an object of a subtype of T”, return an object of the same type” written ‘a -> a where a <: T’. This feature can naturally be applied to recursive data types and can also be extended to facilitate the usage of both inductive and coinductive types in the same language. In addition, we show the implementation of a type checking algorithm for the language of this presentation based on constraint generation and type simplification.