On the composition of timed systems

Abstract

It is generally admitted that timed models can be obtained as extensions of untimed (discrete) models by adding constructs that allow to manipulate time explicitly or implicitly. For instance, timed automata are automata extended with continuous variables, called docks, that can be tested and modified at transitions. Timed process algebras are languages obtained by adding constructs such as delays, timeouts and watchdogs to untmed process algebras. Finally, the different classes of timed Petri nets can be obtained by adding interval time constraints to Petri nets. In timed models, a run can be considered as composed of alternating steps: time steps where time progresses synchronously in all the sequential components and transitions, timeless discrete state changes. This implies in particular, that discrete and continuous steps are mutually exclusive. Model behavior is represented by the language of the time divergent runs.