1
$\begingroup$

I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure:

Kripke structure

Now given the following CTL formulae A(g U EG (b v y)) , which states does it satisfy?

I know that the answer is {s1,s2,s3} (according to lecture notes), but I don't understand that.

This is what I have tried so far to solve it:

  1. I solve EG(b v y) first and for this I get {s1,s3} because from these states there exists a path where either b or y holds globally.
  2. Then I group it together again and solving A(g U EG(b v y)) which I understand as "Along all paths, g holds until there exist a path where b or y holds" and as I already know the last part of it, I understand it as "Along all paths, g holds until either s1 or s3 holds".

To me s2 is the only obvious answer because g holds in s2 until y holds in s1. I don't understand why s1 or s3, is a part of the answer.

Anyone care to explain? Or at least show the steps you take to derive the answer?

$\endgroup$
  • $\begingroup$ Welcome to Computer Science! Note that you can use LaTeX here to typeset mathematics in a more readable way. See here for a short introduction. $\endgroup$ – FrankW Sep 18 '14 at 19:00
1
$\begingroup$

The semantics of the "Until" operator allows for the eventuality to be satisfied immediately. That is, $pUq$ holds both in the computation $ppppq$, but also in $q$.

Thus, in your formula, the eventuality is satisfied immediately in states $s_1,s_3$, and satisfied within 1 step in $s_2$. But all of them satisfy it.

$\endgroup$
  • $\begingroup$ Ooh. That makes much more sense. I never assumed that it could be satisfied already. Thank you! $\endgroup$ – DSF Sep 18 '14 at 19:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.