Efficient Symbolic Reachability of Networks of Transition Systems

Symbolic reachability analysis of networks of transition systems present special optimization opportunities that cannot be exploited by reachability analysis techniques of monolithic transition systems. These optimizations can potentially allow scaling of reachability analysis to much larger networks than can be handled using existing techniques. In this paper, we present a set of techniques for efficient approximate reachability analysis of large networks of transition systems, and analyze their relative precision and performance in BDD-based reachability analyzers. We use overlapping projections to represent the complete state space, and discuss optimizations in image computation operations that significantly limit the set of updations due to each asynchronous transition. The ideas presented in this paper have been implemented in a BDD-based symbolic reachability analyzer built on top of the public-domain tool …