Automatic Abstraction Techniques for Propositional µ-calculus Model Checking

Abelardo Pardo and Gary D. Hachtel

International Conference on Computer Aided Verification (CAV'97), Haifa, Israel, June 1997

Abstract

An abstraction/refinement paradigm for the full propositional µ-calculus is presented. No distinction is made between universal or existential fragments. Necessary conditions for conservative verification are provided, along with a fully automatic symbolic model checking abstraction algorithm. The algorithm begins with conservative verification of an initial abstraction. If the conclusion is negative, it derives a ``goal set'' of states which require further resolution. It then successively refines, with respect to this goal set, the approximations made in the sub-formulas, until the given formula is verified or computational resources are exhausted.

Click here to download the compressed postscript version.

BibTeX Entry

@InCollection{Pardo97,
  author =       {A. Pardo and G. Hachtel},
  title =        {Automatic Abstraction Techniques for Propositional
                  $\mu$-calculus Model Checking},
  booktitle =    {9th Int. Conference on Computer Aided Verification (CAV'97)},
  publisher =    {Springer-Verlag},
  year =         1997,
  editor =       {O. Grumberg},
  month =        {June},
  pages =        {12-23},
  note =         {LNCS-1254}
}
Return to the home page