Alleviating State-space Explosion in Component-based Systems with Distributed, Parallel Reachability Analysis Algorithm

TL;DR

This paper presents a distributed, parallel reachability analysis algorithm that constructs a sum machine to mitigate state-space explosion in component-based systems, enabling efficient verification of global states.

Contribution

It introduces a novel sum machine composition based on partial-order semantics and a parallel, distributed algorithm for reachability analysis that avoids exponential complexity.

Findings

Sum machine reduces state-space explosion in CBS.

Parallel, distributed reachability algorithm improves efficiency.

Implementation demonstrates effective verification without exponential complexity.

Abstract

In this work, we alleviate the well-known State-Space Explosion (SSE) problem in Component Based Systems (CBS). We consider CBS that can be specified as a system of n Communicating Finite State Machines (CFSMs) interacting by rendezvous/handshake method. In order to avoid the SSE incurred by the traditional product machine composition of the given input CFSMs based on interleaving semantics, we construct a sum machine composition based on state-oriented partial-order semantics. The sum machine consists of a set of n unfolded CFSMs. By storing statically, just a small subset of global state vectors at synchronization points, called the synchronous environment vectors and generating the rest of the global-state vectors dynamically on need basis depending on the reachability to be verified, the sum machine alleviates the SSE of the product machine. We demonstrate the implementation of checking the reachability of global state vector from the checking of local reachabilities of the components of the given state vector, through a parallel, distributed algorithm. Parallel and distributed algorithms to generate the sum machine and verifying the reachability in it both without exponential complexity are the contributions of this work. Keywords: interleaving semantics, partial-order semantics, sum machine, product machine, synchronization points, synchronous environment state vectors, reachability.