1
$\begingroup$

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!

$\endgroup$
8
  • 1
    $\begingroup$ $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. $\endgroup$
    – mohottnad
    Nov 9, 2021 at 22:38
  • $\begingroup$ @mohottnad yes p is a mistype. Sorry about this. Thanks for reviewing! $\endgroup$ Nov 9, 2021 at 23:03
  • $\begingroup$ @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. $\endgroup$ Nov 9, 2021 at 23:20
  • $\begingroup$ 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. $\endgroup$
    – mohottnad
    Nov 9, 2021 at 23:36
  • 1
    $\begingroup$ 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)$... $\endgroup$
    – mohottnad
    Nov 10, 2021 at 1:11

1 Answer 1

0
$\begingroup$

There is a kind of templates to translate common NLP patterns into LTL. https://matthewbdwyer.github.io/psp/patterns/ltl.html

Hope it helps :D.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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