Towards an Optimal Generation of Zones Graph Relating Timed Bisimulation Relation and Distribution

The timed automata are extensively used in different fields of formal validation in particular the model checking one. In this paper the authors are interested by a class of TA called durational actions timed automata (daTA) and the zones graph which represents an exact finite state abstraction based on what called Zones. The authors present a novel approach to construct a zone graph, based on the maximality semantics called maximality-based zone graph (MZG) by a local construction approach and they define timed maximality bisimulation relation for real-time model based on the maximality semantics. The authors propose a new method for distributed state space generation of maximality-based zone graph based on DHT structure. They also describe an implementation of this construction (DTaMaZG tool). The experiments given at the end of this article has shown good results especially when comparing with other works that have already proceed in the distributed generation of MLTS (Maximality based Labeled Transition Systems).