0
$\begingroup$

If you were given a "new operator" Wh and a formula a Wh b meaning that a holds for at least as long as b does (in all executions). How would you define this operator in CTL? This is an exercise question in the book "Principles of Model Checking" (page 303) if anyone has a copy.

My first thoughts are that I'll definitely need to use the "FOR ALL" quantifier, but I'm not sure where to go from there. So I want to know the thought-process that I should have when dealing with these types of questions more than anything. What I'm looking for is for someone to perhaps give me a walk-through or a very quick guide to solving questions like these.

Thanks in advance for any input.

Improve this question
$\endgroup$
7
  • $\begingroup$ Note that this operator is temporal, and does not relate to path quantifiers (A and E). So you need to use only temporal operators to define it. Then, you can talk about $A(a\ Wh\ b)$ or $E(a\ Wh\ b)$. $\endgroup$
    – Shaull
    Jan 12, 2015 at 16:32
  • $\begingroup$ Ah OK, I'm still unsure as to what my answer should look like. Should it include a and b or just a bunch of squares/circles/diamonds? $\endgroup$
    – eyes enberg
    Jan 12, 2015 at 16:42
  • $\begingroup$ Well, you will need to apply these squares/circles/diamonds to some arguments, won't you? So you will obviously need to use $a$ and $b$. Perhaps try to think of these not as operators, but as properties: how would you express the property "$a$ holds at least as long as $b$ holds" in CTL? $\endgroup$
    – Shaull
    Jan 12, 2015 at 16:57
  • $\begingroup$ Hmm, still not sure. If we get rid of "at least" and just work with "a holds as long as b holds", is this basically saying a and b occur at the same time? $\endgroup$
    – eyes enberg
    Jan 12, 2015 at 17:27
  • $\begingroup$ Or a can only hold if b holds? Maybe the way it's worded is what's throwing me off $\endgroup$
    – eyes enberg
    Jan 12, 2015 at 17:33

1 Answer 1

Reset to default
2
$\begingroup$

You seem to be stuck, so here is the answer:

You want $a$ to hold for at least as long as $b$ does. The alphabet consists of $2^{\{a,b\}}=\{\emptyset, \{a\},\{b\},\{a,b\}\}$.

Rephrasing the condition, it means that $\{b\}$ cannot appear before either $\{a\}$ or $\emptyset$ have appeared. Indeed, this is the only violation of the condition.

So once $\{a\}$ or $\emptyset$ hold, you're in the clear. You just need to make sure that until then (sounds familiar?), $\{a,b\}$ holds.

Thus, you have $$a\ Wh\ b\equiv (a\wedge b)U(\neg b)$$

Improve this answer
$\endgroup$
9
  • $\begingroup$ Wow this made a lot of sense. One little thing I want to be clear on though, since the question says this must hold FOR ALL EXECUTIONS - should there be a square in front of the entire formula? So $\Box((a \wedge b) U (¬b))$ $\endgroup$
    – eyes enberg
    Jan 13, 2015 at 0:18
  • $\begingroup$ So there's another question that says define $N$ where $a$ $N$ $b$ means there is an execution such that, at the next time $b$ holds, $a$ also holds. I followed your exact steps (listed the letters, rephrased the question then found the violations of the condition) and ended up with $\diamond ((a$ $\wedge$ $b$) $U$ $¬\bigcirc b)$. I feel pretty confident with this but would you be kind enough to double check that this is correct? A little confirmation goes a long way for me. $\endgroup$
    – eyes enberg
    Jan 13, 2015 at 2:03
  • 1
    $\begingroup$ For your first question - No, it would be $A$ before the formula, not $\square$. Otherwise it wouldn't even be a legal CTL formula, but an LTL formula. For the second question, it should be $E(\neg b U (b\wedge a))\vee E(\square \neg b)$, since you want not to allow $b$, unless it comes with an $a$. $\endgroup$
    – Shaull
    Jan 13, 2015 at 7:22
  • 1
    $\begingroup$ Two comments: (1) You can actually simplify that formula to $a U (\neg b)$, and (2) I would interpret "at least as long as" as allowing the trace where $a$ and $b$ hold forever, i.e. $a W (\neg b)$, where $W$ is weak until. $\endgroup$
    – Klaus Draeger
    Jan 13, 2015 at 15:28
  • 1
    $\begingroup$ @KlausDraeger - The simplification $aU(\neg b)$ is incorrect, since it allowes computations such as $\emptyset,b,a^\omega$ (the until is satisfied in the first step). I agree that one can use Weak Until, but it should still be $E((\neg b)W (b\wedge a))$. $\endgroup$
    – Shaull
    Jan 13, 2015 at 15:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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