<p>I am not sure what you are referring to when you say "this is not covered in theory in general." The specific example that you give has been studied and is called antecedent failure. </p>

<blockquote>
  <p><a href="http://www.cs.york.ac.uk/rts/docs/DAC-1964-2006/PAPERS/1994/DAC94_596.PDF" rel="nofollow">Formally verifying a microprocessor using a simulation methodology.</a>, D. L. Beatty and R. L. Bryant, 1994</p>
  
  <p><em>One of the principal dangers of formal verification is what we have called antecedent failure. Formally, implications have an extensional meaning: they are also true if the antecedent condition is not true. Antecedent failure means that we can speak nonsense and not realise it.</em></p>
</blockquote>

<p>The problem of detecting more general forms of such logical pitfalls is called vacuity detection. The introduction of the paper below has an excellent overview. You will also find examples of formulae.</p>

<blockquote>
  <p><a href="http://www.cs.rice.edu/~vardi/papers/cav03.ps.gz%E2%80%8E" rel="nofollow">Enhanced Vacuity Detection in Linear Temporal Logic</a>, Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, and Moshe Y. Vardi, 2003</p>
</blockquote>

<p>There are lots of courses where people teach temporal logic and those notes and exercises have lots of examples. I would also suggest Manna and Pnueli's book for examples. </p>

CC BY-SA 3.0
2013-07-07T20:16:09.780Z
2013-07-07T20:16:09.780Z
Vijay D
<p>A good starting point for practical LTL examples is <a href="http://www.iaik.tugraz.at/content/research/design_verification/lily/" rel="nofollow">LILY</a>, as well as the <a href="http://www.iaik.tugraz.at/content/research/design_verification/prosyd/" rel="nofollow">PROSYD project</a>.</p>

<p>They provide some examples for LTL formulas, both "toy examples" and real-life applications. I think the website for the Prosyd project is a bit dead.</p>

<p>By the way, your interpretation of the formula $P\to \Diamond Q$ is not exactly correct. First of all, it is not a state-formula, even if you consider it as a CTL^* formula and not an LTL formula.
It's evaluation is over a path, and a path satisfies it iff if P holds in the first state of the path, then eventually Q also holds.</p>

CC BY-SA 3.0
2013-07-07T15:18:42.167Z
I changed a bit my explanation but afaik a path satisfy an LTL formula by definition wlog. iff it holds on its first state in that path. As long as this path satisfies $\Diamond Q$ P can be true or false, which doesn't matter. As such it is a bit weird.
panny
CC BY-SA 3.0
2013-07-07T18:08:14.157Z
As it is now, it is correct indeed.
Shaull
CC BY-SA 3.0
2013-07-07T14:59:36.407Z
2013-07-07T14:59:36.407Z
Shaull
<p>I would like to practice on some problems for using LTL formulae but besides the foundations and theory there are only every few examples. I know that having understood theory is not enough. Where can I go looking for interesting applications, examples including discussions about it. Is it possible to open a thread with examples here?</p>

<p>E.g. </p>

<p>$(P\to \Diamond Q)$ is intriguing. One would think "On a path $\pi$ starting at state $s$ when P holds, eventually Q will hold." But of course given LTL formula does also hold for any other path which does not satisfy $P$ but $\Diamond Q$ (def. $\rightarrow$ or $\neg P \vee  Q$).</p>

<p>Now, this is not covered in theory in general. It is experience knowledge. I want to practice LTL formulae, where can I go looking for them?</p>

<linear-temporal-logic>
Resource for LTL formulae?
panny
# Resource for LTL formulae?

(Asked by: username_0 on 2013-07-07)

I would like to practice on some problems for using LTL formulae but besides the foundations and theory there are only every few examples. I know that having understood theory is not enough. Where can I go looking for interesting applications, examples including discussions about it. Is it possible to open a thread with examples here?

E.g.

$(P\to \Diamond Q)$ is intriguing. One would think "On a path $\pi$ starting at state $s$ when P holds, eventually Q will hold." But of course given LTL formula does also hold for any other path which does not satisfy $P$ but $\Diamond Q$ (def. $\rightarrow$ or $\neg P \vee Q$).

Now, this is not covered in theory in general. It is experience knowledge. I want to practice LTL formulae, where can I go looking for them?

**Tags:** linear-temporal-logic

---

## 2 answers

### Answer by username_1 on 2013-07-07. Score: 2

I am not sure what you are referring to when you say "this is not covered in theory in general." The specific example that you give has been studied and is called antecedent failure.

> [Formally verifying a microprocessor using a simulation methodology.](http://www.cs.york.ac.uk/rts/docs/DAC-1964-2006/PAPERS/1994/DAC94_596.PDF), D. L. Beatty and R. L. Bryant, 1994
>
> *One of the principal dangers of formal verification is what we have called antecedent failure. Formally, implications have an extensional meaning: they are also true if the antecedent condition is not true. Antecedent failure means that we can speak nonsense and not realise it.*

The problem of detecting more general forms of such logical pitfalls is called vacuity detection. The introduction of the paper below has an excellent overview. You will also find examples of formulae.

> [Enhanced Vacuity Detection in Linear Temporal Logic](http://www.cs.rice.edu/~vardi/papers/cav03.ps.gz%E2%80%8E), Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, and Moshe Y. Vardi, 2003

There are lots of courses where people teach temporal logic and those notes and exercises have lots of examples. I would also suggest Manna and Pnueli's book for examples.


---

### Answer by username_2 on 2013-07-07. Score: 1

A good starting point for practical LTL examples is [LILY](http://www.iaik.tugraz.at/content/research/design_verification/lily/), as well as the [PROSYD project](http://www.iaik.tugraz.at/content/research/design_verification/prosyd/).

They provide some examples for LTL formulas, both "toy examples" and real-life applications. I think the website for the Prosyd project is a bit dead.

By the way, your interpretation of the formula $P\to \Diamond Q$ is not exactly correct. First of all, it is not a state-formula, even if you consider it as a CTL^\* formula and not an LTL formula.
It's evaluation is over a path, and a path satisfies it iff if P holds in the first state of the path, then eventually Q also holds.

> **Comments:**
> **username_0**: I changed a bit my explanation but afaik a path satisfy an LTL formula by definition wlog. iff it holds on its first state in that path. As long as this path satisfies $\Diamond Q$ P can be true or false, which doesn't matter. As such it is a bit weird.  
> **username_2**: As it is now, it is correct indeed.  

---

