1
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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., 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, 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.

$\endgroup$
1
$\begingroup$

A good starting point for practical LTL examples is LILY, as well as the PROSYD project.

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – panny Jul 7 '13 at 15:18
  • $\begingroup$ As it is now, it is correct indeed. $\endgroup$ – Shaull Jul 7 '13 at 18:08

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.