In this work we present
Zeus, a distributed timed model checker that evolves from the TCTL model checker
Kronos [13] and that currently can handle backwards computation of reachability properties [2] over timed automata [3].
Zeus was developed following a software architecture-centric approach. Its conceptual architecture was conceived to be sufficiently modular to house several features such as a priori graph partitioning, synchronous and asynchronous computation, communication piggybacking, delayed messaging, and dead-time utilization.
Surprisingly enough, early experiments pinpointed the difficulties of getting speedups using asynchronous versions and showed interesting results on the synchronous counterpart, although being intuitively less attractive.
Keywords Timed systems - Distributed timed model checking - Timed automata - Kronos - Zeus