CTL* as in https://en.wikipedia.org/wiki/CTL*, is a logic that combines CTL and LTL. I know that CTL* can express everything expressible in these two languages and more. My question is whether we can model the computation tree of each LTS with CTL*


1 Answer 1


First of all, for every transition system M, there indeed exists a CTL* formula Φ such that M ⊨ Φ holds, namely the CTL* formula "true".

What you may have wanted to express is the question if for every transition system M, there exists a CTL* formula Φ such that exactly the computation tree of M satisfies Φ. This is not the case. There are multiple reasons for this, and I will list two.

For the first, note that CTL* cannot distinguish between bisimulation-equivalent LTS. Hence, when computing a CTL* property characterizing an LTS, there will always be another bisimulation-equivalent-but-not-the-same-LTS that will also do.

Second, note that CTL* is not a counting logic. You cannot express "along all traces, in infinitely many even positions in a trace, p holds" in CTL*. This means that for a LTS having this property, we can't compute a CTL* property capturing this aspect.

  • $\begingroup$ Thanks for answer, I have edited my question to make sense now. Can you point to me resources that prove the 2 points you said and how would i go about getting concrete examples in each case. $\endgroup$
    – revision
    Commented May 3 at 11:30
  • 1
    $\begingroup$ @revision There is the paper "Counting LTL" which also includes a counting variant of CTL*. That would not make sense if CTL* can count already. For the bisimulation equivalence, the lecture videos by JP Katoen (youtube.com/watch?v=XNmazTIsOaw) may be helpful. Most likely this is proven in the Model checking textbook by him as well - Sorry, don't have a copy here. $\endgroup$
    – DCTLib
    Commented May 3 at 13:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.