Evènement pour le groupe Modélisation et Verification

Date 2010-09-16  11:30-12:45
TitreDistributed Timed Automata with Independently Evolving Clocks 
RésuméWe propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to. Since we have unrelated time values on different components, we are interested in the underlying untimed behaviors of these distributed timed automata rather than their timed behaviors. Thus, the clocks (and time itself) are synchronization tools rather than being a part of the observation. There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. Thus, it can be considered as an underapproximation of the actual behavior. This is a natural choice when checking that a system always satisfies a positive specification. However, to check if a system avoids a negative specification, it is better to use the existential semantics (an overapproximation of the actual system behavior): the set of behaviors that the system can possibly exhibit under some choice of clock rates. We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable, which is shown by a reduction from Post’s correspondence problem. This result is further strengthened to some bounded cases, where we have restrictions on the relative time rates such as fixed slopes. As an alternative to the universal semantics, we propose a game-based reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors. This is joint work with S. Akshay, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurBenedikt Bollig 
UrlLSV, Cachan 

Aucun document lié à cet événement.

Retour à l'index