TY - GEN

T1 - State space reduction of rewrite theories using invisible transitions

AU - Farzan, Azadeh

AU - Meseguer, José

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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. Furthermore, we also present a generalization of our construction that instead uses a stuttering simulation and can be applied to an even broader class of systems.

AB - 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. Furthermore, we also present a generalization of our construction that instead uses a stuttering simulation and can be applied to an even broader class of systems.

UR - http://www.scopus.com/inward/record.url?scp=33746239698&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33746239698&partnerID=8YFLogxK

U2 - 10.1007/11784180_13

DO - 10.1007/11784180_13

M3 - Conference contribution

AN - SCOPUS:33746239698

SN - 3540356339

SN - 9783540356332

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 142

EP - 157

BT - Algebraic Methodology and Software Technology - 11th International Conference, AMAST 2006

PB - Springer

T2 - 11th International Conference on Algebraic Methodology and Software Technology, AMAST 2006

Y2 - 5 July 2006 through 8 July 2006

ER -