Partial tau-Confluence for Efficient State Space Generation; Software engineering rept

摘要

We extend the theory of partial order methods with a new notion of tau-confluence. Based on this new notion we define a reduced transition system, which is branching bisimilar to the original state space. We show that the new notion is preserved under various transformations. We present an algorithm which efficiently computes the reduced transition system from a symbolic representation.