Visualising CTL Witnesses and Counterexamples -- Extended Version
Arend Rensink

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
