Vorträge im SS 2014

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in Raum 11.150-113 in der Martensstr. 3 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 SS 2014

—

Bisherige Vorträge


Date	Speaker, Topic	Abstract
8-Jul	Peter Jipsen, Searching for evidence or failure of the amalgamation property	The amalgamation property holds in a class of structures K if for all A,B,C in K such that A is embedded in B and in C, there exists a D in K such that B, C embed in D. We describe how standard first-order automated theorem provers and model finders can be used to investigate the amalgamation property (AP) for many varieties of algebras. This method gives automated proofs of known results such as the failure of the AP for semigroups, monoids and rings, as well as the failure of the strong AP for distributive lattices. Applying the same method to distributive residuated lattices and distributive l-monoids shows that AP fails there, as well as for varieties of idempotent semirings and various other related classes.
1-Jul	Drew Moshier, String diagrams for categories of posets	String diagrams, e.g., for braiding and symmetric monoidal categories, have proven useful in Physics and Theoretical Computer Science, thanks to coherence theorems that tell us that diagrams equivalent under suitable topological invariants denote equal morphisms. In this talk, we extend a similar courtesy to categories of partially ordered sets by adding an order on diagrams and allowing for topologically “lossy” diagram rewrites. As an application, we characterize the objects in such categories that behave as semi-lattices, lattices and distributive lattices.
24-Jun	Daniel Hausmann, From depth-1 to flat coalgebraic fixed point logics , [pdf-embedder url=”/wp-content/uploads/media/ss14/ober/hausmann.pdf” ]	The extension of basic coalgebraic modal logics by depth-1 and by flat fixed point operators leads to two different variants of fixed point logics, respectively. Deciding the satisfaction problem of the former is slightly less intricate than deciding the same problem for the latter: Least fixed points (referred to as eventualities) are not necessarily recreated after each modal step in flat fixed point logics so that ensuring the actual satisfaction of an eventuality falls apart into ensuring the eventual satisfaction of its potentially procrastrinating fragments, so-called deferrals. To this end, we will consider a global caching algorithm which makes use of a variant of the concept of focussing [1] in order to detect infinitely deferring eventualities. It is then possible to construct a model – that is, a coherent coalgebra in which all deferralls are eventually satisfied – from the information gathered by a successful run of the algorithm, thus effectively deciding the satisfiability problem of flat (and depth-1) fixed point logics. The obtained model is small in the sense that it is a coalgebra over the ordinary Fisher-Ladner closure of the considered formula. We will also consider some observations towards an (efficient) implementation of said algorithm and take first steps towards possibly extending the presented methods to the alternation-free fragment of the mu-calculus. [1] K. Brünnler, M. Lange: Cut-free sequent systems for temporal logic.
17-Jun	Christoph Rauch, Generic Programming with Generic Effects via Effect Handling, [pdf-embedder url=”/wp-content/uploads/media/ss14/ober/christoph.pdf” ]	Effect handling is a novel paradigm in programming that complements the established algebraic approach to programming with effects. Intuitively, algebraic effects are those which distribute over sequential composition and hence can affect the control flow only in a quite conservative fashion. Effect handling, by contrast, allows for expressing more powerful constructions, the most basic example being exception handling. We develop novel semantic foundations for effect handling in the presence of iteration, based on cofree extensions of monads. In the larger perspective we view our current work as a prerequisite for designing a generic relatively complete Hoare calculus from programs with algebraic effects, iteration and handling. In this talk, I will give an overview of the current work in progress, including work on a folklore theorem and operational semantics.
4-Jun	Ulrich Dorsch, Succinctness Results for some Extensions of Multimodal Logic over K and S5, [pdf-embedder url=”/wp-content/uploads/media/ss14/ober/ulrich.pdf” ]	One possibility for the comparison of logics is their succinctness: For a fixed set of properties, the shorter formulas in a logic expressing these properties can be, the more succinct the logic is. In [1] T. French et al. presented several succinctness results using games to find formulas of minimum size separating large sets of models. In my M.Sc. thesis, I improve these results using similar but more compact methods (see [2]) to find shortest modal descriptions. In this talk I will describe these methods and show the results for some extensions of multimodal logic over K and S5. [1] T. French et al. On the succinctness of some modal logics. http://cgi.csc.liv.ac.uk/~wiebe/pubs/Documents/ARTINT2699.pdf [2] S. Figueira, D. GorÃn. On the size of shortest modal description. http://www8.cs.fau.de/~gorin/papers/aiml10.pdf
27-May	Hiroki Takamura, Formal Methods in Atelier Inc. and international standarization efforts in the context of the DEOS project	The talk will consist of two parts, each lasting roughly half an hour. In the first part, I want to introduce the company Atelier Inc. I am presently employed by, with an emphasis on its use of Formal Methods. Atelier (Advanced TEchnology Laboratory for Information Engineering Research) is a new company that was established in 2013. Its main business activities are: 1. Consultation for Functional Safety: ISO 26262, IEC 61508 2. Automotive ECU Software Development 3. Service Robot Software Development 4. Establishing and research of International standards: esp. IEC 62853 5. Establishing and verification of Software development process 6. Software independent certification services. Here I will focus in particular on the use of FM for Automotive EUC and our tool (under development) for automatic translation from SysML to B-methods. In the second part, I would like to report on the DEOS project ( Dependability Engineering for Open Systems, http://www.jst.go.jp/crest/crest-os/osddeos/index-e.html), which was one of the JST (Japan Science and Technology Agency) CREST projects for Dependability Engineering. Its first phase has been completed on March 2014 and focused on dependability for ever-changing systems. The project now moves to the second stage concerning practical applications. I would like to discuss the project in a broader context of international standardization activities.
26-May	John Baez, Network Theory, [ slides ]	We are entering the Anthropocene, a new geological epoch in which the biosphere is strongly affected by human activities. So, we can expect the science of this century to draw inspiration from biology, ecology and the environmental problems that confront us. What can category theorists, of all people, have to say about this? Researchers in many fields draw diagrams of networks: flow charts, Petri nets, Bayesian networks, electrical circuit diagrams, signal-flow graphs, Feynman diagrams and the like. In principle these diagrams fit into a common framework: category theory. But we are still far from a unified theory of networks. We give an overview of the theory as it stands now, with an emphasis on topics for future research, some involving higher categories.
20-May	Krystina Stawikowska, Folded Hasse diagrams of combined traces	Combined traces are intrinsic mathematical model for studying concurrent systems behaviors. They can be used to describe and investigate processes of elementary net systems with inhibitor arcs and allow to describe weak causality and simultaneity of actions. I will present work of L.Mikulski nad M. Kounty: the definition of folded Hasse diagrams of comtraces which generalise Hasse diagrams defined for partial orders and traces. I will present also their efficient on-line algorithm for deriving Hasse diagrams from language theoretic representations of comtraces.
13-May	Tobias Polzer, Formal verification of contracts for synchronous software components using NuSMV, [pdf-embedder url=”/wp-content/uploads/media/ss14/ober/tobias.pdf” ]	The GALS Transformation Language (GTL) is a tool that was created as a means to approach formal verification of large asynchronous systems of synchronous components. To facilitate global verification, synchronous components are abstracted by contracts, which are specified by LTL formulae, as state machines or both. To model and verify the synchronous components of the system the proprietary SCADE Suite was used, whose proof engine is an SMT-based model checker. In my B.Sc. thesis project I am adding support for the free NuSMV language. And I will evaluate its suitability / performance for modelling and verification of synchronous components. NuSMV can do bounded model checking as well as symbolic model checking on binary decision diagrams.
6-May	Thorsten Wißmann, COOL – The Coalgebraic Ontology Logic Reasoner, [pdf-embedder url=”/wp-content/uploads/media/ss14/ober/thorsten.pdf” ]	COOL is a generic reasoner for modal and hybrid logics satisfiability checking. It already handles logics like multimodal K (known as ALC), graded modal logic (known als ALCQ), and coalition logic and still is being extended. After presenting shortly how the implementation of logics work, I will give a tour through its features, by showing them in a live demonstration.
29-Apr	Ray Ming Chen, Introduction to Principal Component Analysis, [pdf-embedder url=”/wp-content/uploads/media/ss14/ober/ray.pdf” ]	Principal component analysis (PCA) has a very wide application, in particular in data mining, feature extraction, clustering, compression,…etc. In this talk I will introduce PCA to the general audience by giving a complete proof and showing its application. PCA is mainly used to reduce high dimensions to lower ones. In doing so, it saves a lot of resources. Of course, it doesn’t come for free. The trade-off is how to balance the benefit of resource saving and the loss of information.
15-Apr	Stefan Milius, //Generalized Eilenberg Theorem I: Local Varieties of Languages //	We investigate the duality between algebraic and coalgebraic recognition of languages to derive a generalization of the local version of Eilenberg’s theorem. This theorem states that the lattice of all boolean algebras of regular languages over an alphabet Sigma closed under derivatives is isomorphic to the lattice of all pseudovarieties of Sigma-generated monoids. By applying our method to different categories, we obtain three related results: one, due to Gehrke, Grigorieff and Pin, weakens boolean algebras to distributive lattices, one due to Polak weakens them to join-semilattices, and the last one considers vector spaces over Z₂.