State Space Reduction of Rewrite Theories Using Invisible Transitions

Abstract. State space explosion is the hardest challenge to the effective application of model checking methods. We present a new technique for achieving drastic state space reductions that can be applied to a very wide range of concurrent systems, namely any system specified as a rewrite theory. Given a rewrite theory R = (, E, R) whose equational part (, E) specifies some state predicates P, we identify a subset S R of rewrite rules that are P-invisible, so that rewriting with S does not change the truth value of the predicates P. We then use S to construct a reduced rewrite theory R/S in which all states reachable by S-transitions become identified. We show that if R/S satisfies reasonable executability assumptions, then it is in fact stuttering bisimilar to R and therefore both satisfy the same CTL -X formulas. We can then use the typically much smaller R/S to verify such formulas. We show through several case studies that the reductions achievable this way can be huge in practice...

• Type: Conference
• Year: 2006
• Where: AMAST
• Authors: Azadeh Farzan, José Meseguer
• Keywords: AMAST 2006, Rewrite Theory, Rewrite Theory R/s, Software Engineering, State Space