0 votes

Hi,

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

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 (93k 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
0 votes
1 answer
asked Aug 23, 2020 in * TF "Emb. Sys. and Rob." by Nicola (800 points)
Imprint | Privacy Policy
...