Defining a new (informal) operator in CTL

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.

• 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)$. Jan 12 '15 at 16:32
• 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? Jan 12 '15 at 16:42
• 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? Jan 12 '15 at 16:57
• 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? Jan 12 '15 at 17:27
• Or a can only hold if b holds? Maybe the way it's worded is what's throwing me off Jan 12 '15 at 17:33

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)$$

• 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))$ Jan 13 '15 at 0:18
• 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. Jan 13 '15 at 2:03
• 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$. Jan 13 '15 at 7:22
• 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. Jan 13 '15 at 15:28
• @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))$. Jan 13 '15 at 15:35