An Approach to State Space Reduction for Systems with Dynamic Process Creation

Automated verification of dynamic multi-threaded computing systems can be adversely affected by problems relating to dynamic process creation. We therefore investigate—in a general setting of labelled transition systems–a way of reducing the state spaces of multi-threaded systems. At the heart of our method is a state equivalence, which may produce a finite representation of an infinite state system while still allowing to validate the relevant behavioural proper-ties. We demonstrate the feasibility of the method through experiments involving the checking of the proposed state equivalence.