Hypervolume Approximation in Timed Automata Model Checking

Dierence Bound Matrices (DBMs) are the most commonly used data structure for model checking timed automata. Since long they are being used in successful tools like Kronos or UPPAAL. As DBMs represent convex polyhedra in an n-dimensional space, this paper explores the idea of using its hypervolume as the basis for two optimization techniques. One of them is very simple to implement. The other, an improvement over the rst, requires more involved programming. Each of them saves verication time (up to 19% in our case studies), with a modest increase of memory requirements. Their impact diers among the dierent case studies but, as they can be combined, there is no need to choose a priori.

• Type: Conference
• Year: 2007
• Where: FORMATS
• Authors: Víctor A. Braberman, Jorge Lucángeli Obes, Alfredo Olivero, Fernando Schapachnik
• Keywords: Case Studies, DBMs Represent Convex, Dierence Bound Matrices, FORMATS 2007