The programme consists of five Basic Tutorials (4 hours each) devoted to fundamental subjects, and eight Advanced Lectures (2 hours each) focussed on recent results and specific topics.
8:15 - 10:05 | Coffee Break | 10:30 - 12:20 | Lunch | 14:00 - 15:50 | Coffee Break | 16:15 - 18:05 | |
---|---|---|---|---|---|---|---|
Monday, July 28 | Wolfgang Thomas, Logic and Automata | Wolfgang Thomas, Logic and Automata | Wang Yi, Timed Automata | Wang Yi, Timed Automata | |||
Tuesday, July 29 | Phokion Kolaitis, Logic and Databases | Phokion Kolaitis, Logic and Databases | Didier Caucal, Regular Automata and Monadic Theory | Patricia Bouyer-Decitre, Robustness in Timed Systems | |||
Wednesday, July 30 | Christel Baier, Probabilistic Model-Checking | Christel Baier, Probabilistic Model-Checking | Holger Hermanns, Stochastic model checking - A continuous time perspective | Thomas Wilke, Prophetic Automata | |||
Thursday, July 31 | Nir Piterman, Games and Synthesis | Nir Piterman, Games and Synthesis | Martin Lange, Synthesis of Recursive Programs | Richard Mayr, Infinite-State Probabilistic Systems | |||
Friday, August 1 | Jan Van den Bussche, A Logic-Based Approach to Cloud Computing | Mikołaj Bojańczyk, The Unbounding Quantifier | Departure |
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 quantiable. 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.