Sciweavers

Share
FMSD
2006

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

11 years 12 months ago
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 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
Víctor A. Braberman, Alfredo Olivero, Ferna
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where FMSD
Authors Víctor A. Braberman, Alfredo Olivero, Fernando Schapachnik
Comments (0)
books