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.

  • 1
    $\begingroup$ 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? $\endgroup$ – hengxin Jan 15 '15 at 12:17
  • 1
    $\begingroup$ 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$. $\endgroup$ – Shaull Jan 15 '15 at 13:01
  • $\begingroup$ @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. $\endgroup$ – eyes enberg Jan 15 '15 at 14:28
  • $\begingroup$ 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}$. $\endgroup$ – hengxin Jan 15 '15 at 15:10
  • $\begingroup$ @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. $\endgroup$ – 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.

[1] Specification in CTL+Past for Verification in CTL (2000)

  • $\begingroup$ 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? $\endgroup$ – Shaull Jan 16 '15 at 8:57
  • $\begingroup$ @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. $\endgroup$ – hengxin Jan 16 '15 at 10:43
  • $\begingroup$ 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 $\endgroup$ – eyes enberg Jan 16 '15 at 12:42
  • 1
    $\begingroup$ 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. $\endgroup$ – Shaull Jan 16 '15 at 12:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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