0
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • 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, 2015 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, 2015 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, 2015 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, 2015 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, 2015 at 19:54

1 Answer 1

Reset to default
1
$\begingroup$

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)

Improve this answer
$\endgroup$
4
  • $\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, 2015 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, 2015 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, 2015 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, 2015 at 12:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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