World's most popular travel blog for travel bloggers.

# [Answers] Defining a new (informal) operator in CTL

, ,
Problem Detail:

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.

###### Asked By : eyes enberg

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