Timed Automata with non-Instantaneous Actions

In this paper we propose a model, timed automata with non-instantaneous actions, which allows representing in a suitable way real-time systems. Timed automata with non-instantaneous actions extend the timed automata model by dropping the assumption that actions are instantaneous, that is an action can take some time to be completed. Thus, for an action $\sigma$, there are two particular time instants, the initiation of the action and the completion of the action, which may occur at different times. We investigate the expressiveness of the new model, comparing it with classical timed automata. In particular, we study the set of timed languages which can be accepted by timed automata with non-instantaneous actions. We prove that timed automata with non-instantaneous actions are more expressive than timed automata and less expressive than timed automata with $\epsilon$ edges. Moreover we define the parallel composition of timed automata with non-instantaneous actions. We show how real systems can be suitably modeled by them, in particular we specify a system which was specified in Alur and Dill (1994) by timed automata. We point out how the specification by means of a parallel timed automata with non-instantaneous actions is, in some cases, more convenient to represent reality.