Proof-like counter-examples

Abstract

Counter-examples explain why a desired temporal logic property fails to hold, and as such considered to be the most useful form of output from model-checkers. Reported explanations are typically short and described in terms of states and transitions of the model; as a result, they can be effectively used for debugging. However, counter-examples are not available for every CTL property and are often inadequate for explaining exactly what the answer means [CLJV02]. In this paper, we present the approach of annotating counter-examples with additional proof steps. This approach does not sacrifice any of the advantages of traditional counter-examples, yet allows the user to understand and navigate through the counter-example better. We describe our proof system, discuss how to connect it with counter-example generators, and present KEGVis - a tool for visualizing and browsing the annotated counter-examples. © Springer-Verlag Berlin Heidelberg 2003.