Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton

This paper presents an adaptation of the CEGAR loop approach based on the reduction of the number of clocks in timed automata. In the presented method, an abstraction of the timed automata in which some of the clocks are removed is used to search for a counter-example for a given temporal logic statement. If the counter-example produced by the abstracted timed automaton is not a counter-example of the original timed automaton, the abstracted model is refined by restoring some of the clocks so that the process can be repeated for the new abstracted model. Reducing the number of the clock may result in a substantial reduction in the amount of the computation required for the model checking as the number states is exponential in the number of clocks.