Exam 2017.02.15

Question

Hi,

My Solution Satisfy S2 but not S1, Is my solution correct?

Answer 1

S1 is the same as:

EXFG!b

Hence, your path satisfies both formulas.

Comments

Could you explain the transformation of !AXGFb to EXFG!b ?

---

Sure, I can explain that.

!AXFGb
= E!XFGb (not all paths have the property is the same as at least one path doesn't have the property)
= EX!FGb (no difference whether we negate now or in the next step)
= EXG!Gb
= EXGF!b

---

Thank you for easy explaination

Answer 2

I am afraid that your solution is not correct. We can quickly rewrite your formulas to equivalent CTL formulas:

•     S1 = !A X A G A F b
•     S2 = A G A X A F !b

Then the model checker computes:

•     〖!A X A G A F b〗= {s0}
•     〖A G A X A F !b〗 = {s0}