Anzeige
Erschienen in:
2001 | OriginalPaper | Buchkapitel
Model Checking with Formula-Dependent Abstract Models
verfasst von : Alexander Asteroth, Christel Baier, Ulrich A*Bmann
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
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
We present a model checking algorithm for ∀CTL (and full CTL) which uses an iterative abstraction refinement strategy.It terminates at least for all transition systems M that have a finite simulation or bisimulation quotient. In contrast to other abstraction refinement algorithms, we always work with abstract models whose sizes depend only on the length of the formula θ (but not on the size of the system, which might be infinite).