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 Answers 2

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$
2
  • $\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, 2015 at 16:00
  • $\begingroup$ All the answers seem correct to me. $\endgroup$
    – Shaull
    Apr 26, 2015 at 16:50
0
$\begingroup$

Considering those equivalences: $G \phi \sim \phi \wedge X G \phi$ and $f \to g \sim \neg f \vee g$

We obtain that: $G(a \to Yb) \sim (\neg a \vee Yb) \wedge X G(\neg a \vee Yb)$

Assuming that $Yb$ cannot be satisfied in the first state (state 0) (notice that this is a semantic option for operator Y) so $(\neg a \vee Yb)$ can be reduced to $\neg a$. Thus the whole formula can be reduced to $\neg a \wedge X G(\neg a \vee Yb)$

The latter formula tells us that $G(\neg a \vee Yb)$ must be satisfied in states 1. Hence $(\neg a \vee Yb)$ must be satisfied in any state whose index is $\geq 1$. Let $i \geq 1$. Satisfying $(\neg a \vee Yb)$ at state $i$ is equivalent to satisfy $b \vee X \neg a$ at state $i-1$ (which exists since $i \geq 1$). You can derive this by considering that when $i \geq 1$, $i \models \phi$ $\Leftrightarrow$ $i-1 \models X \phi$. In our case : $i \models ( \neg a \vee Yb)$ $\Leftrightarrow$ $i-1 \models X( \neg a \vee Yb) = X \neg a \vee X Yb = X \neg a \vee b$.

We conclude that satisfying $G( \neg a \vee Yb)$ from state 1 is the same than satisfying $G(b \vee X \neg a)$ from state 0.

Hence the equivalent requested formula is: $\neg a \wedge G(b \vee X \neg a)$

As $X \neg a \sim \neg X a$

This formula can also be written $\neg a \wedge G(Xa \to b)$ as already given in a previous answer above.

$\endgroup$

Your Answer

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

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