Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Local Abstraction-Refinement for the mu-Calculus
verfasst von : Harald Fecher, Sharon Shoham
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Counterexample-guided abstraction refinement (CEGAR) is a key technique for the verification of computer programs. Grumberg et al. developed a CEGAR-based algorithm for the modal
μ
-calculus. There, every abstract state is split in a refinement step. In this paper, the work of Grumberg et al. is generalized by presenting a new CEGAR-based algorithm for the
μ
-calculus. It is based on a more expressive abstract model and applies refinement only locally (at a single abstract state), i.e., the
lazy abstraction
technique for safety properties is adapted to the
μ
-calculus. Furthermore, it separates refinement determination from the (3-valued based) model checking. Three different heuristics for refinement determination are presented and illustrated.