pith. sign in

arxiv: 2604.20253 · v1 · submitted 2026-04-22 · 💻 cs.LO · cs.FL

Visualising CTL Witnesses and Counterexamples -- Extended Version

Arend Rensink This is my paper

Pith reviewed 2026-05-09 23:43 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords CTLwitnessescounterexamplesvisualizationevidencetemporal logicminimal evidenceexplicit state models
0
0 comments X

The pith

CTL evidence can be modeled minimally and visualized to explain property satisfaction or violation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a notion of evidence for CTL that doubles as both witness and counterexample. It gives a formal model for this evidence along with the smallest evidence needed for each temporal operator. A visualization method is then proposed and implemented to make this evidence understandable to people. If this works, it would let users see directly the reasons behind model checking results for branching-time properties.

Core claim

We introduce a formal model of evidence for CTL properties on explicit-state models. This evidence serves for both satisfied properties and their violations. Minimal evidence is characterized for every temporal operator, leading to a concrete visualization proposal that has been implemented.

What carries the argument

The formal model of evidence with its per-operator minimal characterizations, which generates the visual diagrams.

If this is right

  • Evidence structures can represent both positive and negative outcomes uniformly.
  • Minimal evidence focuses attention on the relevant parts of the state space.
  • Visualizations provide concrete diagrams rather than abstract traces or trees.
  • The method applies to all CTL operators through their individual characterizations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar evidence models could be developed for related logics like LTL or others.
  • The approach might reduce the need for manual inspection of large state spaces.
  • Integration with existing model checkers could make results more interpretable without changing the checking process.

Load-bearing premise

Visual representations of the minimal evidence will actually help humans comprehend the CTL properties better.

What would settle it

Performing a user experiment that measures whether people understand CTL properties better when shown the visualizations compared to text or standard counterexamples.

Figures

Figures reproduced from arXiv: 2604.20253 by Arend Rensink.

Figure 1
Figure 1. Figure 1: Game board (L = loss, W = win) [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Kripke model of the game state space (cf. Example 3). [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Sample minimal evidence for temporal formulas. Dotted nodes are open; dashed [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Model checking result and minimal witness for [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Locally closed and natural evidence for E ! d1 U win (compare Fig. 4b). In the next proposition, we use M|s (for s ∈ S) to denote the restriction of M to the states reachable from s. Proposition 21 (combined evidence always exists). Let F ∈ ↓F and let M ∈ M(F) be sound. For every φ ∈ FO there exists combined evidence Eφ ⊑ M. If, moreover, φ ∈ {EU, EG} × F <ω, then there exists combined [natural] evidence E… view at source ↗
Figure 6
Figure 6. Figure 6: Combined natural evidence for the temporal operators of [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper proposes a formal model of evidence for CTL properties on explicit-state models, serving as both witnesses for satisfied properties and counterexamples for violated ones. It characterises minimal evidence per temporal operator, provides proofs for all results in this extended version, and presents a concrete implemented visualisation proposal whose main aim is improved human comprehension of CTL properties.

Significance. The formal model and per-operator minimality characterisations, backed by complete proofs, constitute a solid contribution to representing and reasoning about CTL evidence. If the visualisation proposal is adopted, it could help close the gap between LTL's intuitive traces and CTL's more complex branching structures, aiding debugging and education. The implemented nature of the proposal is a concrete strength.

major comments (1)
  1. [Abstract and §1] Abstract and §1: the main aim is stated as improving human comprehension via visualisation, yet the manuscript contains no user studies, controlled experiments, or quantitative metrics evaluating whether the proposed visuals actually aid understanding; this leaves the central practical claim resting on untested design choices rather than evidence.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and the recommendation for minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract and §1] Abstract and §1: the main aim is stated as improving human comprehension via visualisation, yet the manuscript contains no user studies, controlled experiments, or quantitative metrics evaluating whether the proposed visuals actually aid understanding; this leaves the central practical claim resting on untested design choices rather than evidence.

    Authors: We agree that the manuscript contains no user studies, controlled experiments or quantitative metrics assessing whether the proposed visualisation improves human comprehension of CTL properties. The primary contributions of the work are the formal model of evidence (serving as both witnesses and counterexamples), the per-operator minimality characterisations, and the complete proofs supplied in this extended version. The visualisation scheme is presented as a concrete, implemented proposal whose design is motivated by the formal evidence model and by the contrast with linear LTL traces. We do not claim to have demonstrated improved comprehension empirically; the stated aim is therefore aspirational rather than proven. In the revised manuscript we will add a short dedicated paragraph in §1 (and a corresponding remark in the conclusion) that explicitly acknowledges the absence of empirical validation, summarises the design rationale, and identifies user studies as future work. revision: yes

Circularity Check

0 steps flagged

No circularity: new formal definitions and proofs are self-contained

full rationale

The paper introduces a formal model of evidence for CTL properties on explicit-state models, provides a characterisation of minimal evidence per temporal operator (with proofs in the extended version), and proposes a concrete visualisation. These are definitional contributions and proven results rather than numerical predictions, fitted parameters, or derivations that reduce to inputs by construction. No self-citations appear load-bearing, no ansatzes are smuggled, and no renaming of known results occurs. The central claims rest on explicit definitions and formal proofs, making the derivation chain independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper rests on standard definitions of CTL semantics and explicit-state transition systems. No free parameters are introduced. The new 'evidence' objects are defined rather than postulated as physical entities.

axioms (1)
  • standard math Standard CTL semantics on Kripke structures
    Invoked throughout the formal model of evidence.
invented entities (1)
  • Evidence structure for CTL no independent evidence
    purpose: To serve as witness or counterexample
    Defined formally in the paper; no independent empirical evidence supplied.

pith-pipeline@v0.9.0 · 5404 in / 1163 out tokens · 26057 ms · 2026-05-09T23:43:59.788533+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages

  1. [1]

    Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: On ACTL formulas having linear counterexamples. J. Comput. Syst. Sci.62(3), 463–515 (2001).https://doi.org/ 10.1006/JCSS.2000.1734

    work page doi:10.1006/jcss.2000.1734 2001

  2. [2]

    Busard, S.: Symbolic Model Checking of Multi-Modal logics: Uniform Strategies andRichExplanations.Ph.D.thesis,CatholicUniversityofLouvain(2017),https: //hdl.handle.net/2078.1/186372

    work page 2017

  3. [3]

    Chechik, M., Gurfinkel, A.: A framework for counterexample generation and ex- ploration. Int. J. Softw. Tools Technol. Transf.9(5-6), 429–445 (2007).https: //doi.org/10.1007/S10009-007-0047-9

    work page doi:10.1007/s10009-007-0047-9 2007

  4. [4]

    Clarke and E

    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skele- tons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Pro- grams. Lecture Notes in Computer Science, vol. 131, pp. 52–71. Springer (1981). https://doi.org/10.1007/BFB0025774

    work page doi:10.1007/bfb0025774 1981

  5. [5]

    In: Preas, B

    Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Preas, B. (ed.) Proceedings of the 32st Conference on Design Automation. pp. 427–432. ACM Press (1995).https://doi.org/10.1145/217474.217565

    work page doi:10.1145/217474.217565 1995

  6. [6]

    In: LICS 2002, pp

    Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model check- ing. In: 17th IEEE Symposium on Logic in Computer Science (LICS). pp. 19–29. IEEE Computer Society (2002).https://doi.org/10.1109/LICS.2002.1029814

    work page doi:10.1109/lics.2002.1029814 2002

  7. [7]

    In: Kreutzer, S.(ed.)24thEACSLAnnualConferenceonComputerScienceLogic(CSL).LIPIcs, vol

    Cranen, S., Luttik, B., Willemse, T.A.C.: Evidence for fixpoint logic. In: Kreutzer, S.(ed.)24thEACSLAnnualConferenceonComputerScienceLogic(CSL).LIPIcs, vol. 41, pp. 78–93. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015). https://doi.org/10.4230/LIPICS.CSL.2015.78

    work page doi:10.4230/lipics.csl.2015.78 2015

  8. [8]

    Informatica (Slovenia) 42(2) (2018),http://www.informatica.si/index.php/informatica/article/ view/1442

    Debbi, H.: Counterexamples in model checking - A survey. Informatica (Slovenia) 42(2) (2018),http://www.informatica.si/index.php/informatica/article/ view/1442

    work page 2018

  9. [9]

    In: de Bakker, J.W., van Leeuwen, J

    Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel pro- grams using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Lan- guages and Programming (ICALP). Lecture Notes in Computer Science, vol. 85, pp. 169–181. Springer (1980).https://doi.org/10.1007/3-540-10003-2_69

    work page doi:10.1007/3-540-10003-2_69 1980

  10. [10]

    Allen and Halpern, Joseph Y

    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” revisited: on branch- ing versus linear time temporal logic. J. ACM33(1), 151–178 (1986).https: //doi.org/10.1145/4904.4999

    work page doi:10.1145/4904.4999 1986

  11. [11]

    In: Beyer, D., Huisman, M

    Jiang, C., Ciardo, G.: Generation of minimum tree-like witnesses for existen- tial CTL. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS), Part I. Lecture Notes in Computer Science, vol. 10805, pp. 328–343. Springer (2018).https://doi.org/10.1007/ 978-3-319-89960-2_18

    work page 2018

  12. [12]

    Kaleeswaran, A.P., Nordmann, A., Vogel, T., Grunske, L.: A systematic literature review on counterexample explanation. Inf. Softw. Technol.145(2022).https: //doi.org/10.1016/J.INFSOF.2021.106800

    work page doi:10.1016/j.infsof.2021.106800 2022

  13. [13]

    In: Nielsen, M., Schmidt, E.M

    Kozen, D.: Results on the propositionalµ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages and Programming (ICALP). Lecture Notes in Com- puter Science, vol. 140, pp. 348–359. Springer (1982).https://doi.org/10.1007/ BFB0012782

    work page 1982

  14. [14]

    Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci.27, 333– 354 (1983).https://doi.org/10.1016/0304-3975(82)90125-6

    work page doi:10.1016/0304-3975(82)90125-6 1983

  15. [15]

    Acta Philosophica Fennica 16, 83–94 (1963)

    Kripke, S.: Semantical considerations on modal logic. Acta Philosophica Fennica 16, 83–94 (1963)

    work page 1963

  16. [16]

    In: 32nd International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE)

    Martinelli, F., Mercaldo, F., Santone, A.: On the adoption of counterexample for classification task explainability. In: 32nd International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). pp. 140–

    work page

  17. [17]

    IEEE (2024).https://doi.org/10.1109/WETICE64632.2024.00033

    work page doi:10.1109/wetice64632.2024.00033 2024

  18. [18]

    18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages =

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foun- dations of Computer Science (FoCS). pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32

    work page doi:10.1109/sfcs.1977.32 1977

  19. [19]

    librosa/librosa: 0.6.3,

    Rensink, A.: CTLViz: Visualising CTL witnesses and counterexamples. Soft- ware artefact; published at Zenodo (2026).https://doi.org/10.5281/zenodo. 19169335

    work page doi:10.5281/zenodo 2026

  20. [20]

    In: Ciancia, V., Hartmanns, A

    Rensink, A.: Visualising CTL witnesses and counterexamples. In: Ciancia, V., Hartmanns, A. (eds.) 32nd International Symposium on Model Checking Software (SPIN). Lecture Notes in Computer Science, Springer (2026)

    work page 2026

  21. [21]

    SRI International (2003),http://www.csl.sri.com/people/shankar/wmc.pdf

    Shankar, N., Sorea, M.: Counterexample-driven model checking. SRI International (2003),http://www.csl.sri.com/people/shankar/wmc.pdf

    work page 2003

  22. [22]

    In: Gurfinkel, A., Heule, M

    Stramaglia, A., Keiren, J.J.A., Laveaux, M., Willemse, T.A.C.: Efficient evidence generation for modalµ-calculus model checking. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I. Lecture Notes in Computer Science, vol. 15696, pp. 191–210. Springer (2025). https://doi.org/10.1007/978-3-03...

    work page doi:10.1007/978-3-031-90643-5_10 2025

  23. [23]

    linear time: Final showdown

    Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS).LectureNotesinComputerScience,vol.2031,pp.1–22.Springer(2001). https://doi.org/10.1007/3-540-45319-9_1

    work page doi:10.1007/3-540-45319-9_1 2031

  24. [24]

    In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, A

    Weitl, F., Nakajima, S., Freitag, B.: Structured counterexamples for the temporal description logic ALCCTL. In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, A. (eds.) 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM). pp. 232–243. IEEE Computer Society (2010).https://doi. org/10.1109/SEFM.2010.36

    work page doi:10.1109/sefm.2010.36 2010

  25. [25]

    In: Benzmüller, C., Otten, J

    Wesselink, W., Willemse, T.A.C.: Evidence extraction from parameterised boolean equation systems. In: Benzmüller, C., Otten, J. (eds.) Proceedings of the 3rd Inter- national Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL). CEUR Workshop Proceedings, vol. 2095, pp. 86–100. CEUR-WS.org (2018),https://ceur-ws.org/Vol-2095/paper6.pd...

    work page 2095

  26. [26]

    For allρ∈maxpth 1(s), there is aρ ′ ∈maxpth 2(s)such thatρ⪯ρ ′, and ρ=ρ ′ ifρends inC 1

    work page

  27. [27]

    The following states that, for full models, precisely one ofwtsandctralways holds (for any state and formula)

    For allρ∈maxpth 2(s), there is aρ ′ ∈maxpth 1(s)such thatρ ′ ⪯ρ, and ρ′ =ρifρ ′ ends inC 1. The following states that, for full models, precisely one ofwtsandctralways holds (for any state and formula). Lemma 24 (wtsandctrare complementary in full models.).LetF∈ ↓F and letM∈M(F)be full. For alls∈Sandφ∈F O, exactly one ofwts(s, φ) andctr(s, φ)holds. Proof....

    work page

  28. [28]

    It follows thatMis a witness for (s, φ)

    Ifwts M(s, φ)holds, then (due to Lemma 25) alsowts N(s, φ)holds, hence (due to the observation above)s|=N φ. It follows thatMis a witness for (s, φ)

    work page

  29. [29]

    It follows thatMis a counterexample for (s, φ).⊓ ⊔ Proposition 12 (unconstrained formula sets).LetF∈ ↓Fsuch that the only operators inFare!,+andEU, and letG⊆Fbe non-empty

    Ifctr M(s, φ)holds, then (due to Lemma 25) alsoctrN(s, φ)holds, hence (due to the observation above)s̸|=N φ. It follows thatMis a counterexample for (s, φ).⊓ ⊔ Proposition 12 (unconstrained formula sets).LetF∈ ↓Fsuch that the only operators inFare!,+andEU, and letG⊆Fbe non-empty. If all propo- sitions occurring inGare distinct, thenGis unconstrained. Proo...

    work page

  30. [30]

    IfMis a witness for(s, φ), thenwts(s, φ)holds

    work page

  31. [31]

    Proof.Letb∈Bsuch thatb=1when we are proving Clause 1 andφdoes not equal!ψor we are proving Clause 2 andφequals!ψ, andb=0otherwise, and let ¯bbe the complement ofb

    IfMis a counterexample for(s, φ), thenctr(s, φ)holds. Proof.Letb∈Bsuch thatb=1when we are proving Clause 1 andφdoes not equal!ψor we are proving Clause 2 andφequals!ψ, andb=0otherwise, and let ¯bbe the complement ofb. For alls∈S\C, letˆs /∈Sbe a fresh state. We define ˆS=S∪ {ˆs|s∈S\C} ˆR=R∪ {(s,ˆs)|s∈S\C} ˆL=L∪ {((s, ψ)7→ ¯b)|s∈ ˆS, ψ∈chld(φ),(s, ψ)/∈domL...

    work page

  32. [32]

    Lemma 24 then implies thatwts′(s, φ)holds

    SinceMis a witness for(s, φ), we haves|= M ′ φ, hence (due to Theorem 8) ctr′(s, φ)cannot hold. Lemma 24 then implies thatwts′(s, φ)holds. We prove by case distinction onφthatwts(s, φ)then also holds. –φ=1.wts(s, φ)holds by definition. –φ= !ψ.wts(s, φ)holds due tos∈S ′|ψ,0 =S| ψ,0. –φ=ψ 1 +ψ 2.wts(s, φ)holds due tos∈S ′|ψ1,1 ∪S ′|ψ2,1 =S| ψ1,1 ∪S| ψ2,1. –...

    work page

  33. [33]

    Lemma 24 then implies thatctr ′(s, φ) holds

    SinceMis a counterexample for(s, φ), we haves̸|= M ′ φ, hence (due to Theorem 8)wts ′(s, φ)cannot hold. Lemma 24 then implies thatctr ′(s, φ) holds. We prove by case distinction onφthatctr(s, φ)then also holds. –φ=1. Contradiction (ctr ′(s, φ)cannot hold). –φ= !ψ.ctr(s, φ)holds due tos∈S ′|ψ,1 =S| ψ,1. –φ=ψ 1 +ψ 2.ctr(s, φ)holds due tos∈S ′|ψ1,0 ∩S ′|ψ2,0...

    work page

  34. [34]

    first kind

    By a case distinction onφ. –φ=1.wts M(s, φ)holds always, andMis the smallest model that in- cludessso there does not exist anyN⊑M. –φ= !ψ.wts M(s, φ)clearly holds, and the onlyN<MhasL N =∅, hencewts N(s, φ)does not hold. –φ=ψ 1 +ψ 2.wts M(s, φ)clearly holds, and the onlyN<MhasL N =∅, hencewts N(s, φ)does not hold. –φ=EXψ.succ M(s) ={s ′}ands ′ ∈S M |ψ,1 s...

    work page

  35. [35]

    By a case distinction onφ. –φ=1. Contradiction. –φ= !ψ.ctr M(s, φ)clearly holds, and the onlyN<MhasL N =∅, hencectr N(s, φ)does not hold. –φ=ψ 1 +ψ 2.ctr M(s, φ)clearly holds, and ifN<Mthen|L N |= 1, hencectr N(s, φ)does not hold. –φ=EXψ.s∈C M andsucc(s)⊆S M |ψ,0, soctr M(s, φ)holds. IfN<·M thenS M =S N (otherwiseR M =R N could not hold), so eitherCN =∅ (...

    work page