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