Open access
Date
2005Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
Shorter counterexamples are typically easier to understand. The length of a counterexample, as reported by a model checker, depends on both the algorithm used for state space exploration and the way the property is encoded. We provide necessary and sufficient criteria for a B¨uchi automaton to accept shortest counterexamples. We prove that B¨uchi automata constructed using the approach of Clarke, Grumberg, and Hamaguchi accept shortest counterexamples of future time LTL formulae, while an automaton generated with the algorithm of Gerth et al. (GPVW) may lead to unnecessary long counterexamples. Optimality is lost in the first case as soon as past time operators are included. Adapting a recently proposed encoding for bounded model checking of LTL with past, we construct a B¨uchi automaton that accepts shortest counterexamples for full LTL. We use our method of translating liveness into safety to find shortest counterexamples with a BDD-based symbolic model checker without modifying the model checker itself. Though our method involves a quadratic blowup of the state space, it outperforms SAT-based bounded model checking on a number of examples. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006775691Publication status
publishedJournal / series
Technical reportVolume
Publisher
ETH, Department of Computer ScienceOrganisational unit
02150 - Dep. Informatik / Dep. of Computer Science
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics