Speculative Image Computation for Distributed Symbolic Reachability Analysis

The Saturation-style fixpoint iteration strategy for symbolic reachability analysis is particularly effective for globally asynchronous locally synchronous discrete-state systems. However, its inherently sequential nature makes it difficult to parallelize Saturation on a network workstations (NOW). We then propose the idea of using idle workstation time to perform speculative image computations. Since an unrestrained prediction may make excessive use of computational resources, we introduce a history-based approach to dynamically recognize image computation (event firing) patterns and explore only firings that conform to these patterns. In addition, we employ an implicit encoding for the patterns, so that the actual image computation history can be efficiently preserved. Experiments not only show that image speculation works on a realistic model, but also indicate that the use of an implicit encoding together with two heuristics results in a better informed speculation.