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