On clock difference constraints and termination in reachability analysis of timed automata

The key step to guarantee termination of reachability analysis for timed automata is the normalisation algorithms for clock constraints i.e. zones represented as DBM's (Difference Bound Matrices). It transforms DBM's which may contain arbitrarily large integers (the source of non-termination) into their equivalent according to the maximal constants of clocks appearing in the input timed automaton to be analysed. Surprisingly, though the zones of a timed automaton are essentially difference constraints in the form of x-y ∼ n ¹, as shown in this paper, it is a non-trivial task to normalise the zones of timed automata that allows difference constraints in the enabling conditions (i.e. guards) on transitions. In fact, the existing normalisation algorithms implemented in tools such as Kronos and UPPAAL² can only handle timed automata (as input) allowing simple constraints in the form of x ∼ n. For a long time, this has been a serious restriction for the existing tools. Difference constraints are indeed needed in many applications e.g. in solving scheduling problems. In this paper, we present a normalisation algorithm to remove the limitation, that based on splitting, transforms DBM's according to not only maximal constants of clocks but also the set of difference constraints appearing in an input automaton. The algorithm has been implemented and integrated in the UPPAAL tool, demonstrating that little run-time overhead is needed though the worst case complexity is the same as in the construction of region automata.