Skip to main content

2001 | OriginalPaper | Buchkapitel

Abstraction-Based Model Checking Using Modal Transition Systems

verfasst von : Patrice Godefroid, Michael Huth, Radha Jagadeesan

Erschienen in: CONCUR 2001 — Concurrency Theory

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

We present a framework for automatic program abstraction that can be used for model checking any formula of the modal mu-calculus. Unlike traditional conservative abstractions which can only prove universal properties, our framework can both prove and disprove any formula including arbitrarily nested path quantifiers. We discuss algorithms for automatically generating an abstract Modal Transition System (MTS) by adapting existing predicate and cartesian abstraction techniques. We show that model checking arbitrary formulas using abstract MTSs can be done at the same computational cost as model checking universal formulas using conservative abstractions.

Metadaten
Titel
Abstraction-Based Model Checking Using Modal Transition Systems
verfasst von
Patrice Godefroid
Michael Huth
Radha Jagadeesan
Copyright-Jahr
2001
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-44685-0_29

Neuer Inhalt