Abstract: To deal with the state-explosion problem in the specification analysis and verification of timed automata, an automatic abstraction algorithm for timed automata was proposed. By directly abstracting the specifications of a timed automaton instead of its semantic model ofmuch bigger size, this algorithmyields a polynomial time complexity no more than the four power of its topology complexity. An experiment shows that the algorithm can be applied to any timed automaton satisfying a property called linear resetting and used to simplify system specifications to improve their understandability.