Optimizing timed Automata model Checking via Clock Reordering

VÍCTOR A. BRABERMAN; ALFREDO OLIVERO; FERNANDO SCHAPACHNIK

Río de janeiro, Brasil

Workshop; IEEE International Real-Time Systems Symposium; 2006

IEEE

An essential operation in timed automata model checking is inclusion checking which decides whether a set of states, represented as a convex polyhedron, is included in another set. Several verification tools implement convex polyhedra as square matrixes called DBMs (short for Difference Bound Matrix), where each row and column is associated to a clock in the system under analysis. An element in the matrix represents the bound for the value of a clock or for the difference between two clocks. Inclusion checking can be called hundreds of millions of times during the verification of a medium-size model. The naïve implementation scans each matrix cell by cell and compares it against the corresponding one in the other matrix. If all the checks are successful the first matrix is included into the second. If one of them fails, it is not. In the last case, the order in which matrixes are traversed is decisive for the inclusion checking´s efficiency. In this article we present a clock reordering technique which reduces the number of comparisons needed to find a failure. Experiments show neglectable memory overhead and time savings of up to 17%.