Reducing the number of clock variables of timed automata
Conrado Daws, Sergio Yovine · 2002
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...