Vorträge im SS 2015

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15–15:45 in Raum 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 (mailto:lutz.schroeder@informatik.uni-erlangen.de).

Voraussichtlicher Plan für SS 2015

—

Bisherige Vorträge


Date	Speaker, Topic	Abstract
14-Jul	Daniel Hausmann, //Deciding coalgebraic fixpoint formulas early //	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-calculus. We consider the satisfiability problem of its alternation-free fragment and introduce an optimal, single-pass, global caching algorithm (generalizing ideas from [2] and [3]) which decides the problem by employing 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. Our algorithm operates over subsets of the ordinary Fischer-Ladner closure of the target formula, however, the model construction in the accompanying completeness proof yields so-called focussed models of size at most n(4ⁿ) where n denotes the size of the satisfiable target formula – in particular improving upon previously known lower bounds on model size for e.g. ATL and the alternation-free mu-calculus (both 2^{O(nlog n)}). In this talk, we are going to revisit the model construction that lies at the heart of the justification of the presented algorithm. Regarding a possible implementation of the algorithm as part of the Coalgebraic Ontology Logic Reasoner (COOL, [4]), we are also going to contrast the expected runtime behaviour of the introduced algorithm with the runtime behaviours of previous (multi-pass and single-pass) algorithms. [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. [4] D. Gorin, D. Pattinson, L. Schröder, F. Widmann and T. Wißmann. Check out COOL – The Coalgebraic Ontology Logic Reasoner.
7-Jul	Markus Schöngart, Towards a Practical Specification Language for Lightweight Software Verification	Acquiring sound evidence of the behavior of developed software remains difficult in practice. Although formal verification methods are able to establish absolute certainty of particular properties and continue to improve on their applicability and usability, there are still barriers that prevent formal methods to be employed or the facts established by them to be trusted in practice. Regarded among those barriers are the (sometimes manual) modeling of the program in the verification method’s terms (which may fail to be faithful), the specification of the desired properties (which may be formalized wrongly without getting noticed) as well as interpreting a verification tool’s output. Our approach is to design a specification language which is not tightly coupled to a verification method, tries to stay close to terms a programmer might be used to reason about informally and facilitates lightweight verification. Subsequently, we intend to search for a rule set that maps patterns in programs and specifications to applicable verification methods. Since a useful theoretical characterization of the applicability of such a rule set may be infeasible, we plan to evaluate it empirically.
30-Jun	Julian Jakob, Formal Verification in the Theory of Side-effecting (Co-)Recursion	In theoretical computer science, as in mathematics, the more complicated the subject the more extensive proofs may become. It is therefore helpful to check results with the help of special software to avoid mistakes. In this talk I will give insight into my work verifying the technically quite involved proofs about “Unguarded Recursion on Coinductive Resumptions” (a publication by Sergey Goncharov, Christoph Rauch and Lutz Schröder) in the interactive theorem prover Coq. This involves working with Coq’s type classes to model categories and Elgot monads.
9-Jun	Alexandra Silva, NetKAT: A formal system for the verification of networks	NetKAT is a relatively new programming language and logic for reasoning about packet switching networks that fits well with the popular software defined networking (SDN) paradigm. NetKAT was introduced quite recently by Anderson et al. (POPL 2014) and further developed by Foster et al. (POPL 2015). The system provides general-purpose programming constructs such as parallel and sequential composition, conditional tests, and iteration, as well as special-purpose primitives for querying and modifying packet headers and encoding network topologies. The language allows the desired behavior of a network to be specified equationally. It has a formal categorical semantics and a deductive system that is sound and complete over that semantics, as well as an efficient decision procedure for the automatic verification of equationally-defined properties of networks.
2-Jun	Stefan Milius, Killing Epsilons with a Dagger: A Coalgebraic Study of Systems with Algebraic Label Structure	We propose an abstract framework for modeling state-based systems with internal behaviour as e.g. given by silent or epsilon-transitions. Our approach employs monads with a parametrized fixpoint operator to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems and non-deterministic transducers.
19-May	Sergey Goncharov, Towards a Calculus of (Un-)Guarded Corecursive Definitions	In recent decades, the theory of coalgebras has proven to provide a suitable general platform for defining and reasoning by corecursion and coinduction. Various results in automata theory, game theory, functional programming can be couched in coalgebraic terms and generic coalgebraic arguments can be applied to ensure existence and uniqueness of the defined concepts, essentially yielding the main result of the corresponding theoretical constructions. A well-established way to formulate an existence and uniqueness theorem is by using (systems of) guarded corecursive schemes, i.e. recursive equations in a certain format ensuring productivity of recursion at every iteration. The format of corecursive schemes standardly requires for a distinction between defined symbols and those being defined and allows for mixing them only in certain restricted way. Also the theory of guarded corecursive schemes can not be reused for unguarded definitions. In this work (which is heavily in progress) we propose an alternative strategy for solving guarded definition potentially scaling to the unguarded case. We propose a simple type-theoretic discipline based on computational monads, where undefined operations are treated as first-class citizens (semantically they are adjoined to any given monad to form an extended monad). We show that the standard finality argument formalized in our language implies a definitional principle for free operation (semantically this corresponds to mapping from the extended monad to the original one).
12-May	Tadeusz Litak, Whence Cometh Incompleteness?	I am going to sketch the background of my new collaboration with Wesley Holliday (UC Berkeley) and describe our recent results. It is broadly known in the narrow circle of theoretical modal logicians that while “naturally” obtained modal logics tend to be Kripke complete, things look very differently when one looks at the class of all modal logics. In the 1970’s, S.K. Thomason found a fundamental reason why this phenomenon is unavoidable: modal consequence over Kripke frames is every bit as complex as full second-order consequence. Shortly afterward, Wim Blok proved another amazing result: even those logics that are complete tend to be surrounded by uncountably many incomplete ones, which are sound wrt precisely the same class of Kripke structures. Kripke incompleteness turned out to be much more of a norm than anybody had expected before and in a very precise sense, the problem is irreparable, at least as long as the notion of proof remains decidable. A question then arises if some sensible generalization of Kripke semantics would make the phenomenon of incompleteness disappear. In a way, the answer was known even before Kripke frames dominated the picture: every modal logic is complete wrt Boolean Algebras with Operators (BAOs). As it turns out, this is really the best general completeness result we can hope for. Yes, it is possible to find naturally motivated semantics properly contained between Kripke semantics and algebraic semantics which do not suffer from the “Thomason effect”: the induced notion of consequence can be axiomatized. However, as soon as these notions nontrivially depart from the full generality of algebraic semantics and try to capture at least some of the defining properties of Kripke frames, not only one can still find examples of incomplete logics, but the limitative result of Blok still survives. These questions were investigated in my PhD dissertation a decade ago, building on several decades of work in the modal community. By the time the dissertation was completed, there was still one possible escape route left: complete additivity, one of the three defining properties of (dual algebras of) Kripke frames, could perhaps allow a general completeness result. More recently, Wesley Holliday’s work on “possibility semantics” rekindled the interest in that particular notion of completeness. Now in a joint work, Wesley and myself found out that even this escape route is blocked. Furthermore, the story turns out to involve an unjustly forgotten example, paper and program of Johan van Benthem.
5-May	Ulrich Dorsch, Generic Expressions from Predicate Liftings	I will present an overview of what has been done on the COAX (Coinduction Meets Algebra for the Axiomatization of System Equivalences) project (joint work with S. Milius, L. Schröder). A generic language of expressions has been developed together with a Kleene theorem to describe the behaviour of coalgebras for arbitrary, finitary Set-functors with semantics defined by sets of predicate liftings in a similar fashion to coalgebraic logic. I will touch on functor presentations as well as an expression language based on them [1] and give a more detailed summary of a more recent work [2] connecting relation liftings, notions of bisimularity and functor presentations for certain functors with sets of predicate liftings suitable for our expression calculus. [1] R. Myers, Rational Coalgebraic Machines in Varieties: Languages, Completeness and Automatic Proofs. PhD thesis, Imperial College London, 2013 (unpublished) [2] J. Marti, Y. Venema: Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 2015
28-Apr	Lutz Schröder, Generic Trace Semantics and Graded Monads	Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions\; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. We now refine this abstraction by introducing graded monads, which take into account a notion of depth that corresponds, for example, to trace length or bisimulation depth. We develop the basic theory of graded monads and their algebras, and in particular show how graded algebras play the role of formulas in trace logics.
21-Apr	Kristof Teichel, A Report on the Network Time Security Project and the Associated Formal Verification	The Network Time Security (NTS) specification is a collection of mechanisms for secure time synchronization message exchanges. These mechanisms may in some cases depend on timing because the protected messages directly affect the participants’ clocks. This creates some interesting dependencies between timing and security which make formal verification of the secured protocol more difficult, especially when automated analysis tools are used. This presentation provides an introduction to time synchronization methods and a short overview of the NTS specification. Furthermore, we report on the current progress on the formal verification, highlight with one example the above mentioned security-timing interdependency, and will give an outlook on future steps in our verification project.
14-Apr	Thorsten Wißmann, The Locally Finite Fixpoint and its properties	Coalgebras are a generic way to talk about state or equation-systems. The unique coalgebra homomorphism into the final coalgebra can be understood as the “behaviour”, “semantics”, or “solution” of the corresponding system. In this talk, I will present a uniform framework to talk about the subcoalgebra of the final coalgebra, that captures precisely the behaviours of finitely generated systems, that is, coalgebras with a finitely generated carrier. The induced coalgebra — the locally finite fixpoint (LFF) — is a fixpoint of the functor and has multiple equivalent characterizations. (E.g. as the final “locally finitely generated” coalgebra or as the initial iterative algebra for equation systems).