Shortest Counterexamples for Symbolic Model Checking of LTL with Past

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 modifyin...

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Viktor Schuppan, Armin Biere
• Keywords: Algorithms, Model Checker, Shorter Counterexamples, Shortest Counterexamples, TACAS 2005