Forward Analysis of Timed Automata with Action Durations: Theory and Implementation

Timed automata are widely used to model real-time systems. In this paper we are concerned by durational actions timed automata (daTA) which is a timed automata handling action durations and true concurrency. Our aim is to compute efficiently the state space of (daTA) in order to verify quantitative timing requirements and preserve the true concurrency property. We have designed a new zone graph under the maximality semantics, named Maximality-based Symbolic Graph (MSG), for describing symbolic execution of daTA. An algorithm based on the symbolic and on-the-fly forwards reach ability analysis algorithm for durational actions timed automata is presented. In the implemented tool TaMaZG, daTA description is compiled into a MSG and represented symbolically using the Difference Bounded Matrices data structure (DBM).