Skip to main content
Conference ProceedingsOPEN ACCESS

Model checking with formula-dependent abstract models

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2001) 2102 155-168
DOI: 10.1007/3-540-44585-4_14
5Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

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

Cite

CITATION STYLE

APA

Asteroth, A., Baier, C., & Aßmann, U. (2001). Model checking with formula-dependent abstract models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2102, pp. 155–168). Springer Verlag. https://doi.org/10.1007/3-540-44585-4_14

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free