Visualising CTL Witnesses and Counterexamples -- Extended Version
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910156968689664 |
|---|---|
| author | Rensink, Arend |
| author_facet | Rensink, Arend |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_20253 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Visualising CTL Witnesses and Counterexamples -- Extended Version Rensink, Arend Logic in Computer Science Formal Languages and Automata Theory F.3.1 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. |
| title | Visualising CTL Witnesses and Counterexamples -- Extended Version |
| topic | Logic in Computer Science Formal Languages and Automata Theory F.3.1 |
| url | https://arxiv.org/abs/2604.20253 |