@article{DFP2009,
  title = {Directed model checking with distance-preserving abstractions},
  author = {Klaus Dr{\"a}ger and Bernd Finkbeiner and  and Andreas Podelski},
  journal = {International Journal on Software Tools for Technology Transfer {(STTT})},
  publisher = {Springer Berlin / Heidelberg},
  issn = {1433-2779 (Print) 1433-2787 (Online)},
  url = {http://www.springerlink.com/content/382404j55137h3h8},
  number = {1},
  pages = {27--37},
  volume = {11},
  doi = {10.1007/s10009-008-0092-z},
  year = {2009},
  month = {February},
  subproject={R3},
  access={restricted},
  bibtex={draeger.sttt08.bib},
  pdf={draeger.sttt08.pdf},
  abstract={In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a distance-preserving abstraction for concurrent systems that allows one to compute an interesting estimate of the error distance without hitting the state explosion problem. Our experiments show a dramatic reduction both in the number of states explored by the model checker and in the total runtime. },
}