CTL,LTL and CTL∗ (August 2019)

Question

Please find below my solution is which is different from the exam solution:

Justification for S₁ with signal traces

a                   | (1)^ω

Fa                 | (1)^ω

Xa                | (1)^ω

[Fa SB (Xa)]  | (1)^ω        {because eventually "a" holds (which is from the first point of time)  before next of "a" (as next of "a" is true: self loop) and eventually "a" holds forever (self loop)}

Justification for S₂ with signal traces

a                   | (1)^ω

¬Xa              | (0)^ω

(a & ¬Xa)    | (0)^ω

F(a & ¬Xa)  | (0)^ω

^{Please let me know if my solution is also correct or I did any mistake?}

^{In general can there be multiple solutions to these kind of questions?}

^{Thank you in advance.}

Answer 1

[p SB q] demands that p holds before q holds, so if p is 1^omega and q is 1^omega, then [p SB q] is 0^omega which is then the same as F(a&!Xa) on your path. Hence, your solution is wrong.

Comments

Thank you for the clarification.