Dealing with practical limitations of distributed timed model checking for timed automata

Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Braberman, V., Olivero, A., Schapachnik, F.
Formato:	JOUR
Materias:	DBM Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Algorithms Control equipment Data structures Formal logic Program processors Topology Difference Bound Matrices (DBM) Automata theory
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_09259856_v29_n2_p197_Braberman
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_09259856_v29_n2_p197_Braberman
record_format	dspace
spelling	todo:paper_09259856_v29_n2_p197_Braberman2023-10-03T15:46:31Z Dealing with practical limitations of distributed timed model checking for timed automata Braberman, V. Olivero, A. Schapachnik, F. DBM Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Algorithms Control equipment Data structures Formal logic Program processors Topology Difference Bound Matrices (DBM) Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Automata theory Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better suited for on-the-fly construction of the model, the one known as backwards provides the basis for the verification of arbitrary formulae of the TCTL logic, and more importantly, for controller synthesis. Zeus is a distributed model checker for timed automata that uses the backwards algorithm. It works assigning each automata location to only one processor. This design choice seems the only reasonable way to deal with some complex operations involving many DBMs in order to avoid huge overheads due to distribution. This article explores the limitations of Zeus-like approaches for the distribution of timed model checkers. Our findings justify why close-to-linear speedups are so difficult -and sometimes impossible- to achieve in the general case. Nevertheless, we present mechanisms based on the way model checking is usually applied. Among others, these include model-topology-aware partitioning and on-the-fly workload redistribution. Combined, they have a positive impact on the speedups obtained. Fil:Braberman, V. 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. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_09259856_v29_n2_p197_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	DBM Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Algorithms Control equipment Data structures Formal logic Program processors Topology Difference Bound Matrices (DBM) Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Automata theory
spellingShingle	DBM Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Algorithms Control equipment Data structures Formal logic Program processors Topology Difference Bound Matrices (DBM) Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Automata theory Braberman, V. Olivero, A. Schapachnik, F. Dealing with practical limitations of distributed timed model checking for timed automata
topic_facet	DBM Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Algorithms Control equipment Data structures Formal logic Program processors Topology Difference Bound Matrices (DBM) Distributed timed model checking Kronos Load-balance Reachability Reconfiguration Redistribution Timed automata Zeus Automata theory
description	Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better suited for on-the-fly construction of the model, the one known as backwards provides the basis for the verification of arbitrary formulae of the TCTL logic, and more importantly, for controller synthesis. Zeus is a distributed model checker for timed automata that uses the backwards algorithm. It works assigning each automata location to only one processor. This design choice seems the only reasonable way to deal with some complex operations involving many DBMs in order to avoid huge overheads due to distribution. This article explores the limitations of Zeus-like approaches for the distribution of timed model checkers. Our findings justify why close-to-linear speedups are so difficult -and sometimes impossible- to achieve in the general case. Nevertheless, we present mechanisms based on the way model checking is usually applied. Among others, these include model-topology-aware partitioning and on-the-fly workload redistribution. Combined, they have a positive impact on the speedups obtained.
format	JOUR
author	Braberman, V. Olivero, A. Schapachnik, F.
author_facet	Braberman, V. Olivero, A. Schapachnik, F.
author_sort	Braberman, V.
title	Dealing with practical limitations of distributed timed model checking for timed automata
title_short	Dealing with practical limitations of distributed timed model checking for timed automata
title_full	Dealing with practical limitations of distributed timed model checking for timed automata
title_fullStr	Dealing with practical limitations of distributed timed model checking for timed automata
title_full_unstemmed	Dealing with practical limitations of distributed timed model checking for timed automata
title_sort	dealing with practical limitations of distributed timed model checking for timed automata
url	http://hdl.handle.net/20.500.12110/paper_09259856_v29_n2_p197_Braberman
work_keys_str_mv	AT brabermanv dealingwithpracticallimitationsofdistributedtimedmodelcheckingfortimedautomata AT oliveroa dealingwithpracticallimitationsofdistributedtimedmodelcheckingfortimedautomata AT schapachnikf dealingwithpracticallimitationsofdistributedtimedmodelcheckingfortimedautomata
_version_	1807323834188038144

Dealing with practical limitations of distributed timed model checking for timed automata

Ejemplares similares