A Partial Order Approach to Branching Time Logic Model Checking.

Partial order techniques enable reducing the size of the state space used for model checking, thus alleviating the state space explosion problem. These reductions are based on selecting a subset of the enabled operations from each program state. So far, these methods were being studied, implemented and demonstrated for languages that model the executions of a program as interleaving sequences, i.e., linear assertional languages, in particular the logic LTL. The present paper shows, for the first time, how this approach can be applied to languages that model the behaviour of a program as a tree. We study here partial order reductions for branching temporal logics, e.g., the logics CTL and CTL (all logics with the next-time operator removed). We provide a condition on the subset of successors from each node to guarantee correct reductions. We show by means of counter examples that this is a tight bound, not only for the logic CTL, but even for a very restricted subset of CTL, namely ACTL (which allows no existential quantification).