The color coding means:

: all participate
: Doctoral students participate

Abstracts

Torsten Mütze: Proof of the middle levels conjecture

Define the middle layer graph as the graph whose vertex set consists of all bitstrings of length 2n+1 that have exactly n or n+1 entries equal to 1, with an edge between any two vertices for which the corresponding bitstrings differ in exactly one bit. The middle levels conjecture asserts that this graph has a Hamilton cycle for every n≥1. This conjecture originated probably with Havel, Buck and Wiedemann, but has also been attributed to Dejter, Erdös, Trotter and various others, and despite considerable efforts it remained open during the last 30 years. One of the motivations for tackling this conjecture is an even more general conjecture due to Lovász, which asserts that every connected vertex-transitive graph (as e.g. the middle layer graph) has a Hamilton path, and apart from five exceptional graphs, even a Hamilton cycle. In this talk I present a proof of the middle levels conjecture. In fact, I show that the middle layer graph has 2^2Ω(n) different Hamilton cycles, which is best possible.

Toby Walsh: Grammar Constraints

Constraint programming is a powerful and successful technology for solving a wide range of optimisation problems, especially in domains like scheduling and rostering. An attractive mechanism to specify constraints in many domains is via formal languages. For instance, the Regular and Grammar constraints specify constraints in terms of the languages accepted by an automaton and a context-free grammar respectively. I discuss how we reason with such constraints, as well as use minimization techniques to reduce the size of such automata and speed up reasoning.

Nicole Schweikardt: A tutorial on order-invariant logics

Order-invariant formulas are formulas for which the following is true: If a structure satisfies the formula with one particular linear order of the structure's universe, then it satisfies the formula with any linear order of the structure's universe. This tutorial will give an introduction to order-invariant logics: In particular, we will see examples demonstrating the expressive power of these logics, as well as tools for showing certain expressive weaknesses.

Arnaud Sangnier: On the Complexity of Verifying Regular Properties on Flat Counter Systems

Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. That is why, optimal algorithms for model-checking flat counter systems are being designed since this may represent the core of a verification process. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries. In this work, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including Past LTL, first-order logic, linear mu-calculus, infinite and related formalisms. Our results span different complexity classes (mainly from P to PSPACE) and they apply to languages in which arithmetical constraints on counter values are systematically allowed. As far as the proof techniques are concerned, we provide a uniform approach that focuses on the main issues.

This is a joint work with Stéphane Demri and Amit Kumar Dhar.

Vitaly Perevoshchikov: A Logical Characterization of Timed Pushdown Languages

Timed pushdown automata were introduced by Abdulla et al. in LICS 2012 to model the behavior of real-time recursive systems. In this paper, we introduce a quantitative logic on timed words which is expressively equivalent to timed pushdown automata. This logic is an extension of Wilke’s relative distance logic by quantitative matchings. To show the expressive equivalence result, we prove a decomposition theorem which establishes a connection between timed pushdown languages and visibly pushdown languages of Alur and Mudhusudan; then we apply their result about the logical characterization of visibly pushdown languages. As a consequence, we obtain the decidability of the satisfiability problem for our new logic.

This is a joint work with Manfred Droste.

Dietrich Kuske: Integer arithmetic with counting quantifiers

We consider Presburger arithmetic (PA) extended with modulo counting quantifiers. We show that its complexity is essentially the same as that of PA, i.e., we give a doubly exponential space bound. This is done by giving and analysing a quantifier elimination procedure similar to Reddy and Loveland's procedure for PA. Furthermore, we show that the complexity of the automata-based decision procedure for PA with modulo counting quantifiers has the same triple-exponential complexity as the one for PA when using least significant bit first encoding.

Stefan Kiefer: On the total variation distance of labelled Markov chains

Labelled Markov chains (LMCs) are widely used in probabilistic verification, speech recognition, computational biology, and many other fields. Checking two LMCs for equivalence is a classical problem subject to extensive studies, while the total variation distance provides a natural measure for the "inequivalence'' of two LMCs: it is the maximum difference between probabilities that the LMCs assign to the same event. In this talk we develop a theory of the total variation distance between two LMCs, with emphasis on the algorithmic aspects: (1) we provide a polynomial-time algorithm for determining whether two LMCs have distance 1, i.e., whether they can almost always be distinguished; (2) we provide an algorithm for approximating the distance with arbitrary precision; and (3) we show that the threshold problem, i.e., whether the distance exceeds a given threshold, is NP-hard and hard for the square-root-sum problem. We also make a connection between the total variation distance and Bernoulli convolutions.

Andreas Ecke: Quantitative methods for similarity in Description Logics

Similarity is one of the fundamendal notions in psychology and underlies many tasks in human reasoning. In the form of similarity measures, it has been employed in many complex software systems, like object recognition, natural language processing, information retrivial, and knowledge representation and reasoning. However, in all cases, similarity does not have a universally agreed upon definition, and many different properties of similarity and computational approaches have been proposed and debated.
After a short introduction to similarity in general, we will give an overview of the research field of similarity measures in Description Logics, and discuss advantages and disadvantages of these measures. We will present an approach to use similarity measures to relax the problem of query answering in the Description Logic EL, and introduce a new measure for EL that can be used for this task. Moreover, we will present an idea to directly include concept similarity into DL ontologies via the use of prototypes and conclude the talk with the goals and current progress of the thesis.

Lorenzo Clemente: Un-timing the stack in Dense-timed Pushdown Automata

Recently, a model of Dense-timed Pushdown Automata has been proposed by Abdulla et al. at LICS'12 [1]. This model extends Pushdown Automata by adding real-valued clocks that can be reset and checked against constants, in the spirit of Timed Automata by Alur and Dill [2]. Additionally, stack symbols are equipped with real-valued ages, which monotonically grow with time, and which can be checked against constants at the time of pop. Emptiness for this model is EXPTIME-complete [1].
While the original definition of DPDA is inputless (the input is irrelevant for what concerns emptiness), here we consider DPDAs as acceptors of timed languages, and study their expressive power. We show that DPDAs accept the same class of languages as DPDAs with untimed stack, i.e., where pop operations do not have any constraint on the age of the topmost stack symbol. Thus, the addition of ages to the stack does not increase the expressive power of the model w.r.t. timed languages. We further show that the stack can be untimed even in the presence of seemingly more powerful pop diagonal constraints between the age and the other clocks.
Finally, we complement these equivalence results by showing that, if we allow integer tests on the age, then the stack cannot be untimed anymore.
This is joint work with S. Lasota.
[1] P. A. Abdulla and M. F. Atig and J. Stenman, "Dense-Timed Pushdown Automata", LICS'12.
[2] R. Alur and D. L. Dill, "A theory of timed automata", Theor. Comput. Sci. 1994.

Patricia Bouyer-Decitre: On the optimal reachability problem in weighted timed games

A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal weight and almost-optimal strategies can be computed.
In this talk, I will give an overview of rather old results about the optimal reachability problem in weighted timed games. I will then focus on more recent results, that are joint work with Samy Jaziri and Nicolas Markey. First I will show that the value problem is undecidable in weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. I will then describe an algorithm to compute arbitrary approximations of the value in a game, and corresponding almost-optimal strategies. The algorithm applies to a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.

Shiguang Feng: The Complexity of Path-checking for MTL and TPTL over Data Words

Precise complexity results are derived for the model-checking problem for TPTL (timed propositional temporal logic) on (in)finite data words and deterministic one-counter machines. Depending on the number of register variables and the encoding of numbers in constraints (unary or binary), the complexity is either P-complete or PSPACE-complete.

Claudia Carapelle: Which "Comparability Graphs" are embeddable into "Trees"?

We recently proved that Extended Computation Tree Logic (ECTL*) enriched with constraints over a class of structures A has a decidable satisfiability problem, provided that A satisfies certain properties. One of them - the EHD property - consists in being able to provide an MSO-characterization of all and only those countable structures which are homomorphic to some element of A. We treat the case where A is a class of "tree-like" structures, such as a semi-linear orders, ordinal trees or trees of a fixed height, and prove that these structures enjoy the EHD property. The proof techniques are simple and at the same time unusual, as they make use of some topological and set-theoretic properties of "Comparability Graphs" (we are using non-classical comparability graphs, hence the quotations).

Diego Figueira: On reflexive-transitive navigation in the presence of data values

When working on data words or data trees, it is often important to be able to compare data values from positions far apart. In modal or navigational languages, such as LTL or XPath, this is done using transitive closure modalities (such as Future, or Descendant). As it turns out, this type of modalities very easily makes the satisfiability problem either undecidable or with non-primitive recursive complexity. However, in many of these cases, replacing modalities with their reflexive-transitive counterpart (as opposed to only transitive) entails a series of monotonicity properties useful to gain decidability, even elementarity. The purpose of this talk is to give an idea of why adding reflexivity improves things.
[The results I will present are based on my work that appeared in LICS'11 and PODS'13.]