In recent years many techniques have been developed for automatically verifying concurrent systems and most of them are based on a representation of the concurrent system by means of a finite state transition system. State explosion is one of the most serious problems of this approach: in fact often the prohibitive number of states renders the verification inefficient and, in some cases, impossible.
We propose an approach to the reduction of the state space of the transition system corresponding to a CCS process, which takes into account the deadlock freeness property. The reduced transition system is generated by means of a non-standard operational semantics containing a set of rules which are an abstraction, preserving deadlock freeness, of the inference rules of the standard semantics.