TY - CHAP U1 - Konferenzveröffentlichung A1 - Asteroth, Alexander A1 - Baier, Christel A1 - Aßmann, Ulrich T1 - Model Checking with Formula-Dependent Abstract Models T2 - Berry, Comon et al. (Eds.): Computer Aided Verification. 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings N2 - 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). Y1 - 2001 SN - 978-3-540-42345-4 SB - 978-3-540-42345-4 U6 - https://doi.org/10.1007/3-540-44585-4_14 DO - https://doi.org/10.1007/3-540-44585-4_14 SP - 155 EP - 168 ER -