Visualising CTL Witnesses and Counterexamples -- Extended Version

TL;DR

This paper introduces a formal model and visualization method for CTL witnesses and counterexamples on explicit-state models, enhancing human comprehension of model checking results.

Contribution

It proposes a novel notion of evidence for CTL properties, including a formal model, minimal evidence characterization, and a visualization approach.

Findings

Formal model of evidence for CTL properties

Characterization of minimal evidence per operator

Implemented visualization method for evidence

Abstract

One of the advantages of LTL over CTL is that the notion of a counterexample is easy to grasp, visualise and process: it is a trace that violates the property at hand. In this paper we propose a notion of evidence for CTL properties on explicit-state models -- which equally serves as witness for satisfied properties and counterexample for violated ones -- and how to visualise it, with the main aim of (human) comprehension. The main contribution consists of a formal model of evidence, a characterisation of minimal evidence per temporal operator, and a concrete, implemented proposal for its visualisation. This is the extended version of a paper published in SPIN 2026, containing the proofs of all results.