World's most popular travel blog for travel bloggers.

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

, , No Comments
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

Answered By : Shaull

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

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback