in many lecture notes, I have seen the LTL idempotent law for until and its equivalence is described as $\phi U(\phi U \psi) \equiv \phi U\psi$ and also $(\phi U \psi)U\psi \equiv \phi U \psi$
. Also by definition of $G$, some formula holds in every state. So if globally $\phi$ holds until we see $\psi$ does it make every state after it true? question might sound weird but by formula is it correct to say that also $G(\phi U \psi)U\phi \equiv G(\phi U \psi) $
$\begingroup$
$\endgroup$
1
-
$\begingroup$ Two comments: (1) the validity of an LTL formula is defined over words, not over states. (2) The last statement is ambiguous. There is no standard operator precedence for LTL, although it is typically assumed that unary operators bind stronger than binary operators. Thus, $G(\phi U \psi) U \phi$ can be read both as $(G(\phi U \psi)) U \phi$ and $G((\phi U \psi) U \phi)$, which have very different meanings. $\endgroup$– DCTLibJun 6, 2018 at 8:30
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
Also by definition of $G$, some formula holds in every state.
Well, $\sf true$ holds in every state. I'm unsure about why you mention $G$ here.
So if globally $\phi$ holds until we see $\psi$ does it make every state after it true?
A state can not be true or false, like 42 can not be true or false. This is meaningless.
is it correct to say that also $G(\phi U \psi)U\phi \equiv G(\phi U \psi) $
Take $\phi = \sf false$ and $\psi = \sf true$. Then, $G(\phi U \psi)U\phi$ is equivalent to $\sf false$, and $G(\phi U \psi)$ is equivalent to $\sf true$.
