Skip to Main content Skip to Navigation

Avoiding Shared Clocks in Networks of Timed Automata

Sandie Balaguer 1, 2, * Thomas Chatain 1, 2 
* Corresponding author
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Networks of timed automata (NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks, i.e. the transitions of one automaton may be guarded by a condition on the value of clocks reset by another automaton. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given a NTA A1 || A2 where A2 reads some clocks reset by A1, does there exist a NTA A'1 || A'2 without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only, in particular by copying the value of their neighbor's clocks. We discuss a formalization of the problem and give a criterion using the notion of contextual timed transition system, which represents the behavior of A2 when in parallel with A1. Finally, we effectively build A'1 || A'2 when it exists.
Document type :
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Sandie Balaguer Connect in order to contact the contributor
Submitted on : Monday, June 11, 2012 - 10:55:48 AM
Last modification on : Wednesday, February 2, 2022 - 3:51:14 PM
Long-term archiving on: : Wednesday, September 12, 2012 - 2:25:35 AM


Files produced by the author(s)


  • HAL Id : hal-00706608, version 1


Sandie Balaguer, Thomas Chatain. Avoiding Shared Clocks in Networks of Timed Automata. [Research Report] RR-7990, INRIA. 2012, pp.26. ⟨hal-00706608⟩



Record views


Files downloads