A quadratic-time DBM-based successor algorithm for checking timed automata

Most of the timed automaton model checking algorithms explore state spaces by enumeration of time zones. The data structure called Difference Bound Matrix (DBM) is widely adopted to represent time zones because of its efficiency and simplicity. In this paper, we first present a quadratic-time algorithm to compute the canonical form of the conjunction of a canonical DBM and a time guard or a location invariant. Based on this algorithm, we present a quadratic-time DBM-based successor algorithm for timed automaton model checking.