Visualising CTL Witnesses and Counterexamples -- Extended Version
This work addresses the challenge of making CTL model checking more accessible to users by providing clear visual evidence, though it is incremental as it builds on existing CTL concepts.
The paper tackles the problem of visualizing CTL witnesses and counterexamples for human comprehension by proposing a formal model of evidence, characterizing minimal evidence per temporal operator, and implementing a concrete visualization method.
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.