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 don't think [Fa SB Xa] holds at all because in s1 a doesn't hold at all before Xa then holds. In a SB b, a must hold before b becomes true

---

hmm a does not hold in s1, true, but Fa holds, doesn't it?

---

frzmohammadali, you are right.

daodubasit, you best see it if you just isolate the subformulas. a holds from the third step on, Xa form the second step on. Fa from the first step on. Because it is true from the first step on that it only takes finitely many steps until a holds.

If we look at the states we identified for the subformulas, it is something like:

[ {any step} SB {second step and everything after that} ]

This does hold exactly in the first step.

---

ah, i see that now. does a->b->a->b.... satisfy s2 and not s1. because looking at it from state b violates [Fa SB Xa]

---

a→b→a→b…

would satisfy both formulas. There'd be a in the first step, satisfying Fa in the first step, satisfying the SB in the first step. Xa is not satisfied as {b} does not satisfy a. So S1 is satisfied. Also, first step satisfy a&X¬a. So F(a&X¬a) is satisfied to.

---

oh true, i was thinking of G[a SB Xa], that would not be satisfied by a→b→a→b…

---

as a counter example for S1, a->c->c->c .... would satisfy s2 and not s1 right since Xa never holds

---

ignore my last comment, i just realised i was thinking of something else. sorry. Can you please provide an example that satisfies s2 and not s1

---

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).