A simple approach for reducing timed automata

Today model checking is the most useful verification method of real time systems, so there is a serious need for improving its efficiency with respect to both time and resources. In this paper we present a new approach for reducing timed automata. In fact regions of a region automaton are aggregated according to a coarse equivalence class partitioning based on traces. We will show that the proposed algorithm terminates and preserves original timed automaton behavior.