Improvements for the Symbolic Verification of Timed Automata

Abstract. Based on the equivalence relation for location based reach-ability between continuous and integer semantics of closed timed au-tomata, Beyer et al. have implemented the verifier Rabbit, with the uni-form representation of reachable configurations. However, the growth of maximal constant of clock variables will decline the performance of Rabbit. The paper proposes an improved symbolic method, using bi-nary decision diagrams (BDDs) to store the symbolic representation of discretized states, for the verification of timed systems. Compared with Rabbit, experiments demonstrate that besides the memory reduction, our implementation is also less sensitive to the size of clock domain