I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct.
I'm given the sentences, and my assumption is that $l$ is true:
- $l$ is always false after $m$
LTL Translation: $G(m \to G(\neg l))$ i.e on all paths m implies on all paths not l
- $l$ is false between $m$ and $n$
LTL Translation: $G((m \land Fn) \to \neg l \space Un)$ i.e on all paths m and finally n, implies not l until n
Is my thinking correct in the examples? Thanks for the help!