An Efficient State Space Construction for a Class of Timed Automata

In this paper we propose a timed abstraction, called acceleration, for the analysis of NCTAs, a class of networks of timed automata tailored to model systems composed out of non-deterministic cyclic agents updating shared variables. The abstraction is based on “maximal action zones”, easy to compute on the fly, which generally aggregate regions in a different way than classical zones do. The original and accelerated semantics are shown coherent in the sense that they both lead to the same untimed semantics, and satisfy the same class of positive reachability queries.