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!

Improve this question
$\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$
    – cinch
    Commented Nov 9, 2021 at 22:38
  • $\begingroup$ @mohottnad yes p is a mistype. Sorry about this. Thanks for reviewing! $\endgroup$
    – UnevenMango
    Commented 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$
    – UnevenMango
    Commented 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$
    – cinch
    Commented 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$
    – cinch
    Commented Nov 10, 2021 at 1:11

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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