INVESTIGADORES
BRABERMAN Victor Adrian
artículos
Título:
"Hypervolume Approximation in Timed Automata Model Checking
Autor/es:
BRABERMAN; LUCANGELI; OLIVERO; SCHAPACHNIK
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer Verlag
Referencias:
Lugar: Berlin; Año: 2007 vol. 4763 p. 69 - 81
ISSN:
0302-9743
Resumen:
DBMs (Difference Bound Matrices) 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 first, 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 differs among the different case studies but, as they can be combined, there is no need to choose a priori.
