Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

972 questions

1.1k answers


469 users

0 votes

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

in * TF "Emb. Sys. and Rob." by (790 points)
Seems to be rather LTL model checking than CTL satisfiability.

1 Answer

0 votes
Best answer

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.
by (25.6k points)
selected by

Related questions

Imprint | Privacy Policy