Trace Abstraction Refinement for Timed Automata

Timed automata are a well known formalism for modeling real-time systems. Model checking of timed automata is important for ensuring that the systems satisfy certain properties. Safety is one of the most important properties for timed automata. In this paper we propose a method for the safety checking of timed automata, which is an adaptation of the general trace abstraction refinement framework to timed automata. The feature of our work is that we use zone-based LU-abstraction instead of interpolation techniques. This method performs zone computation only when necessary, and the abstraction on zones is coarser because only part of the control structure is considered when computing LU-bounds. We give an example to show when this method could perform more efficiently than the traditional zone-based search algorithm.