Symbolic Partial Order Reduction for Rule Based Transition Systems

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.

• Type: Conference
• Year: 2005
• Where: CHARME
• Authors: Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan
• Keywords: CHARME 2005, Hardware, Order Reduction Algorithm, Partial Order, Static-analysis Based Algorithm