Splitting reachability analysis in hybrid automata

Within the framework of time verification of real time systems, we present a new technique for the reachability analysis of hybrid automata. We call this technique the “Splitting Reachability Analysis”. It is applied to a synchronized product of hybrid automata. The basic idea is to compute separately and simultaneously states sets in each component of a synchronized product of hybrid automata. The composition of these sets is an upper-approximation of the reachable states set of the synchronized product. Compared to a classical technique, the benefit, shown through with the example of the Fischer mutual exclusion protocol, is to reduce the costs in memory and computation time