  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.
