Model Checking with Formula-Dependent Abstract Models
- 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).
Document Type: | Conference Object |
---|---|
Language: | English |
Author: | Alexander Asteroth, Christel Baier, Ulrich Aßmann |
Parent Title (English): | Berry, Comon et al. (Eds.): Computer Aided Verification. 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings |
First Page: | 155 |
Last Page: | 168 |
ISBN: | 978-3-540-42345-4 |
DOI: | https://doi.org/10.1007/3-540-44585-4_14 |
Date of first publication: | 2001/07/04 |
Dewey Decimal Classification (DDC): | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Entry in this database: | 2015/08/21 |