State space reduction of rewrite theories using invisible transitions

Azadeh Farzan, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. 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.

Original languageEnglish (US)
Title of host publicationAlgebraic Methodology and Software Technology - 11th International Conference, AMAST 2006
PublisherSpringer-Verlag Berlin Heidelberg
Pages142-157
Number of pages16
ISBN (Print)3540356339, 9783540356332
DOIs
StatePublished - Jan 1 2006
Event11th International Conference on Algebraic Methodology and Software Technology, AMAST 2006 - Kuressaare, Estonia
Duration: Jul 5 2006Jul 8 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4019 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Conference on Algebraic Methodology and Software Technology, AMAST 2006
CountryEstonia
CityKuressaare
Period7/5/067/8/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'State space reduction of rewrite theories using invisible transitions'. Together they form a unique fingerprint.

Cite this