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

868 questions

986 answers

1.4k comments

438 users

0 votes

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.

related to an answer for: LTL Equivalence and its notation
in * TF "Emb. Sys. and Rob." by (630 points)

1 Answer

0 votes
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.
by (139k points)
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.

Related questions

0 votes
1 answer
0 votes
1 answer
asked Jun 17, 2019 in * TF "Emb. Sys. and Rob." by erji (420 points)
0 votes
1 answer
Imprint | Privacy Policy
...