Local First Search - A New Paradigm for Partial Order Reductions.

Partial order reductions are an approved heuristic method to cope with the state explosion problem, i.e; the combinatory explosion due to the interleaving representation of a parallel system. The partial order reductions work by providing sufficient criteria for building only a part of the full transition system on which the verification algorithms still compute the correct result for verifying local properties. In this work, we present a new reduction method with a completely different justification and functioning: We show that under very realistic assumptions, local properties can be verified considering paths only corresponding to partial orders with very few maximal elements. Then we use this observation to derive our local first search algorithm. Our method can be understood as a hybrid between partial order reductions and the McMillan unfolding approach. Experiments justify the practicality of the method.