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...

Descripción completa

Detalles Bibliográficos
Autores principales:	Braberman, Víctor Adrián, Lucángeli Obes, Jorge, Schapachnik, Fernando Pablo
Publicado:	2007
Materias:	Automata theory Computer aided software engineering Data structures Verification Difference Bound Matrices Hypervolume approximation Timed automata Model checking
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v4763LNCS_n_p69_Braberman
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_03029743_v4763LNCS_n_p69_Braberman
record_format	dspace
spelling	paper:paper_03029743_v4763LNCS_n_p69_Braberman2023-06-08T15:28:26Z Hypervolume approximation in timed automata model checking Braberman, Víctor Adrián Lucángeli Obes, Jorge Schapachnik, Fernando Pablo Automata theory Computer aided software engineering Data structures Verification Difference Bound Matrices Hypervolume approximation 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 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. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Obes, J.L. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Schapachnik, F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2007 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v4763LNCS_n_p69_Braberman
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Automata theory Computer aided software engineering Data structures Verification Difference Bound Matrices Hypervolume approximation Timed automata Model checking
spellingShingle	Automata theory Computer aided software engineering Data structures Verification Difference Bound Matrices Hypervolume approximation Timed automata Model checking Braberman, Víctor Adrián Lucángeli Obes, Jorge Schapachnik, Fernando Pablo Hypervolume approximation in timed automata model checking
topic_facet	Automata theory Computer aided software engineering Data structures Verification Difference Bound Matrices Hypervolume approximation Timed automata Model checking
description	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.
author	Braberman, Víctor Adrián Lucángeli Obes, Jorge Schapachnik, Fernando Pablo
author_facet	Braberman, Víctor Adrián Lucángeli Obes, Jorge Schapachnik, Fernando Pablo
author_sort	Braberman, Víctor Adrián
title	Hypervolume approximation in timed automata model checking
title_short	Hypervolume approximation in timed automata model checking
title_full	Hypervolume approximation in timed automata model checking
title_fullStr	Hypervolume approximation in timed automata model checking
title_full_unstemmed	Hypervolume approximation in timed automata model checking
title_sort	hypervolume approximation in timed automata model checking
publishDate	2007
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v4763LNCS_n_p69_Braberman
work_keys_str_mv	AT brabermanvictoradrian hypervolumeapproximationintimedautomatamodelchecking AT lucangeliobesjorge hypervolumeapproximationintimedautomatamodelchecking AT schapachnikfernandopablo hypervolumeapproximationintimedautomatamodelchecking
_version_	1768545690592477184

Hypervolume approximation in timed automata model checking

Ejemplares similares