Tesei : Timed Automata with non-instantaneous Actions

Abstract. 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 σ, there are two particular time instants, the initi-ation 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 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 particu-lar we specify a system which was specified in [7] 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.