CTL and LTL restrictions

Question

I am a bit confused about the restrictions in CTL and LTL formulas, i know in CTL a path quantifier must always occur before a temporal operator, is there any other restriction other than that for CTL ?

For LTL it says no path quantifier, but this formula AG(a ∧ ¬b) is valid in LTL and A is a path quantifier.

Can you please give me examples and mention the restrictions of CTL and LTL

Answer 1

Yes, in CTL, temporal operators and path quantifiers always occur in pairs, i.e. EX, EG, EF, E[. SU .], E[. WU .],E[. SB .], E[. WB .], AX, AG, AF, A[. SU .], A[. WU .],A[. SB .], A[. WB .]. That is the restriction for a CTL* formula to become a CTL formula.

Concerning LTL, we consider formulas of the form A phi where phi does not contain any path quantifier. Hence, AG(a ∧ ¬b) is a LTL formula since there is no path quantifier in a ∧ ¬b.

However, AG(a ∧ ¬b) is  not valid: Validity means that the formula should hold on every Kripke structure. 

There is not much more to say about the syntactical restrictions of CTL and LTL. That is the simple part. It is much more difficult to check whether a given formula could be rewritten to an equivalent CTL or LTL formula.