We propose a method for reducing the number of clocks of a timed automaton by combining two algorithms. The first one consists in detecting active clocks, that is, those clocks whose values are relevant for the evolution of the system. The second one detects sets of clocks that are always equal. We implemented the algorithms and applied them to several case studies. These experimental results show that an appropriate encoding of the state space, based on the output of the algorithms, leads to a considerable reduction of the memory space allowing a more efficient verification. 1 Introduction Timed automata [3, 13], are automata extended with a finite set of real-valued clocks that proceed at a uniform rate and constrain the times at which transitions occur. Since the time component makes the underlying transition system to be infinite, verification algorithms depend on the construction of a finite partition of the state space. As shown in [2, 3] the complexity of the verification probl...

Multirate timed automata are an extension of timed automata where each clock has its own speed varying between a lower and an upper bound that may change from one control location to another. This formalism is well-suited for specifying hybrid systems where the dynamics of the continuous variables are defined or can be approximated by giving the minimal and maximal rate of change. To avoid the difficulties inherent in the verification of multirate timed automata, we follow an approach that consists of first transforming the multirate timed automata into timed automata and then applying the symbolic techniques implemented in KRONOS. We show the practical interest of this approach analyzing two examples recently proposed in the literature and considered to be realistic case studies: a manufacturing plant and the Philips audio control protocol.