Visualising CTL Witnesses and Counterexamples -- Extended Version
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.
Keywords
Cite
@article{arxiv.2604.20253,
title = {Visualising CTL Witnesses and Counterexamples -- Extended Version},
author = {Arend Rensink},
journal= {arXiv preprint arXiv:2604.20253},
year = {2026}
}
Comments
for associated software artefact, see https://doi.org/10.5281/zenodo.19169335