2
$\begingroup$

I am wondering what exactly the difference between CTL and CTL* is. I know that CTL* is strictly more expressive than CTL, but it is not clear to me how the "restrictions" to CTL accomplish that. I.e., why do we have to alternate quantifiers and do not allow negation nor conjunction (no boolean logic)?

In the book I am reading "Principles of Model Checking" by Baier & Katoen, the abstract syntax for CTL simply enforces the aforementioned restrictions by construction.

I would appreciate some "intuition" behind this, e.g., why are the restrictions necessary and where could these restrictions be stretched.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

First, let's see a formula that's in CTL$^*$ but not in CTL: $EGFp$. That is, there exists a path with infinitely many $p$'s.

One intuition (and this is by no means a formal argument) is that the "closest" CTL formulas are $EGEFp$ and $EGAFp$, and neither of them capture the same notion.

The motivation behind defining this restriction of CTL$^*$ is that it still captures interesting properties, and it allows efficient model checking. The reason behind this efficiency is that CTL can be model-checked "bottom-up", and evaluating each path formula is easy, as these are simple formulas: just one temporal operator. If you allow arbitrary LTL within each path formula, you immediately get PSPACE hardness from LTL.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ The intuition you gave regarding the "closest" CTL formula is really insightful. Thank you very much. I started reading about the problem of PSPACE-completeness for LTL, thank you for the reference. $\endgroup$
    – marcluque
    Commented Mar 18, 2022 at 0:28
  • $\begingroup$ Please don't read too much into this intuition: there may well be cases where there is an equivalent CTL formula, but it doesn't look similar at all. $\endgroup$
    – Shaull
    Commented Mar 18, 2022 at 8:07
  • $\begingroup$ I agree, thank you. $\endgroup$
    – marcluque
    Commented Mar 18, 2022 at 9:52

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.