The color coding means:

: all participate
: Doctoral students participate

Abstracts

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.

Szymon Toruńczyk: Verification with Atoms

Sets with atoms extend standard set theory, by allowing to construct sets basing on a fixed underlying logical structure, using first-order formulas. This gives rise to a more relaxed notion of a finite set, which in turn allows to generalise notions of finite automata, Turing machines, programming languages, etc. It turns out that these more general models have, on one side, good mathematical and computational properties, and on the other hand, applications to theoretical verification. In particular, we show how this can be applied to verify properties of systems manipulating a finite database.

Daniel Gburek: Stochastic Transition Systems

In this talk I will present my ongoing research on stochastic transition systems.

Markus Teichmann: Intersection of Tree Languages for Weighted Approximation

In this talk, I describe a method to approximate a weighted linear nondeleting context-free tree grammar (wlnCFTG) by means of a weighted regular tree grammar (wRTG). More specifically, I find the closest (concerning Kullback-Leibler divergence) weight assignment for a given unambiguous regular tree grammar. For this, I recall the intersection of a wlnCFTG and a wRTG. The approximation result generalizes existing results from the string case and the case of tree adjoining grammars.

Salomon Sickert: Deterministic omega-Automata for LTL: A safraless, compositional and mechanically verified construction

Recently a new method directly translating linear temporal logic (LTL) formulas to deterministic (generalized) Rabin automata was proposed by Javier Esparza and Jan Křetínsḱy. Compared to the existing approaches of constructing a non-deterministic Buechi-automaton in the first step and then applying a determinization procedure (e.g. some variant of Safra's construction) in a second step, this new approach preservers a relation between the formula and the states of the resulting automaton. While the old approach produced a monolithic structure, the new method is compositional. Furthermore it was shown in experiments that the resulting automata were much smaller then the automata generated by existing approaches. In order to guarantee the correctness of the construction a full verification of it was done using Isabelle/HOL.

In my talk I will introduce the basic concepts and essential ideas of the construction.

Erik Paul: Weighted Tree Automata, Ambiguity and Logics

Ambiguity is a structural property of automata. While in the unweighted case every recognizable word or tree language is also deterministically recognizable, weighted automata are not determinizable, meaning that ambiguity is also inherent to recognizable power series and tree series. As weighted logics provide another method to describe these series, it is interesting to consider how the ambiguity of automata relates to formulas of such a logic. In my talk I will present two results concerning the ambiguity of weighted tree automata which have applications in translating different ambiguity classes of weighted tree automata into characteristic formulas of a suitable weighted logic.

Stefan Dück: Weighted Automata and Logics on Graphs using Valuation-Monoids

Weighted automata model quantitative features of the behavior of systems and have been investigated for various structures like words, trees, traces, pictures, and nested words. In this talk, we present a general model of weighted automata acting on graphs, which form a quantitative version of Thomas' unweighted model of graph acceptors. We derive a Nivat theorem for weighted graph automata which shows that their behaviors are precisely those obtainable from very particular weighted graph automata and unweighted graph acceptors with a few simple operations. We also show that a suitable weighted MSO logic is expressively equivalent to weighted graph automata. As a consequence, we obtain corresponding Büchi-type equivalence results known from recent literature for weighted automata and weighted logics on words, trees, pictures, and nested words. Establishing such a general result has been an open problem for weighted logic for some time. Furthermore, we extend the underlying weight model to valuation monoids, a very general weight structure, which in particular allows to model the computation of average and discounting. Using valuation monoids, we investigate how to extend our results to infinite graphs.

Ludwig Staiger: ω-automata: Topology and Measure

ω-automata play a major role in the study of correctness of reactive and concurrent systems. In this respect the largeness of ω-languages (sets of infinite words) accepted by finite automata in an important issue. In the talk we compare two aspects of largeness: topological density and and probabilistic measures. In contrast to the case of general ω-languages for ω-languages accepted by finite automata topological and measure-theoretical (in particular, probabilistic) largeness coincide. We show this for the usual topology of the Cantor space and a large class of not necessarily probabilistic measures.

Pavlos Marantidis: Approximately Solving Linear Language Equations

Unification of concept terms in the simple Description Logic FL_0 were proved by Baader and Narendran to be equivalent to solving linear equations in Formal Language Theory. Several decidability and complexity results have been derived since then. In this talk, ongoing research will be presented in the case when there is no solution to such equations. We define measures for counting how “good” an approximation is, and we provide algorithms for proving the existence and finding the optimal approximation in each case. Finally, similar results for set equations are presented.

Jarkko Kari: An Algebraic Geometric Approach to Multidimensional Patterns

We apply linear algebra and algebraic geometry to study infinite multidimensional words of low pattern complexity. By low complexity we mean that for some finite shape, the number of distinct sub-patterns of that shape that occur in the word is not more than the size of the shape. We are interested in discovering global regularities and structures that are enforced by such low complexity assumption. Using Hilbert's Nullstellensatz we prove a decomposition of the word into finitely many periodic components. We briefly discuss applications of our technique in the Nivat's conjecture and the periodic tiling problem.

Lisa Hutschenreiter: Permutation Pattern Avoidance Classes and their Model Companions

In this talk I will present the results of my master’s thesis where I took a look at the model theoretic properties of permutation pattern avoidance classes. These classes have been studied primarily from a combinatorial point of view for quite some time now. Regarding permutations as finite relational structures Cameron proved that apart from the trivial class of permutations there are only five permutation classes which are Fraïssé classes. With this in mind the goal was to analyse some of the model theoretic properties of pattern avoidance classes that are not Fraïssé classes. In particular, I strived to examine in which cases the first-order theory of such a class has a model companion, and whether the model companion is ω-categorical. If such an ω-categorical model companion exists, this means among other things that the class has a unique universal limit even if it is not a Fraïssé class. To get a better understanding of the problem at hand my focus was on studying classes that avoid one or multiple patterns of length 3. It turned out that for infinite classes that avoid at least two patterns of length 3 the joint embedding property entails the existence of such a unique universal limit which lead to the conjecture that this is true for any pattern avoidance class.

Markus Ulbricht: Charging Strategies for Hybrid Cars

In my diploma thesis, I examined a model for hybrid cars aiming towards minimizing recharging costs when a route and the service stations are given. In this talk, I give a brief overview of the model and some natural modifications, the occurring optimization problems and approaches how to solve them.

Bernd Finkbeiner: Temporal Logics for Hyperproperties

There are many important properties of computer systems that cannot be described by referring to individual execution traces. For example, information flow policies characterize the circumstances under which an external observer can distinguish two executions. Because these properties are properties of sets of execution traces, rather than properties of individual traces, they are called hyper properties. In this talk, I will present temporal logics for hyperproperties. Unlike classic temporal logics like LTL or CTL*, which refer to one computation path at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL* can express properties that relate multiple paths by explicitly quantifying over multiple paths simultaneously. I will relate the new logics to the linear-branching spectrum of process equivalences, present model checking algorithms, and report on experience with applying the logics to the verification of real hardware designs, including an I2C bus master, the symmetric access to a shared resource in a mutual exclusion protocol, and the functional correctness of encoders and decoders for error resistant codes.

Vojtěch Forejt: Frequency LTL in probabilistic systems

In this talk I will present frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator Gp expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended “until” and “globally” operator, leading to undecidability of most interesting problems.

For the variant I will present, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but under some restrictions, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.

This talk is based on joint work with Jan Krčál and Jan Křetínský (and papers presented at CONCUR 2015 and LPAR 2015).

Luisa Herrmann: A Weighted MSO Logic with Storage Behaviour and its Büchi-Elgot-Trakhtenbrot Theorem

We introduce a weighted MSO-logic in which one outermost existential quantification over behaviours of a storage type is allowed. As weight structures we take unital valuation monoids which include all semirings, bounded lattices, and computations of average or discounted costs. Each formula is interpreted over finite words yielding elements in the weight structure. We prove that this logic is expressively equivalent to weighted automata with storage. In particular, this implies a Büchi-Elgot-Trakhtenbrot Theorem for weighted iterated pushdown languages. For this choice of storage type, the satisfiability problem of the logic is decidable for each bounded lattice provided that its infimum is computable.

Johannes Osterholzer: Linear Context-Free Tree Languages and Inverse Homomorphisms

We prove that the class of linear context-free tree languages is not closed under inverse linear tree homomorphisms. The proof is by contradiction: we encode Dyck words into a context-free tree language and prove that its presage under a certain linear tree homomorphism cannot be generated by any context-free tree grammar. A positive result is also obtained: the linear monadic context-free tree languages are closed under inverse linear tree homomorphisms.