Next-preserving branching bisimulation

As an example for its application we show how this definition gives rise to an advanced slicing procedure that creates a formula-specific slice, which constitutes a reduced model of the system that can be used as a substitute when verifying this formula. The result is a novel procedure for generating slices that are next-preserving branching bisimilar to the original model for any formula. We can assure that each slice preserves the formula it corresponds to, which renders the overall verification process sound.