Find equivalent LTL formula, without Y (Yesterday) operator. How can I handle first state?
-
02-11-2019 - |
Question
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?
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange