ZEUS: A Distributed Timed Model-Checker Based on KRONOS

In this work we present Zeus, a Distributed Model-Checker that evolves from the tool Kronos [8] and that currently can handle backwards computation of TCTLreachability properties [1] over timed-automata [2]. 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. Although some good results have been obtained, early experiments pinpointed the difficulties of getting speedups using a parallel asynchronous version. We also propose some paths to overcome those obstacles.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Víctor A. Braberman, Alfredo Olivero, Fernando Schapachnik
• Keywords: Architecture Centric Approach, Backwards Computation, Distributed Model-Checker, ENTCS 2002