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íctor Adrián, Schapachnik, Fernando Pablo
Publicado:	2006
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:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09259856_v29_n2_p197_Braberman 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	paper:paper_09259856_v29_n2_p197_Braberman
record_format	dspace
spelling	paper:paper_09259856_v29_n2_p197_Braberman2023-06-08T15:51:31Z Dealing with practical limitations of distributed timed model checking for timed automata Braberman, Víctor Adrián Schapachnik, Fernando Pablo 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. 2006 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09259856_v29_n2_p197_Braberman 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íctor Adrián Schapachnik, Fernando Pablo 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.
author	Braberman, Víctor Adrián Schapachnik, Fernando Pablo
author_facet	Braberman, Víctor Adrián Schapachnik, Fernando Pablo
author_sort	Braberman, Víctor Adrián
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
publishDate	2006
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09259856_v29_n2_p197_Braberman http://hdl.handle.net/20.500.12110/paper_09259856_v29_n2_p197_Braberman
work_keys_str_mv	AT brabermanvictoradrian dealingwithpracticallimitationsofdistributedtimedmodelcheckingfortimedautomata AT schapachnikfernandopablo dealingwithpracticallimitationsofdistributedtimedmodelcheckingfortimedautomata
_version_	1768544232685961216

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

Ejemplares similares