Behavior verification of large component systems suffers of state explosion in particular when components involve parallel activities. For behavior protocols, a method of component behavior specification, we present a method of state space size reduction based on symbolic manipulation with the specification done by applying a set of reduction rules.
A case study is presented showing that the specification size is often reduced to only a fraction of the original one.