Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers

1.3k comments

424 users

0 votes
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
in * TF "Emb. Sys. and Rob." by (790 points)

1 Answer

0 votes
 
Best answer

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.

by (117k points)
edited by

Related questions

Imprint | Privacy Policy
...