Paper Details

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.