Issues in distributed timed model checking

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.