Hypervolume approximation in timed automata model checking
Difference 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...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v4763LNCS_n_p69_Braberman |
| Aporte de: |
| Sumario: | Difference 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 first, requires more involved programming. Each of them saves verification 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. © Springer-Verlag Berlin Heidelberg 2007. |
|---|