A partial order approach to branching time logic model checking

Abstract

Partial order techniques enable reducing the size of the state graph 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 have been studied, implemented and demonstrated for assertional languages that model the executions of a program as computation sequences, in particular the logic LTL (linear temporal logic). The paper shows, for the first time, how this approach can be applied to languages that model the behavior 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) and process algebras such as CCS. Conditions on the subset of successors from each node to guarantee reduction that preserves CTL properties are given. Provided experimental results show that the reduction is substantial.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>