Efficient computation and representation of large reachability sets for composed automata

We propose an approach that integrates and extends known techniques from different areas to handle and analyze a complex and large system described as a network of synchronized components. State spaces and transition graphs are first generated for single components. Then, we reduce the component state spaces by using a reachability-preserving equivalence relation. The reduced descriptions are used afterwards for reachability analysis. Reachability analysis is performed in an incremental way that exploits the component structure which defines the adjacency matrix of the transition graph of the complete system as a Kronecker product of small component adjacency matrices. This representation often achieves a significant reduction of the number of transition interleavings to be considered during reachability analysis. An acyclic graph is used to encode the set of reachable states. This representation is an extension of ordered binary decision diagrams and allows for a compact representation of huge sets of states. Furthermore, the full state space is easily obtained from the reduced set. The reduced or the full state space can be used in model-checking algorithms to derive detailed results about the behavior of the modeled system. The combination of the proposed techniques yields an approach suitable for extremely large state spaces, which are represented in a space-efficient way and generated and analyzed with low effort.