Vorträge im SS 2017 - Lehrstuhl für theoretische Informatik 8

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 SS 2017

—

Bisherige Vorträge


Date	Speaker, Topic	Abstract
18-July	Kristin Braun, Elimination of Nominals in Coalgebraic Description Logics [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/braun-talk.pdf” ]	Nominals in coalgebraic modal logics can be seen as names for worlds in a model M. Reasoners are often overhelmed when solving modal formulas with nominals. In this talk a translation from hybrid to non-hybrid formulas (presented last year by Johannes Kern) will be benchmarked and optimized. The talk will be given in German.
18-July	Frederik Haselmeyer, Inclusion Checking for Nominal Automata with Name Binding [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/haselmeyer-talk.pdf” ]	Nominal sets have been used for a wide variety of applications in computer science. Recently, they have been adapted to be used in automata theory to capture a notion of global and local freshness. The inclusion problem of local freshness has been solved by Schröder et all using regular nondeterministic nominal automata (RNNAs) generated from regular bar expressions. I will give an introduction to the theory and provide a concrete implementation of said inclusion algorithm. I will then demonstrate a tool that I developed, that uses this inclusion algorithm and show inclusions for a few select languages.
11-July	Armin Helmberg, One-Step Algebras — Bounded Proofs and Step Frames [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/helmberg-talk.pdf” ]	In this talk, we will discuss one-step algebras as introduced by Nick Bezhanishvili and Vilvio Ghilardi. One-step algebras originate in one-step frames, which we use to show properties of axiomatic systems that are adequate to a logic. To that end we will define the bounded proof property as well as the finite model property.
4-July	Fatemeh Seifan, Bisimulation quantifiers for modal logic [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/fatemeh-slides.pdf” ]	Bisimulation quantifiers were first introduced by Pitts for propositional intuitionistic logic, and then studied in different contexts, mainly as a tool for proving strong forms of interpolation (such as uniform interpolation). In this talk , as it is announced in the title, we will discuss bisimulation quantifiers in the context of modal logic. In particular we discuss the interaction between modal operators and bisimulation quantifiers and the relation between closure under bisimulation quantifiers and uniform interpolation.
27-June	Sergey Goncharov, Guarded monoidal traces, Hoare logic and the Grothendieck construction [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/goncharov-slides.pdf” ]	I present a snapshot of recent developments devoted to the study of a generic notion of guardedness and its connection to solutions of fixpoint program equations, capitalizing on recent work [1]. The main motivation stems from process algebra where systems of guarded processes under strong bisimilarity admit unique solutions–a well known fact dating back to Milner. Nevertheless, guarded processes under infinite trace equivalence need not have unique solutions. This and further examples can be captured by a generic notion of guarded co-Cartesian category, essentially axiomatized in [1]. Here I present a novel equivalent axiomatization, straightforwardly giving rise to a generalization to symmetric monoidal categories, and thus leading to a notion of guarded traced monoidal category with an inherent coherence theorem a la Selinger. In the specific case of a Kleisi category of a monad the axioms of co-Cartesian categories bear a resemblance to the axioms of Hoare logic, where guardedness assertions are used in place of partial correctness assertions. I provide an attempt to formalize this resemblance by identifying suitable fibrations over Kleisli categories drawing on the Grothendieck construction. [1] Sergey Goncharov, Lutz Schröder, Christoph Rauch, Maciej Pirog, Unifying Guarded and Unguarded Iteration, In Proc. Foundations of Software Science and Computation Structures (FoSSaCS)
20-June	Tadeusz Litak, The Subkripkean, the Subcanonical’ and the Completeness Hypercuboid	I am going to overview mutual relations between notions of strong completeness, canonicity and closure under various form of completions, and propose a way of classifying them. Especially in the modal context, numerous examples illustrating these concepts are not equivalent have been produced since the 1970’s. Outside of a relatively narrow group of experts, awareness of these issues in both algebraic and coalgebraic community seems rather poor. Yet, these distinctions are likely to play an important role in the development of: the theory of coalgebraic logics beyond shallow axioms, algebraic proof theory and so-called possibility semantics, currently a subject of intensive investigations. Besides, given the essentially non-constructive character of canonical extensions, it is important to note that results much more general than failure of canonicity can be shown in a simpler manner. Finally, as proofs that these notions are distinct involve natural logics of independent interest, it appears that each of these strong completeness notions deserves attention in its own right.
13-June	Christoph Rauch, A Generic Metalanguage for Guarded and Unguarded Iteration [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/rauch.pdf” ]	The notion of guardedness is widespread in the world of iterated computation. It usually means that productivity is maintained throughout the computation by wrapping recursive calls into certain operations considered as guarding operations. We recently designed a set of rules to abstractly specify guardedness of programs in a monad T, i.e. what it means for a morphism X â†’ TY to be guarded with respect to a summand of Y. A monad with a guardedness concept adhering to these rules is called guarded iterative, subsuming the notions of iterative monads and Elgot monads. I present an extension of this calculus providing support for contexts and multiple variables by means of strong monads and product types and a corresponding computational metalanguage enabling the use of guarded iteration, where complex guardedness judgements are built up from a basic set of basic guarded programs.
30-May	Kristof Teichel, Design and Analysis of Cryptographically Secured Time Synchronization Methods – Third Report on the NTS Project	The Network Time Security (NTS) project seeks to develop a collection of mechanisms for cryptographically secured time synchronization message exchanges over packet-based networks. When such measures are employed, the reliability of the clock synchronization clearly depends on the cryptographic measures. Furthermore, cryptographic measures always, to a certain degree, depend on synchronous time. This creates some interesting dependencies between timing and security, which cause challenges in both the design of standard documents and the formal analysis (especially with automated tools) of developed protocols. This presentation continues and updates last year’s presentation on the NTS-related work, provides an introduction to the relevant topics and reports on the current progress of the project. Specifically, it reports on the status of the specification design and the drastic changes since last year, and also on the standardization work that is associated with the development of the NTS documents. The presentation also provides insight on the formal analysis of specification and protocol parts, in particular on a UPPAAL analysis of timing aspects in broadcast mode that was published last year, and on the work that is currently being carried out with the theorem Prover Isabelle.
23-May	Merlin Göttlinger, Dynamic state-space exploration on generated application-specific OSEK kernels	dOSEK is an implementation of the OSEK standard for real-time operating systems that generates specialized kernel instances for each application. I will give a high-level overview of the architecture of dOSEK and describe my method to dynamically extract the complete application specific state-space of a single generated kernel as a deterministic labeled transition system. Additionally, I will show how to check the resulting graph against a statically pre-computed OS-application interaction graph and explain why graph isomorphism is both useful and feasible for this task.
16-May	Hans-Peter Deifel, Verifying Operating Systems against the OSEK Specification with Temporal Logic	The OSEK industrial standard governs the design of embedded real-time operating systems in the automotive domain. I will give a quick introduction into this standard and explain how we turn an OS-application interaction graph that is generated during the compilation phase of the operating system into a Kripke frame so that we can verify that its behaviour conforms to the specification using temporal logic. I will also highlight the pitfalls and problems when generating NuSMV specifications.
16-May	Daniel Hausmann, Determinizing Eventually Deterministic automata [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/hausmann.pdf” ]	We introduce a natural notion of eventually deterministic automata, along with a method that determinizes eventually deterministic Büchi automata to deterministic parity automata of size O((n+2)!) with O(n) priorities. As a corollary, eventually deterministic parity automata of size n with k priorities can be determinized to deterministic parity automata of size O((nk+2)!) and with O(nk) priorities. The new construction relies on eventual determinism to avoid the full complexity of the Safra/Piterman-construction by using partial permutations of states in place of Safra-Trees. Eventually deterministic automata can be used to recognize unsuccessful branches in pre-tableaux for the aconjunctive Âµ-calculus. Using the new determinization method, we thus obtain so-called permutation games, that is, satisfiability games for the aconjunctive Âµ-calculus that are of size O((nk+2)!) and have O(nk) priorities.
09-May	Thorsten Wißmann, An Efficient Coalgebraic Paige Tarjan Algorithm [pdf-embedder url=”/wp-content/uploads/media/ss17/ober/thorsten-coalgpt.pdf” ]	I will present an algorithm for computing behavioural equivalence in a coalgebra for a functor H on three levels: 1) on the general level of a regular category, the algorithm computes two refining sequences of partitions, which identify equivalent behaviours on termination. 2) in (sorted) sets for so-called zippable functors H, we can optimize the algorithm by computing the sequences incrementally. 3) if the functor H admits a so-called refinement interface, we can implement the incremental computation in pseudocode such that the overall complexity of the algorithm is in O((m+n) log n). Here n is the number of states and m is the number of edges, which are provided by the interface of H. This generic algorithm instantiates to many partition refinement algorithms allowing the same complexity, e.g. for transition systems (Powerset functor P), with labels (P(LÃ—-)), weighted systems allowing negative weights (monoid-valued functor), deterministic automata with the same complexity as Hopcroft’s algorithm. The instantiation to generic (as well as simple) Segala systems lives in 2-sorted sets and improves the known complexity to O((m+n) log (m+n)).