Disjunctive Transition Relation Decomposition for Efficient Reachability Analysis

The applicability of disjunctive Transition Relation decompositions in the context of symbolic model checking is researched. An algorithm that generates such decompositions is proposed and evaluated on the VIS benchmarks. The obtained decompositions are well-balanced and the algorithm compares well with IWLS'95.