# Defining a new operator in CTL

Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL.

My working: the system can only fail if $b$ holds. If $b$ doesn't hold, we're in the clear - so one possible path could be $(¬ □ b)$. The only other path that could hold is one where $a$ happens before $b$, so $(a$ $U$ $b)$ is another path. Overall we're left with $∀((a U b) ∨ (¬ □ b))$. For every path either $a$ happens before $b$ OR $b$ never happens.

Is the way I reasoned about this question correct? Are there any holes in my logic that I should re-consider? Please reply as a comment if possible, and many thanks in advance for any input.

• First, "$b$ doesn't hold" should be $\Box (\lnot b)$. Second, $a \bigcup b$ means $a$ hold at least until at some time $b$ holds. Is this desired? Or do you only require $a$ to hold at some time before $b$ holds? – hengxin Jan 15 '15 at 12:17
• First, the formula you defined is not in CTL (you're not allowed a disjunction between temporal operator inside a path quantifier). Secondly, since you can also read $\emptyset$ as a letter, it may very well be that both $aUb$ and $\neg \square b$ don't hold. By the way, I think you meant $\neg \diamond b$. – Shaull Jan 15 '15 at 13:01
• @hengxin actually $a$ should hold at some time before $b$ (not necessarily immediately before), in that case, I really can't think of a way to solve this. I've never worked with going backwards in a path? What sort of operators/combination of operators do I need to consider? $¬ \Diamond b$ does make more sense now that I think about it, thanks. – eyes enberg Jan 15 '15 at 14:28
• As you say, the time is "going backwards" in $a B b$. However, the time in $CTL$ goes forwards. So, a natural way is to consider the opposite of the specification ("in every execution, if $b$ holds some time, then $a$ does so before it"). A hint is: $a B b$ does not allow the case of $(\lnot a) \bigcup b$. BTW, there is a past CTL (PCTL) which incorporates past operators such as $\Diamond^{-1}$. – hengxin Jan 15 '15 at 15:10
• @hengxin How about $\forall ¬\exists( (¬a) U b) )$? So instead of focusing on which paths we can take we just state which ones we can't. – eyes enberg Jan 15 '15 at 19:54

For the answer $\forall \lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$:
I think you have got the right idea. However, this formula is not in CTL since $\lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$ is not a path formula.

By $\forall \lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$, I think you want to say $\forall \Box \left( \lnot \exists \left( \left( \lnot a \right) \bigcup b \right) \right)$, which is the answer.

(If you are observing the system from the very start (i.e., its initial state), the simpler and weaker one $\lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$ would be also acceptable. Please check it and let me know whether it is right.)

As I have mentioned in the comment, there are past CTLs (PCTL) which incorporate past operators facilitating the expression of "time going backwards". Using PCTL (for example in [1]), your property can be directly rendered by $\forall \Box (b \implies \Diamond^{-1} a)$ (Note its syntax!). You can guess the meaning of $\Diamond^{-1}$ easily.

• You seem to interpret the OP's question as a property that should hold infinitely. I wonder if that's the intention, or whether it should just hold once? – Shaull Jan 16 '15 at 8:57
• @Shaull It is a bit hard for me to tell the real intention of the OP from the literal statement. I also give a weaker edition without $\forall \Box$. Is it right to use $\forall \exists$ if it should just hold once? Please feel free to modify it or post a new answer/comment. – hengxin Jan 16 '15 at 10:43
• Thanks guys. I can't figure out which case the question wants (whether it should hold just once or forever). I will find out and get back to you, but I'm confident that I understand the concept of 'going back in time' now and how to solve a question of this type - so for that I'm really grateful. Also, we don't study PCTL though it does more appropriate in this context – eyes enberg Jan 16 '15 at 12:42
• The point is that without the $\forall \square$ the formula is not CTL, and so far I haven't found a corresponding CTL formula. Indeed, it might not be CTL. I actually don't like this form of questions, exactly because they give a description in English and ask for a formalization, whereas at least a mathematical definition should be given, to make things unambiguous. – Shaull Jan 16 '15 at 12:55