@techreport{SchuppanBiereETHZTr470,
  author={V. Schuppan and A. Biere},
  title={Shortest Counterexamples for Symbolic Model Checking of {LTL} with Past},
  institution={ETH Z\"urich, Computer Systems Institute},
  year={2005},
  month={01},
  type={Technical Reports},
  number={470},
  ee={ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/4xx/470.pdf},
}