Dealing with Practical Limitations of Distributed Timed Model Checking for Timed Automata

VICTOR A. BRABERMAN; ALFREDO OLIVERO; FERNANDO SCHAPACHNIK

FORMAL METHODS IN SYSTEM DESIGN

Kluwer

Lugar: Amsterdan; Año: 2005 vol. 29 p. 197 - 214

0925-9856

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.