# Exam 2020.02.19 problem 7

Hi,

How does path shown below satisfy S1?

edited
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 draw.io,

+1 vote

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