Paper Details

A Performance Study of Distributed Timed Automata Reachability Analysis
Gerd Behrmann

We experimentally evaluate a distributed reachability algorithm for timed automata on a Linux Beowulf cluster. It is discovered that the algorithm suffers from load balancing problems and a high communication overhead. The load balancing problems are caused by inclusion checking performed between symbolic states unique to the timed automaton reachability algorithm. We propose adding a proportional load balancing controller on top of the algorithm. We evaluate various approaches to reduce communication overhead by increasing locality and reducing the number of messages. Both approaches increase performance but can make load balancing harder and has unwanted side effects that result in an increased workload.