Avoiding Shared Clocks in Networks of Timed Automata

Networks of timed automata (NTA) are widely used to model distributedreal-time systems. Quite often in the literature, the automata are allowed toshare clocks, i.e. transitions of one automaton may be guarded by conditions onthe value of clocks reset by another automaton. This is a problem when oneconsiders implementing such model in a distributed architecture, since readingclocks a priori requires communications which are not explicitly described inthe model. We focus on the following question: given an NTA A1 || A2 where A2reads some clocks reset by A1, does there exist an NTA A'1 || A'2 withoutshared clocks with the same behavior as the initial NTA? For this, we allow theautomata to exchange information during synchronizations only, in particular bycopying the value of their neighbor's clocks. We discuss a formalization of theproblem and define an appropriate behavioural equivalence. Then we give acriterion using the notion of contextual timed transition system, whichrepresents the behavior of A2 when in parallel with A1. Finally, we effectivelybuild A'1 || A'2 when it exists.Comment: Article accepted to Logical Methods in Computer Science. Number: LMCS-2013-837 Special issue: 23rd International Conference on Concurrency Theory (CONCUR 2012