Sujet : Synthèse pour une logique temps-réel faible

Responsable : A. Arnold et Igor Walukiewicz
Téléphone : 6094 / 6917
e-mail : arnold@labri.fr, igw@labri.fr
Equipe : MVTsi--L3A

Présentation du sujet :



Synthesis for weak real-time logics

Synthesis problem attracted recently quite a bit of attention. There
are many formulations of this problem; here we consider the following
one.

Given a plant we would like to find a controller such that the
controlled plant satisfies the given specification (say expressed in
the mu-calculus). We model a plant P by a deterministic finite
automaton over the alphabet of actions. Such an automaton represents
all possible behaviours of the plant. A controller is also such an
automaton. The controlled plant is PxC, i.e. the synchronous product
of P and C. Intuitively the role of C is to forbid some actions of
P.

Formally the problem is:
given P, \alpha, \beta find C such that PxC satisfies \alpha and C
satisfies \beta.
Hence, \alpha is the specification of the desired behaviour of the
controlled plant and \beta specifies additional requirements on the
controller. This formulation of the synthesis problem has been recently
investigated in "Games for synthesis of controllers with partial
observation"
, A. Arnold, A. Vincent and I. Walukiewicz


The object of the thesis would be to investigate the possible
extensions of this setting to timed specifications. A lot is known
about this extension if one considers that specifications are given by
timed automata cf. "Timed Control Synthesis for External Specifications" by Deepak D'Souza and P. Madhusudan. In most cases the synthesis
problem for real-time specifications turns out to be undecidable.

An interesting and very different specification formalism was proposed
recently:
"A Decidable Fixpoint Logic for Time-Outs"
, Maria Sorea
The advantage of this formalism is that it is decidable and closed
under Boolean operations. It is also much less ambitious in expressive
power because it expresses the properties of a subclass of timed
automata.

The first goal of this thesis would be to define the division
operation for the above fixpoint logic similarly to the division
operation from the Arnold et.al. paper. Later one can study the
complexity questions as well as the numerous possible extensions.




Mot-clés : Synthèse de contrôleurs, Logique temps-réel