Then, valid formulas are those that include: Quantifier + Temporal Operator
Examples:
AX p : In every path, the next state satisfies p
EX p : There is a path such that the next state satisfies p
Then the following model:
satisfies the property EX p (there is a path starting from the first state such that in the next state p holds), but it doesn't satisfy AXp (the path that continues below doesn't have p in the next state).
The temporal operators can be combined with boolean ones to build more complex formulas, for example
E(p U AX q) : there is a path where p holds until one state where every next state satisfies q.
Challenge:
1) for what CTL formula there isn't an LTL equivalent formula ?
2) for what LTL formula there isn't a CTL equivalent formula ?