# Difference between CTL and CTL*

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.

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.