|
Evènement pour le groupe Modélisation et Verification
Date | 2010-09-16 11:30-12:45 |
Titre | Distributed 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. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Benedikt Bollig |
Email | bollig@lsv.ens-cachan.fr |
Url | LSV, Cachan |
Aucun document lié à cet événement. RetourRetour à l'index
| |