Zeus: A Distributed Model-Checker Based on Kronos Fernando Schapachnik, Víctor Braberman, and Alfredo Olivero
In this work we present Zeus, a Distributed Model-Checker that evolves from
the tool Kronos and that currently can handle backwards computation of
TCTL-reachability properties over timed-automata.
Zeus was developed following a software architecture centric approach. It introduces some interesting features such as a priori graph partitioning, a sophisticated machinery to reach optimum performance (communication piggybacking and delayed messaging) and dead-time utilization, where every processor uses time intervals of inactivity to perform auxiliary, time-consuming tasks that will later speed up the rest of the computation. |