Retour à la page principale
Automata-based reachability analysis
of pushdown automata networks
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.
Sensor Minimization Problems in Diagnosis of Finite State Systems
Franck Cassez (travail commun avec Karine Altisen et Stavros Tripakis)
LTL with the Freeze Quantifier and Register Automata
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.
Automata-based Verification of Programs with Tree
Updates
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.
When are Timed Automata Weakly Timed Bisimilar
to Time Petri Nets?
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.
Synthèse de programme distribués sur architecture avec cycles et sémantique zéro-delais par codage dans les jeux distribués
David Janin
FAST Extended Release
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.
Expressiveness and Complexity of
ATL
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).
Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences
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.
Non-interférence dans le contexte temporisé
Olivier (H.) Roux
(travail commun avec Guillaume Gardey et John Mullins)
From Pointer Systems to Counter Systems using Shape Analysis
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.
Verification of nondeterministic channel systems
with probabilistic message losses
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.
Parameterized Abstract Domains in
TReX
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.
Distributed Synthesis for Well-Connected
Architectures
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.
Unranked tree algebra
Igor Walukiewicz
Parity games as a limit of discounted
games
Wieslaw Zielonka (travail
commun avec Hugo Gimbert)
Retour à la page principale