State Space Reduction Using Partial (tau)-Confluence. Software Engineering

摘要

We present an efficient algorithm to determine the maximal class of confluent tau-transitions in a labelled transition system. Confluent tau-transitions are inert with respect to branching bisimulation. This allows to use tau-priorisation, which means that in a state with a confluent outgoing tau-transition all other transitions can be removed, maintaining branching bisimulation. In combination with the removal of tau-loops, and the compression of tau-sequences this yields an efficient algorithm to reduce the size of large state spaces.