A Refined Algorithm for Reachability Analysis of Updatable Timed Automata

Timed automata (TAs) are a widely-used model for formally analyzing real-time systems. Updatable Timed Automata (UTAs), extended from TAs, provide a more flexible way to adjust the value of clock during location switches. The reachability problem of some subclasses of UTAs is decidable. When considering an efficient implementation of these subclasses, the algorithm that is usually used is based on the notion of zones, implemented by Difference Bound Matrices (DBMs). However, similar to that of TAs, the zone-based algorithm is not sound when considering diagonal constraints on clocks, illustrated by a well-known counterexample. This paper proposes a sound zone-based algorithm by introducing extended DBM (EDBM). It refines the standard forward reachability analysis (FRA) algorithm. The correctness of the algorithm is proven and experimental results are given to show the efficiency of the implementation.