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

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, V., Obes, J.L., Olivero, A., Schapachnik, F.
Formato: SER
Materias:
Automata theory
Computer aided software engineering
Data structures
Verification
Difference Bound Matrices
Hypervolume approximation
Timed automata
Model checking
Acceso en línea: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 todo:paper_03029743_v4763LNCS_n_p69_Braberman
record_format dspace
spelling todo:paper_03029743_v4763LNCS_n_p69_Braberman2023-10-03T15:19:00Z Hypervolume approximation in timed automata model checking Braberman, V. Obes, J.L. Olivero, A. Schapachnik, F. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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.
Obes, J.L.
Olivero, A.
Schapachnik, F.
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.
format SER
author Braberman, V.
Obes, J.L.
Olivero, A.
Schapachnik, F.
author_facet Braberman, V.
Obes, J.L.
Olivero, A.
Schapachnik, F.
author_sort Braberman, V.
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
url http://hdl.handle.net/20.500.12110/paper_03029743_v4763LNCS_n_p69_Braberman
work_keys_str_mv AT brabermanv hypervolumeapproximationintimedautomatamodelchecking
AT obesjl hypervolumeapproximationintimedautomatamodelchecking
AT oliveroa hypervolumeapproximationintimedautomatamodelchecking
AT schapachnikf hypervolumeapproximationintimedautomatamodelchecking
_version_ 1807323828443938816

Ejemplares similares