CHRISTEL BAIER: Probabilistic Model-Checking
Slides
Abstract: 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. The first part will present the basic princi- ples of the automata-based approach for linear temporal logic (LTL) and probabilistic computation tree logic (PCTL), including a summary of tech- niques that have been proposed to tackle the state-explosion problem. The second part of the tutorial will present algorithms for dealing with fairness assumptions and computing conditional probabilities and quantiles.

PHOKION KOLAITIS: Logic and Databases
Slides, part1, Slides, part2
Abstract: During the past forty years, there has been a continuous and fruitful interaction between logic and databases. The aim of this tutorial is to present an overview of this interaction by focusing on two topics that have occupied a central place in database research: the connections between logic and database query languages, and the connections between logic and database dependencies.

The first part of the tutorial will cover the connections between logic and database query languages with emphasis on first-order logic and its extensions with mechanisms embodying recursion, such as Datalog and its variants.

The second part of the tutorial will cover some of the main concepts and results about logic and database dependencies, including the formalization of database dependencies in fragments of first-order logic, the exploration of the implication problem for database dependencies, and the more recent uses of database dependencies in data exchange and data integration.

NIR PITERMAN: Games and Synthesis
Slides
Abstract: Reactive systems such as robot controllers and web interfaces are systems that persistently interact with their environment. Such systems are notoriously hard to design and implement. Synthesis is a technique for automatically generating correct-by-construction reactive systems from high-level descriptions. This is one of the greatest challenges in the area of formal methods. Recent years have seen significant theoretical and practical progress in this field leading to applications in hardware design, robotics, user programming, and model-driven development.

This course will cover the theoretical background of synthesis of reactive systems from linear temporal logic specifications. We will introduce the problem and show how it can be viewed as a two-player game between a system and its environment. We will consider algorithms for solving several types of simple games and show a direct reduction from LTL synthesis to parity games. We will then turn to highlight some of the problems with this approach and follow two possible lines of attack. The first, through restriction of the specification language and the second through bypassing some of the difficulties involved in the solution of such games. Finally, we will consider other practical problems in applications of synthesis and the current suggestions on how to solve them.

WOLFGANG THOMAS: Logic and Automata
Slides, part1, Slides, part2
Abstract: Lecture 1: Historical introduction. We explain how the “automata theoretic method” developed over several decades as an approach to solve logical decision problems, today extended to a powerful framework for verifying and synthesizing programs.

Lecture 2: Büchi automata. This lecture gives two proofs of the fundamental result on omega-automata, the determinization of Büchi automata: a more abstract proof focusing on the conceptual core of the result, and a concrete construction optimizing the complexity in terms of number of states.

Lecture 3: Tree automata and infinite games. The theory of automata on infinite trees is outlined, leading to two results with great impact: the decidability of the monadic second-order theory of the infinite binary tree, and the synthesis of finite-state winning strategies in regular infinite games.

Lecture 4: Infinite models and limits of decidability. We discuss applications of the previous results for obtaining complex infinite models (“infinite-state systems”) with good decidability properties. An important example is the “pushdown hierarchy” (or “Caucal hierarchy”), a rather unexplored landscape of infinite models each of which has a decidable monadic second-order theory.

WANG YI: Timed Automata
Abstract: This lecture will introduce the theory of timed automata and its application in modeling and analysis of embedded and real-time systems, with a focus on the concrete and abstract semantics of timed automata based on transition systems, regions and zones, and related decision problems. The lecture will also provide a tutorial on UPPAAL, a model checher for timed automata, developed jointly by Uppsala University in Sweden and Aalborg University in Denmark, covering the UPPAAL input language for modeling, Timed CTL for property specification, and central algorithms and data structures implemented in UPPAAL.

MIKOŁAJ BOJAŃCZYK: The Unbounding Quantifier
Abstract: MSO+U is an extension of monadic second-order logic, which adds a quantifier U, called the unbounding quantifier. A formula UX.phi(X) says that phi(X) is true for arbitrarily big finite sets X. Languages definable in MSO+U look like they admit finite state recognisers. For instance consider the left Myhill-Nerode equivalence: finite words w and w' are equivalent if for every infinite word u, either both or none of the words wu, w'u are in the language. It is not difficult to show that languages recognised in MSO+U have finitely many equivalence classes under this relation.

In the talk, I will discuss two results: a positive result about decidability of Weak MSO+U, and a negative result about undecidability of MSO+U on infinite trees.

The positive result is that finite state recognisers do exist when set quantification is restricted to finite sets, i.e. in Weak MSO+U. With finite set quantification only, the logic admits automata models for both infinite words and infinite trees, and is decidable.

The negative result is about MSO+U over infinite words and trees. This logic turns out to be dangerously expressive already over infinite words, e.g. it can recognise languages that are arbitrarily high in the projective hierarchy known from descriptive complexity. This topological complexity can be combined with Shelah's proof of undecidability of MSO over the real numbers, to show that MSO+U is undecidable over infinite trees (under the set-theoretic assumption that V=L).

PATRICIA BOUYER-DECITRE: Robustness in Timed Systems
Slides
Abstract: Timed automata, an extension of finite automata with analog clock variables, are now a well-understood modelling formalism for real-time systems. Efficient model-checking algorithms have been designed, and several tools are now available, that alows for the verification of various properties in timed automata. Basics of timed automata verification will be given in the tutorial by Wang Yi.

The whole verification process makes strong assumptions on the (abstract) model of timed automata: it assumes infinite precision of the clocks, perfect synchrony, instantaneous actions, etc. However concrete implementations cannot always be assumed to satisfy these assumptions; there is therefore a need to study verification methodologies for timed automata where these idealistic assumptions are relaxed.

In this lecture, we will describe different approaches to the robustness of timed automata with respect to slight perturbations or errors in the system's behaviour, and we will concentrate on robustness against timing errors (measuring errors, imprecise clocks, etc).

The benefits of such an approach will be twofold: First, robustness is a desired property of a real-time system, which should tolerate clock imprecisions. Second, it will reconcile abstract models and real-world systems, in the sense that the behaviours of the design would more closely correspond to the behaviours of the real system. This is a desirable condition if we want to transfer the analysis made on the abstract model to the real-world system.

JAN VAN DEN BUSSCHE: A Logic-Based Approach to Cloud Computing
Slides
Abstract: In cloud computing one uses a cluster of compute nodes to solve problems that are computationally intensive (e.g., weather prediction) or data-intensive (big data). We present an approach to model data-intensive computations on clusters using “relational transducers”, which are an established logic-based formalism from database theory. This logic-based approach can be seen as a formal model of the Bloom programming language for cloud computing, developed at UC Berkeley. Our model allows us to formalise “eventual consistency” which is a key notion in cloud computing and big data. Moreover, the model allows us to formally investigate a number of conjectures made by Joe Hellerstein on the relationship between monotonicity of database queries and programs, and the need for coordination between compute nodes. We will present our results on the computational power of relational transducer networks; on the decidability of eventual consistency; on the characterization of coordination-free database queries (Hellerstein's “CALM” conjecture); and on the use of Datalog for modeling cloud computations (Hellerstin's “CRON” conjecture).

DIDIER CAUCAL: Regular Automata and Monadic Theory
Slides
Abstract: We first recall some fundamental results on the transition graphs of pushdown automata: their identity with the prefix transition graphs of word rewriting systems, the finiteness of their decomposition by distance (as shown by Muller and Schupp), their generation by deterministic graph grammars, and their construction from the complete binary tree via inverse path functions. These graphs, seen as infinite automata, can be generalized to so-called regular automata either by applying monadic interpretations to the complete binary tree, or by considering the transition graphs of recognizable prefix word systems.

HOLGER HERMANNS: Stochastic model checking - A continuous time perspective
Abstract: Compositional model construction and model checking are two aspects of a modern strategy to ensure correctness of system designs. In the era of power-aware, wireless and distributed systems, correctness guarantees for such systems must become quantiable. Instead of guaranteeing that a system is performing the expected tasks, we are ultimately interested in guaranteeing that the system performs its task within a given time bound and with power consumption within a given limit. Or better: that the probability thereof is above a given threshold. In this lecture I will paint the landscape of behavioural models for probability, time, and cost, with a strict focus on concurrent Markov models in continuous time. I discuss foundational and practical aspects of compositional modelling and model checking such systems.

MARTIN LANGE: Synthesis of Recursive Programs
Slides
Abstract: Temporal logics are widely used in the specification and verification of reactive and concurrent systems for the purpose of building correct systems. Verification through model checking for instance is used to prove that a system, constructed in a possibly faulty way, satisfies a formal specification. Synthesis aims at eliminating errors in the construction phase already: a system (model) should automatically be derived from the formal specification such that satisfaction is guaranteed. Synthesis is therefore closely related to a logic's satisfiability problem: apart from deciding whether a formula has a model, such a model should also be returned.

In this talk we will present a generic game-theoretic approach to the satisfiability problems for various temporal logics. Typical known logics that can be embedded into MSO have the finite model property though, i.e. synthesis for these logics is restricted to finite models only. In order to create the theoretical foundations for synthesis of infinite-state systems like recursive programs for instance it is necessary to consider temporal logics beyond MSO that do not have the finite model property. There is only a narrow gap between the finite model property on one side and undecidability on the other. A family of temporal specification languages in this corridor - therefore suitable for such synthesis purposes - is obtained by enriching classical temporal logics with visibly pushdown languages.

RICHARD MAYR: Infinite-State Probabilistic Systems
Slides
Abstract: The topic of this lecture are Markov chains, Markov decision processes and stochastic games with infinite state spaces. For example, pushdown automata model unbounded recursion, and their probabilistic extension induces infinite-state recursive Markov chains. By adding one or two strategic players, one obtains recursive Markov decision processes and stochastic games, respectively. By restricting the stack alphabet to just one symbol (plus a bottom symbol), one obtains probabilistic one-counter machines, arguably the simplest class of infinite-state probabilistic systems. Another class are probabilistic lossy channel systems that model message passing communication via unboundedly buffered but unreliable communication channels. We give an overview over techniques for analyzing such systems and show how to verify several qualitative and quantitative properties.

THOMAS WILKE: Prophetic Automata
Abstract: Prophetic automata are reverse deterministic Büchi-automata, so special automata on infinite words. The talk covers the transformation of Büchi automata into prophetic automata, classfication of fragments of temporal logic using prophetic automata, and related topics.