The second QuantLA spring school takes place from 17th to 20th of May in Leipzig. Our guest lecturers are Véronique Bruyère and Standa Živný.

All talks are held at the Pentahotel Leipzig (Großer Brockhaus 3, 04103 Leipzig), except when indicated.

The talks on Thursday, May 19, from 9 a.m. to 3 p.m. are held at the Leipzig University, Paulinum, Augustusplatz 10, room P502.

The slides of (almost) all talks can be found in the internal pages.

Time Table

Updated: 23. March

Course Programme

Algorithmic Aspects of Two-player Zero-sum and Multi-Player Non Zero-sum Games: Véronique Bruyère

Reactive computer systems (like power plants, plane navigation systems, ABS systems, ...) bear inherent complexity due to continuous interactions with the environment in which they evolve. Formal techniques using mathematical models have been advocated to help to their systematic design. A challenging goal is the automatic synthesis of a correct system from a given specification, that is, a system that enforces this specification no matter how the environment behaves. The mathematical framework used for the synthesis problem is game theory and in particular infinite two-player games played on graphs where the two players are the system and the environment, the vertices of the graph model their possible states, and the edges model their possible interactions. Synthesizing a correct system then means constructing a winning strategy of the system such that, whatever the strategy of the environment, the outcome of the play satisfies the specification. The fundamental algorithmic questions are therefore: Can we decide whether a player has a winning strategy? Can we construct such a strategy, and if possible a simple one? What are the complexities of these problems? In the first part of the tutorial, we will present classical answers to these questions in the case of qualitative specifications like reachability objectives, Büchi objectives, … . We will also present well-known results about games played on weighted graphs with quantitative objectives, in a way to treat specifications like never dropping out of fuel, ensuring a suitable mean response time, … . In the second part of this tutorial, we will consider the extension to multiplayer games where several (instead of two) players have their own objectives that are are not necessarily antagonistic. In this context, the notion of winning strategy has to be replaced by adapted solution concepts that are good for each player with respect to his objective. We will present some different approaches and their related results.

2 x 90 min.

Constraint Satisfaction Problems that Count: Manuel Bodirsky

This lecture is about constraint satisfaction problems (CSPs) that are quantitative in the sense that they can express some form of arithmetic: they « can count ». The most fundamental CSPs of this type are over the integers, the rationals, or reals, for example the feasiblity problem for linear programming, or the max-atoms problem. I will survey what is know about the computational complexity of such CSPs. In particular, I will be interested in CSPs that can be solved in polynomial time, e.g., polynomial-time tractable extensions of linear programming, or polynomial-time tractable fragments of integer linear programming. I will also give an introduction to *polymorphisms* as an important tool from universal algebra to systematically study the complexity of such CSPs.

1 x 60 min.

Formalisms for Data Languages: Karin Quaas and Vitaly Perevoshchikov

In recent years, there has been an active research programme on structures that enrich classical words and trees with additional information. A structure that attracts a remarkable interest especially in the fields of program verification and database management is data words. A data word is a finite sequence in which every position carries two pieces of information: a label from a finite alphabet and a data value from an infinite set such as natural numbers or ASCII strings. The goal of this tutorial is to present an overview of the main formalisms for reasoning about data words.

In the first part, we introduce register automata. A register automaton (RA) is a finite state machine equipped with a finite set of registers. During processing of a data word, the automaton may store the data value of the current position in the registers. It may also test the data value of the current position with the values stored in registers for equality, where the result of this test determines the next action of the automaton. Note that the semantics of an RA is infinite due to the unbounded domain of values that the registers may store. Nonetheless, the emptiness problem for RA is PSPACE-complete; On the other hand side, the language inclusion problem is undecidable. We introduce the logic Freeze LTL, which is an extension of Linear Temporal Logic with a freeze quantifier. With the freeze quantifier one can store the current data value into a register for future comparison. The satisfiability problem for this logic is undecidable in general; One can however prove that the fragment allowing for one register only is decidable by a reduction to the emptiness problem for alternating RA with one register.

The second part of the tutorial deals with first-order logic on data words, an extension of the classical first-order logic on words with data equality checking. We will concentrate on the satisfiability problem for this logic. We prove that the two-variable fragment has decidable satisfiability. For the proof, we introduce data automata (which are slightly different from register automata) and show that every two-variable first-order formula can be effectively translated into an equivalent data automaton. After that, we prove that the emptiness problem for data automata is decidable. We show this by reduction to the emptiness problem for multi-counter automata.

2 x 60 min.

Knowledge Representation: Anni-Yasmin Turhan, Sebastian Rudolph and Gerd Brewka

This course on knowledge representation covers Description Logics (DLs) in the first part. DLs can represent the conceptual knowledge of an application domain in a structured and formally well-understood way. Based on their formal semantics, many reasoning procedures have been defined and were investigated for a range of DLs. This course introduces basic notions underlying knowledge representation with DLs, reasoning procedures for DLs and their complexity. We also take a look at the Semantic Web ontology language OWL and its profiles, which are based on DLs.

The second part of the course deals with Existential Rules, a formalism previously known as tuple-generating-dependencies (TGDs) in databases, which has lately become popular in knowledge representation. We will introduce the central reasoning problem of answering conjunctive queries in the presence of existantial rules and talk about different classes of existential rules as well as their expressivity and associated complexities. We will also address comonalities and differences between existential rules and description logics.

The third part of the course will first motivate the need of nonmonotonic reasoning formalisms, that is, formalisms able to handle rules with exceptions. We then introduce two rather simple nonmonotonic formalisms, namely abstract argumentation frameworks and logic programs under answer set semantics. In each case we discuss semantic foundations and potential applications.

3 x 60 min.

Probabilistic Model Checking: Christel Baier

Markov chains (MC) and Markov decision processes (MDP) are widely used as operational models for the quantitative system analysis. They can be understood as transition systems augmented with distributions for the states (in MC) or state-action pairs (in MDPs) to specify the probabilities for the successor states. Additionally one might add weight functions for modeling accumulated costs or rewards earned along path fragments to represent e.g. the energy consumption, the penality to be paid for missed deadlines, the gain for completing tasks successfully or the degree of the achieved utility.

The tutorial will introduce the main features of discrete-time, finite-state Markovian models (MC and MDP) and their quantitative analysis against temporal logic specifications. It will present the basic principles of the automata-based approach for linear temporal logic (LTL) and probabilistic computation tree logic (PCTL), including a summary of techniques that have been proposed to tackle the state-explosion problem. The last part of the tutorial will present algorithms for dealing with fairness assumptions and computing conditional probabilities and quantiles.

1 x 60 min.

The Complexity of and the Algorithms for Valued Constraint Satisfaction Problems: Standa Živný

In this talk we will present recent results on the computational complexity of and the algorithms for discrete optimisation problems knowns as constraint satisfaction problems (and their optimisation variants). We will focus on algorithmic characterisations, complexity classifications, and main techniques and ideas behind the proofs.

2 x 90 min.

Tricks of the Trade: Franz Baader

The purpose of this course is to make the doctoral students aware of useful (proof) methods that one usually does not encounter in undergraduate studies. On the one hand, we will look at the use of well-founded orders for proving termination, but also for proving other results using Noetherian induction. We will also show how well-founded orders that are useful for these purposes can be constructed. On the other hand, we will consider methods that can be used to show that problems can be decided using only polynomial space.

1 x 90 min.

Weighted Automata and Weighted Logics: Manfred Droste and Heiko Vogler

The goal of this lecture is to investigate weighted automata and weighted logics. Weighted automata on finite words have already been investigated in seminal work of Schützenberger (1961). They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. This concept soon developed a flourishing theory.

We investigate weighted automata and their relationship to weighted logics. For this, we present syntax and semantics of a quantitative logic; the semantics counts 'how often' a formula is true in a given word. Our main result, extending the classical result of Büchi, Elgot and Trakhtenbrot, shows that if the weights are taken from an arbitrary semiring, then weighted automata and a syntactically defined fragment of our weighted logic are expressively equivalent. A corresponding result holds for infinite words. Moreover, this extends to quantitative automata investigated by Henzinger et al. with (non-semiring) average-type behaviors, or with discounting or limit average objectives for infinite words. It also extends to multi-weighted automata and to other discrete structures like trees, traces, pictures, or graphs.

We extend weighted automata (over strings) by a storage, like a pushdown or stack, and define an extension of a weighted MSO-logic such that we again obtain a Büchi, Elgot and Trakhtenbrot result. In the extended weighted MSO-logic we allow one outermost existential quantification over behaviours of a storage type. If we choose iterated pushdown as storage type, then the satisfiability problem of the extended weighted MSO-logic is decidable for each bounded lattice provided that its infimum is computable.

2 x 60 min.