Partial order (PO) reduction methods are widely employed to combat state explosion during model-checking. In this paper, we develop a partial order reduction algorithm for rule-based languages, such as Murphi[5] and Unity[3]. Our algorithm is based on the simple observation that for finite-state systems, the independence conditions can be encoded as boolean propositions, which can be checked by a SAT solver. We compare the results of this algorithm against a standard, static-analysis based algorithm, with favorable results.
Ritwik Bhattacharya, Steven M. German, Ganesh Gopa