Balaguer, Sandie and Chatain, Thomas - Avoiding Shared Clocks in Networks of Timed Automata

lmcs:933 - Logical Methods in Computer Science, November 14, 2013, Volume 9, Issue 4
Avoiding Shared Clocks in Networks of Timed Automata

Authors: Balaguer, Sandie and Chatain, Thomas

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. transitions of one automaton may be guarded by conditions 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 an NTA A1 || A2 where A2 reads some clocks reset by A1, does there exist an 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 define an appropriate behavioural equivalence. Then we 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.


Source : oai:arXiv.org:1310.5558
DOI : 10.2168/LMCS-9(4:13)2013
Volume: Volume 9, Issue 4
Published on: November 14, 2013
Submitted on: January 15, 2013
Keywords: Computer Science - Formal Languages and Automata Theory


Share

Consultation statistics

This page has been seen 66 times.
This article's PDF has been downloaded 33 times.