Ahmed Bouajjani (travail commun avec Markus Müller-Olm et Tayssir Touili)

We consider models for multithreaded programs based on (dynamic) networks of pushdown systems. We propose reachability analysis techniques for these models based on word/tree automata.

Franck Cassez (travail commun avec Karine Altisen et Stavros Tripakis)

Stéphane Demri (travail commun avec Ranko Lazic)

Temporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A data word is a word over a finite alphabet, together with a piece of data (an element of an infinite domain) at each position. Examples include timed words and XML documents. To refer to the data, temporal logics are extended with the freeze quantifier, first-order logics with predicates over the data domain, and automata with registers or pebbles. We investigate relative expressiveness and complexity of standard decision problems for LTL with the freeze quantifier 2-variable first-order logic over data words, and register automata. The only predicate available on data is equality. Previously undiscovered connections among those formalisms, and to counter automata with incrementation errors, enable us to answer several questions left open in recent literature.

Peter Habermehl (travail commun avec Radu Iosif et Tomas Vojnar)

We describe an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the AVL trees, the red-black trees, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various (possibly all) paths in the tree. The class of TASC is closed under the operations of union, intersection and complement, and moreover, the emptiness problem is decidable, which makes it a practical verification tool. We validate our approach considering red-black trees and the insertion procedure, for which we verify that the output of the insertion algorithm is a balanced red-black tree, i.e. the longest path is at most twice as long as the shortest path.

Serge Haddad (travail commun avec Béatrice Bérard, Franck Cassez, Didier Lime et Olivier (H.) Roux)

In this talk, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass TA- of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for TA- are PSPACE-complete. Furthermore we show that for a TA in TA- with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.

David Janin

Jérôme Leroux (travail commun avec Sébastien Bardin et Gérald Point)

FAST is a tool designed for the analysis of counter systems, i.e. automata extended with unbounded integer variables. Despite the reachability set is not recursive in general, FAST implements several innovative techniques such as acceleration and circuit selection to solve this problem in practice. In its latest version, the tool is built upon an open architecture: the Presburger library is manipulated through a clear and convenient interface, thus any Presburger arithmetics package can be plugged to the tool. We provide three implementations of the interface using LASH, MONA and a new shared automata package with computation cache PRESTAF. Finally new features are available, like different acceleration algorithms.

Nicolas Markey (travail commun avec François Laroussinie et Ghassan Oreiby)

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. On the expressiveness side, we prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") is not as expressive as one could expect, since it does not allow to express the "Weak Until" modality. On the complexity side, we precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Delta2- and Delta3-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also study the complexity of the extension ATL+, and prove that it is Delta3-complete in both cases (and even with fixed number of agents).

Pierre-Alain Reynier (travail commun avec Patricia Bouyer et Serge Haddad)

Timed Petri nets and timed automata are two standard models for the analysis of real-time systems. In this paper, we prove that they are incomparable for the timed language equivalence. Thus we propose an extension of timed Petri nets with read-arcs (RATdPN), whose coverability problem is decidable. We also show that this model unifies timed Petri nets and timed automata. Then, we establish numerous expressiveness results and prove that zeno behaviours discriminate between several sub-classes of RATdPNs. This has surprising consequences on timed automata, for instance on the power of non-deterministic clock resets.

Olivier (H.) Roux (travail commun avec Guillaume Gardey et John Mullins)

Arnaud Sangnier (travail commun avec Sébastien Bardin, Alain Finkel et Etienne Lozes)

We aim at checking safety properties on systems manipulating dynamic linked lists. First we prove that every pointer system is bisimilar to an effectively constructible counter system. We then deduce a two-step analysis procedure. We first build an over-approximation of the reachability set of the pointer system. If this over-approximation is too coarse to conclude, we then extract from it a bisimilar counter system which is analyzed via efficient symbolic techniques developed for general counter systems.

Philippe Schnoebelen (travail commun avec Christel Baier et Nathalie Bertrand)

We introduce NPLCS's, a model for asynchronous communication protocols where messages can be lost according to probabilistic laws, and investigate the decidability of qualitative linear-time verification problems. Beside its application domain, the specificity of this research is that the operational semantics for our model are infinite-state Markovian decision processes.

Mihaela Sighireanu

TReX is a tool for analysis of extended automata, i.e., automata with clocks, counters, lossy fifo queues, and parameters. Parameters are symbolic constants used either by the user to give symbolic bounds or by the tool to accelerate reachability analysis. To manipulate parameters, TReX provides parameterized abstract domains based on well known numerical domains like DBMs and intervals. The operations on these domains use external or internal decision procedures for integers and reals. We show which are the form of the decision problem we need to solve and how we use existing decision procedures of LASH, Omega or Fast.

Nathalie Sznajder

We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures. Informally, external means that the specification is not allowed to constrain internal variables. We provide a decidability criterion for the distributed synthesis problem on a subclass of architectures, named uniformly well-connected, for which there exists a routing of input variables allowing any output process to get the value of all inputs it is connected to. On the positive side, we show how to reduce such an architecture to a pipeline. We also show that this class cannot be extended by letting the routing depend on the output process.

Igor Walukiewicz

Wieslaw Zielonka (travail commun avec Hugo Gimbert)

Retour à la page principale