2019 August

Question

How is S1 satisfied ?, in s1 Xa holds and Fa has not been satisfied yet

Answer 1

I think Fa is satisfied on every states of the only path that we have, because we eventually see "a" in s2. so Fa should be true in s0 and s1. However, in my opinion, states s1 is not the point of interest. The state s0 is more interesting while [Fa SB Xa] is satisfied for a moment in time and that moment is enough to show the two formula are not equivalent. Correct me if I am wrong :)

Comments

I think your example path a -> c -> selfloop could also be correct as an example that satisfies S2 but not S1. However, I just doubt if we can use variable c in the structure while it is not present in either of formulas. So I think if you just replace c with {} such that your path looks like a -> {} -> selfloop , then it should be a correct example of a path that satisfies S2 but not S1 :)

---

i think a -> c -> selfloop satisfies S1 too because S1 says [Fa SB Xa] and in SB once Fa is satisfied it becomes satisfied. If it was [Fa SU Xa], then a -> c -> selfloop would not satisfy it

---

are you sure we can't include additional variables not included in the original formulas ?

---

Ah I see .. you are totally right, a -> c -> selfloop satisfies S1. I made a mistake there.
Regarding the c variable, now that I gave it a second thought, to my understanding, it shouldn't be wrong to include additional variables not included in the original formulas. However, I don't have a valid reference to a text book or slide to refer to. Generally my argument would be, having a state for {c} here, is like we have {!a,c} which implies !a obviously. Having a state for {} also implies {!a}. So both should be useable to solve this problem. Anyway, I hope we get a more promising answer from Martin or Prof. Schneider later.

---

Since there is only one outgoing transition in every state, we may add a A in front of each temporal operator and consider this way the CTL formulas A [(A F a) SB (A X a)]  and A F (a & !A X a) instead. This way, we can conveniently use the model checker to verify the example. However, note that these formulas are in general not equivalent, but on the considered structure they are!

We then get the following:

〖A X a〗 = {s1;s2}
〖!A X a〗= {s0}
〖a & !A X a〗= {}
〖A F (a & !A X a)〗 = {}

〖A X a〗 = {s1;s2}
〖A F a〗 = {s0;s1;s2}
〖A [(A F a) SB (A X a)]〗 = {s0}

So, the only path s0->s1->s2->... satisfies [(F a) SB (X a)] but not F(a & !X a) which distinguishes the two formulas.
 
Comments on the discussion above: Of course, you can use in the state transition diagrams also variables that do not occur in the formula. However, this has no effect on the evaluation of the formulas and thus, you can also safely ignore them.

If you consider the structure {a}->{c}->{} with a self loop on the final state {}, you get no difference on the formulas since then both formulas are satisfied: F a is true initially, X a is not, and thus (Fa) SB (X a) is satisfied initially, and since a & !Xa holds initially also, we also have F(a & !X a).