Could someone kindly proof check my solution for a task in problem 7?

Question

Hello,

In problem 7.e of the Feb 2020 exam, it is asked to find a counterexample for equivalence of the two formulas.

Could someone please verify for me if my solution below (which obviously differs from the provided solution) is also correct or not? if not, why?

Thanks in advance.

Answer 1

There is one bug about your signal trace. something^ω means that something holds infinitely often. So you can't something^ω somethingelse^ω because thensomethingelse would happen after the end of infinity which is quite late (and impossible).

What you'd rather do is describing all paths that satisfy G(p ∧ ¬q) and then identifying all states from where such a path can be started (i.e. the states satisfying EG(p ∧ ¬q):
As (p ∧ ¬q) only holds in your middle state, the path consisting of this state infinitely often is the only path satisfying G(p ∧ ¬q). That makes this state the only state satisfying EG(p ∧ ¬q). The initial state does not satisfy EG(p ∧ ¬q).

So your structure satisfies neither of the formulas.

Here are two hints:

1. Is S2 satisfiable?
2. What happens if you remove your initial state and make the current middle state the new initial state?

Answer 2

You can rewrite S1 to the CTL formula E F q & E G (p & !q) so that you can use our CTL model checker with the following input to check both CTL formulas:

transition system:

    vars p,q;
    init 0;
    labels 0:; 1:p; 2:q;
    transitions 0->1; 1->2; 1->1; 2->2;

specs: 

    (E F q) & E G(p&!q);
    E F(q & E G(p&!q))

You will find the following:

• 〖p〗= {s1}
• 〖q〗= {s2}
• 〖p & !q〗 = {s1}
• 〖E G (p & !q)〗 = {s1}
• 〖E F q〗 = {s0;s1;s2}
• 〖q & E G (p & !q)〗 = {}
• 〖E F q & E G (p & !q)〗= {s1}
• 〖E F (q & E G (p & !q))〗= {}

The two formulas are state formulas, and therefore it is required to say in which state the one, but not the other one holds. Traces are used to distinguish path formulas.

Comments

Your last paragraph was an important remark which I was missing so thank you very much for pointing that out Prof. Schneider. Now if we ignore the trace part, after all, since according to model checker, the formula S1 is satisfied in state s1 and the formula S2 is not satisfied on any state, can we say the structure I drew is sufficient to show these 2 formulas are not equivalent or still not?

---

Yes, state {p} of your structure distinguishes between the two formulas. You don't even need the state {} and could use {p} as initial state.

---

That honestly cleared many of my doubts. Many thanks.