Sujet : Verification using traces and net unfoldings

Responsable : Igor Walukiewicz
Téléphone : 69 17
e-mail : voir la page web
Site Web : http://www.labri.fr/Perso/~igw/
Equipe : LAAA

Présentation du sujet :

Most frequently an execution of a system is represented by a sequence of
actions that the system performed. This representation is not perfect,
especially when the system is composed from several components working
concurrently. Not only the size of the representation may be
exponential in the number of components, but also the information about
concurrency is absent in the model. By comparison, in a trace model
the concurrency information is made explicit by declaring which
actions can occur concurrently. This gives a more faithful and,
sometimes, a more succinct representation. The set of all the
executions of the system may have a trace representation that is
exponentially more succinct than the sequence representation. This
suggests to try to use a methodology based on traces, rather than
sequences, in verification.

In verification, called model-checking in this context, we are given a
model of a system and a property of executions and we want to check if
all executions of the system satisfy the property. A simple example of
such a property is reachability: some final state is reached. More
generally one uses so called programme logics to describe properties
of executions. Prominent examples of such logics are: propositional
temporal logic (LTL) and the mu-calculus.

To develop trace-based methodology for verification on needs to model
systems by devices with explicit representation of concurrency. These
can be, for example, communicating finite automata or 1-safe Petri
nets. Unwinding technique of McMillan gives good results for verifying
reachability properties for such models. This technique was
consequently developed in the references given below. The objective is
to extend this technique to programme logics.

A good progress was made in recent years in understanding of programme
logics to describe trace properties. We now have a number of temporal
logics with good expressive power and based on relatively simple
operators. The goal is to see which operators are most suitable in the
context of the unwinding technique.

In conclusion, the goal of this thesis would be to use the progress
made in unfolding methods as well as programme logics in order to
develop a new verification method.

Mot-clés : traces, model-checking, Petri-net unfolding method

Références :
(All the papers are available from the authors\' pages.)