Question

Use your own words, describe the semantic meaning of the following LTL expressions (note that the U symbol is the Until operator, not the set union operator, true is a Boolean constant that always holds at any state in a sequence)

a. p -> F q

b. G F p

c. F G p

d. true U q

e. ¬ (F ¬p)

Answer 1

a. p->Fq = p implies eventually q = If p is true then q is true sometimes in the future.

b. GFp = Infinitely Often = Everywhere Fp is true from any point in the world I will be able to reach a point where p is true i.e. p is true infinitely often.

c. FGp = Eventually Forever = At some point of time, Gp is true which means there is some point from where p is always true

d. true U q = Fq = true until q = At some point of time q is true and until that time you don't care what to be true.

e. ¬(F¬p) = ¬(¬Gp) = Gp = p is always true in the future.