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

1.1k questions

1.2k answers


546 users

0 votes


How does path shown below satisfy S1?

in * TF "Emb. Sys. and Rob." by (1.4k points)
edited by
Out of curiosity: Who painted this path?
I did, using online tool
oh. Interesting. I normally use Tikz Automate or our own teaching tools. Always interesting to see different styles.
ahh i see, i used,

1 Answer

+1 vote
Best answer

I don't think that the path satisfies S1: To simplify matters, we may write (a<->b) as ¬(a⨁b), so that S1 becomes ¬XX(G(a⨁b)⨁F¬(a⨁b)) and moreover equivalent to ¬XX(G(a⨁b)⨁¬G(a⨁b)). If you now abbreviate G(a⨁b) as p, the formula becomes ¬XX(p⨁¬p) and since p⨁¬p holds for any p, it is simply true. Hence, it follows that S1 is simply false on every path.

The path does also not satisfy S2, so it does not distinguish between these two formulas. You can quickly check this with the online tool using the following:

    (¬a&¬b) & X(¬a&¬b) & X X G(a&b) -> X X G((a⊕X a)&(b⊕X X b))

To distinguish between the two formulas, we therefore need a path that satisfies S2. Obviously, this path must satisfy after two steps G((a⊕X a)&(b⊕X X b)) and that means that a always alternates between true and false, and b does the same but with a period of 2.

For instance, the following will satisfy S2, but not S2:

by (166k points)
selected by

Related questions

0 votes
1 answer
0 votes
1 answer
asked Feb 8, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy