Why Fb sequence is 1 0 0 0 .. ?

Question

Hello,

if in above example, FB sequence is 1 0 0 0 ...

Then Is the below second representation of Fa in exercise solution sheet a valid representation?

Because here also Fa sequence will be 1 0 0 0 ....

Kindly confirm.

Answer 1

I am not sure what you are asking, but the two paths satisfy the formula F a, since there is a point of time on these paths where "a" holds. Note that for F a, it is sufficient to have an infinite path where at least once "a" holds.

Comments

Thanks for the explanation.
But I saw you provided a sequence as below in the related question :
                b : 1 0 0 0 ...
              F b : 1 0 0 0 ...

I extracted the part of the solution you provided in related question ( LTL Equivalence and its notation)

Why Fb sequence here is 1 0 0 0.. since b atleast holds once, Should not it be 1 1 1 1 .... ?

Thanks.

---

If we have a path where b is evaluated as 1 0 0 0 ... then F b is 1 0 0 0 ... also, since at the initial point of time, we consider the path 1 0 0 0 ... and find a point of time where b holds. At the next point of time, and all others that follows, we consider the path 0 0 0 ... and there is no point of time where b holds. Thus F b is false there.