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
$\begingroup$
$\endgroup$
2
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$– revisionCommented 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$– DCTLibCommented May 3 at 13:38