Sujet : Logics
for real-time systems
Responsable : Igor Walukiewicz
Téléphone : 05 40 00 69 17
e-mail : igw@labri.fr
Équipe : Méthodes Formelles
Thème : Logics for real-time systems
Présentation du sujet :
Sometimes a
correct behaviour of a system depends on its reaction time
to some events. A standard example is a controller of a
steam boiler
that has to keep water temperature in the desired range. In
such a
case it is necessary to model the flow of time explicitly. Usually,
time is modeled by real numbers as the input events of the
system are
generally of a continues rather than discreet nature.
Many formalisms were proposed to model such phenomena. The
most widely
known is an extension of finite automata with time [A]. Unlike
in the
case of finite automata, automata with time are not closed
under
complementation. Subsequently many authors tried to find a "nicer"
classes of automata that have better closure properties. Recently
an
alternating-timed automaton model was proposed [LW]. The
limitation of
this model is that it uses only one clock, but the advantage
is that
it is closed under boolean operations.
A different approach is to consider a logic for real-time
properties. By definition, a logic has some good closure
properties;
but then most of the logics over reals are undecidable. Some
interesting decidable logics over reals were proposed by
Hirshfeld and
Rabinovich [HR1,HR2]. These are first and monadic second
order logics
with restrictions on the use of +1 predicate.
The objective in this work would be to understand the
relations
between alternating timed automata and the logics mentioned
above. Some results indicate that their expressive power is
not the
same but we do not know any concrete example. It would be
also very
interesting to see who logic or automata can be modified to match
the
expressive power of other formalism.
Mot-clés : Real-time sytems, automata, logics
Références :
[A] Timed Automata. 11th International Conference on
Computer-Aided
Verification, LNCS 1633, pp. 8-22, Springer-Verlag,
1999. http://www.cis.upenn.edu/~alur/onlinepub.html
[HR1] Y. Hirshfeld
and A. Rabinovich Quantitative Temporal Logic. In Computer
Science
Logic 1999, LNCS vol. 1683, pp172-187, Springer Verlag
1999. http://www.math.tau.ac.il/~rabinoa/conference.html
[HR 2] Y. Hirshfeld and A. Rabinovich A Framework for
Decidable Metrical
Logics. In ICALP99, LNCS vol. 1644, pp 422-432, Springer
Verlag
1999. http://www.math.tau.ac.il/~rabinoa/conference.html
[LW] S. Lasota
and I. Walukiewicz Alternating Timed Automata, manuscript