B. Boigelot (CFV, University of Liège, Belgium)

Automata-based representations of arithmetic sets

Slides: [PDF]; Refs.: [TXT]

Using automata for representing sets of numbers is an old idea, orginally introduced as a tool for reasoning about decidable fragments of arithmetic. There is now a growing interest in using such automata-based representations as data structures for dealing with the sets of configurations that have to be handled during symbolic state-space exploration, especially when the analyzed systems rely on integers and real variables. In this survey, we will present automata-based representations of integer and real vectors, describe their main properties, and show how they can be used for exploring symbolically infinite state-spaces, as well as for manipulating systems of linear constraints.

F. Herbreteau (LABRI, University of Bordeaux, France)

Accelerated model-checking of timed and hybrid automata

Slides: [PDF]; Refs.: [TXT]

Model-checking timed or hybrid automata requires to traverse infinite state spaces. This entails two main problems: the finite representation and the effective computation of infinite sets of states. We present a technique based on Real Vector Automata (RVA) for the representation of state-sets and on acceleration to help the termination of state-space exploration. RVA are weak Büchi automata that we use to encode sets of values definable in Presburger arithmetic over reals and integers. They can particularly represent infinite periodic unions of sets, that we use in turn to capture loop invariants in the model. We show that we can express the iteration of any loop in a timed automaton as a Presburger formula. Following a result of Comon & Jurski on flatness of timed automata, this yields an algorithm for the computation of the reachability space of timed automata. For linear hybrid automata, we present a technique to compute invariants for ultimately periodic loops. Despite model-checking linear hybrid automata is undecidable, our approach succeeded on many examples found in the literature.

K. G. Larsen (CISS, Aalborg University, Denmark)

Priced Timed Automata and Games

R. Lazic (University of Warwick, United Kingdom)

Automata and logics on structures with data

Slides: [PDF]; Refs.: [BIB]

Even without continuous phenomena, words and trees over finite alphabets are sometimes insufficiently detailed models. A prominent example is processing semistructured data, which may involve attribute values from infinite domains. With such a motivation, several formalisms for reasoning about words and trees with infinitary data have recently been studied, using a variety of techniques. The emerging landscape is interesting, but careful navigation is required for avoiding undecidability and very high complexity.

C. Löding (RWTH Aachen, Germany)

Specification logics for non-regular properties

Slides & Refs.: [PDF]

In the model checking framework for the verification of state based systems, temporal logics as, e.g., linear time temporal logic (LTL) or computation tree logic (CTL) are very popular for specifying properties of the system under consideration. These logics are expressive enough to describe important classes of properties like reachability, safety, or liveness conditions. In the context of software model checking, most of the systems are infinite due to unbounded data structures or recursion. It has turned out that many of the verification techniques can be transferred to the case of recursive programs over finite data types using pushdown automata as a model for the programs. For these models other properties like pre-post-conditions for procedures become interesting. Such conditions cannot be expressed in the usual specification logics because relating entry and exit points of a procedure in a computation is a non-regular condition. In the last few years, initiated by the work of Alur, Etessami, and Madhusudan, some logics have been developed for this purpose. The aim of this talk is to give an overview of these logics and the main results from this area.

P. Schnoebelen (LSV, ENS Cachan, France)

The complexity of lossy channel systems

Slides: [PDF]; Paper: [PDF]

Lossy channel systems are a fundamental computational model for which several verification problems are decidable but exhibit very high worst-case complexity (not multiply-recursive). In this talk we describe how the complexity analysis has been carried out and how it has consequences beyond channel systems.

R. Segala (University of Verona, Italy)

Verification with probabilistic automata

Slides: [PPT]

P. Bouyer (LSV, ENS Cachan, France)

Probabilities in Timed Automata

In this talk I will present a probabilistic semantics for timed automata, that allows to measure the likelihood of properties in a timed system. I will then describe an abstraction that can be used to verify almost-surely LTL properties, and I will present limits of the approach. I will then turn to quantitative aspects, and present an approximation scheme that can be used to compute the probabilities of LTL properties in a timed automaton. This is based on joint works with Christel Baier, Nathalie Bertrand, Thomas Brihaye, Nicolas Markey and Marcus Groesser.

A. David (CISS, Aalborg University, Denmark)

Tool "UPPAAL Tiga"

M. Jurdzinski (University of Warwick, United Kigdom)

Strategy improvement algorithms for timed and hybrid automata

R. Lanotte (University of Insubria, Italy)

Distributed time-asynchronous automata

Slides: [PDF]; Refs.: [DOC]

We investigate the class of distributed time-asynchronous automata, which are tuples of timed automata synchronized on input symbols and whose time-passage transitions are asynchronous (i.e. time is local to each automaton). Time-asynchronous automata can model preemptive scheduling, and their study would help understanding the benefits of using automata theory in solving scheduling problems. We show that the class of distributed time-asynchronous automata is more expressive than timed automata, has a decidable emptiness problem, is closed under union, concatenation, star, shuffle and renaming, but not under intersection. The closure results are obtained by showing that distributed time-asynchronous automata are equivalent with a subclass of stopwatch automata.

J. Leroux (LABRI, University of Bordeaux, France)

TaPAS : The Talence Presburger Arithmetic Suite

Slides: [PDF]

The additive first order theory over the integers and the reals, also called Presburger arithmetic is a good trade off between decidability and expressiveness. We present TaPAS, a suite of tools for this theory. This is a joint work with Gerald Point.

O. Serre (LIAFA, University Paris Diderot - Paris 7, France)

Collapsible Pushdown Automata

In this talk we present an extension of pushdown automata called collapsible pushdown automata. We will give several results on this class. In particular, we will state an equi-expressivity theorem relating collapsible pushdown automata as generators for trees with higher-order recursion schemes. We will also present decidability of parity games played over transition graphs of collapsible pushdown automata as well as consequences and related open problems.

W. Thomas (RWTH Aachen, Germany)

Infinite Games: From Winning Strategies to Optimal Strategies

Slides: [PDF]

In logic and model-checking, infinite games are analyzed with respect to existence of winning strategies. For applications in the automatic synthesis of systems, infinite games require more refined solutions in terms of strategies that are "optimal" in some adequate sense. We discuss this shift of emphasis by the example of "request-response" games, where the winning condition is a conjunction of requirements of the form "if a state with property Q is visited, then later also a state with property P is visited". We present results on the construction of winning strategies that minimize the wait times between visits to Q-states and subsequent visits to P-states.
(joint work with Florian Horn and Nico Wallmeier)