State Space Reduction of Rewrite Theories Using Invisible Transitions

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

$\mathcal{R}=(\Sigma,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

$\mathcal{R}/S$

in which all states reachable by

S

-transitions become identified. We show that if

$\mathcal{R}/S$

satisfies reasonable executability assumptions, then it is in fact stuttering bisimilar to

$\mathcal{R}$

and therefore both satisfy the same

${\it CTL}^{\rm \ast}_{\rm -{\it X}}$

formulas. We can then use the typically much smaller

$\mathcal{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.