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

1.1k questions

1.2k answers


524 users

0 votes


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

in * TF "Emb. Sys. and Rob." by (1.4k points)

2 Answers

+1 vote
Best answer
S1 is the same as:


Hence, your path satisfies both formulas.
by (25.6k points)
selected by
Could you explain the transformation of !AXGFb to EXFG!b ?
Sure, I can explain that.

= 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
+1 vote

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}
by (165k points)

Related questions

0 votes
2 answers
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy