Return to Question

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 p

2. $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 p until n

Is my thinking correct in the examples? Thanks for the help!

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

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

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 p

2. $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 p until n

Are these right? Thanks for the help!

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 p

2. $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 p until n

Is my thinking correct in the examples? Thanks for the help!

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 it is always the case that m implies always not p

2. $l$ is false between $m$ and $n$

LTL Translation: $G((m \land Fn) \to \neg l \space Un)$ i.e it is always the case that m and finally n, implies negation of p until n

Are these right? Thanks for the help!

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 p

2. $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 p until n

Are these right? Thanks for the help!