CTL satisfiability

Question

S1 = b ∧ X(¬b ∧ GFa) 

S2 = b ∧ X(¬b ∧ Ga)

I believe 1 in the picture below satisfies S1 and S2 but i am not sure if 2 satisfies S1 and not S2

Comments

Seems to be rather LTL model checking than CTL satisfiability.

Answer 1

Both structures satisfy S1 but not S2.

Let's look at the formulas from inside out:

• Ga: neither of the paths have a section from where on a holds on every step.
• GFa: holds on all states of both paths. No matter where we are, we reach a after finitely many steps.
• ¬b: holds in the second state of both paths, and in the third state of the first path.
• X(¬b ∧ Ga): holds nowhere as Ga holds nowhere
• X(¬b ∧ GFa): as GFa holds everywhere, this formula holds on all states whose successors satisfy ¬b. Thus, it holds on all states except for the second state of the second path.
• b ∧ X(¬b ∧ Ga): holds nowhere as  X(¬b ∧ Ga) holds nowhere
• b ∧ X(¬b ∧ GFa): holds precisely on the initial states as they satisfy both b and the inner X-formula.