Model Checking with Formula-Dependent Abstract Models

Alexander AsterothAlexander Asteroth, Christel BaierChristel Baier, Ulrich AßmannUlrich Aßmann

DOI Link

Alexander Asteroth, Christel Baier, Ulrich Aßmann
Model Checking with Formula-Dependent Abstract Models
13th International Conference on Computer Aided Verification (CAV), volume 2102 of Lecture Notes in Computer Science, 155--168, 2001. Springer

Details
Bibtex

KurzfassungAbstract
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).
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-44585-4_14.

@inproceedings{ABA2001,
  author    = {Alexander Asteroth and Christel Baier and Ulrich A{\ss}mann},
  title     = {Model Checking with Formula-Dependent Abstract Models},
  booktitle = {13th International Conference on Computer Aided Verification
               (CAV)},
  series    = {Lecture Notes in Computer Science},
  volume    = {2102},
  publisher = {Springer},
  year      = {2001},
  pages     = {155--168},
  doi       = {10.1007/3-540-44585-4_14}
}