### Distributed Timed Automata with Independently Evolving
Clocks

S Akshay, B Bollig, P Gastin, M Mukund and K Narayan Kumar

*Proc. CONCUR 2008*, Springer LNCS 5201 (2008), 82-97.

*© Springer-Verlag Berlin Heidelberg*

### Abstract

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.

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. 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---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 turns out to be undecidable. As
an alternative to the universal semantics, we propose a
*reactive* semantics that allows us to check positive
specifications and yet describes a regular set of behaviors.