1
$\begingroup$

enter image description here

The task is to find an equivalent LTL formula for $G(a \Rightarrow Yb)$, which doesn't contain the Y operator. My idea is to search for invalid path patterns with 2 $a$'s in a row, e.g. bbbbaab.

Therefore I'm thinking of $G(Xa \Rightarrow b)$, so whenever an $a$ occurs in the next state the the current state must be true for $b$. But I have a problem with the starting states. Consider a path starting with $a$, e.g. s3->s4->... this path would be false for the original formula (iv), since Yb is always false for the first state. But this exact state would be true for the formula $G(Xa \Rightarrow b)$.

How do I have to modify my formula to also cover the starting states correctly?

$\endgroup$
2
$\begingroup$

Initial states are somewhat of an anomaly. A similar problem is encountered in the $X$ operator when you try to define LTL over finite words. That is, it somehow would have made more sense to define PLTL over computations that are "infinite on both sides".

So, being an anomaly, it is probably easiest to treat it as such, and just explicitly deal with the initial state, requiring the first state not to have $a$.

Thus, an equivalent formula would be $G(Xa\to b)\wedge \neg a$.

$\endgroup$
  • $\begingroup$ Thanks Shaull, now that I see the solution it's obvious. I honestly wasted 2 hours for that example and couldn't come up with the right solution. Do you mind proof checking my solutions for i)-iv)? i) {s0,s1,s2,s3} ii) {} iii){s1,s2,s3,s4} iv) {s2, s4} $\endgroup$ – Mad A. Apr 26 '15 at 16:00
  • $\begingroup$ All the answers seem correct to me. $\endgroup$ – Shaull Apr 26 '15 at 16:50

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.