# Translating Natural Language to LTL Formulae

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:

1. $$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

1. $$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!

• $G$ had better be translated as on all subsequent path. For 1. isn't p a typo and should be $l$? And its translation seems very straightforward. For 2. again isn't p a typo and should be $l$? And $F$ had better be translated as "eventually somewhere on the subsequent path". Overall sounds fine to me. Nov 9, 2021 at 22:38
• @mohottnad I am thinking my last formula is wrong because it's not 'always' that $l$ is false between $m$ and $n$. Would it be $(m \land Fn) \to \neg l \space Un$? I just removed the G. Nov 9, 2021 at 23:20
• But your spec requirement of 2 clearly states "$l$ is false between $m$ and $n$", I don't understand why it's not always so? Your goal is to write such a sentence to satisfy the spec, right? In general in LTL we need unary or binary operators for the whole sentence. Nov 9, 2021 at 23:36
• If you use $U$ as above then $l$ must be always false between $m$ and $n$. If you interpret your spec as $l$ only needs sometimes false between $m$ and $n$, then you may try something like $G((m∧F(¬l))→ Fn)$... Nov 10, 2021 at 1:11