3
$\begingroup$

Do they need to "unwind" exactly to the same set of paths or does it suffice when one set is contained in the other ?

Or is it sufficient to argue that M,s satisfies both LTL formulas for any starting s and a model M, that is, reaching with both at "true" ?

Generally.

Let $M$ be any model. Further, let $s$ be any state $M$ might be in.

Let $\phi$ and $\psi$ be two LTL formulas.

If $\forall$ paths $\pi$ in $M$ starting at $s$ it holds that $\pi \models \phi \leftrightarrow \pi \models \psi $ then we say $\phi$ and $\psi$ are equivalent ($\phi \equiv \psi$).

More succinct

$(\pi \models \phi \leftrightarrow \pi \models \psi) \rightarrow (\phi \equiv \psi)$.

Example. Prove that $\neg G \chi \equiv F \neg \chi$.

If we can show that $(\pi \models \neg G \chi \leftrightarrow \pi \models F \neg \chi)$ we would have proven that $(\neg G \chi \equiv F \neg \chi)$. So we reduce to the former.

Step 1. We show that $(\pi \models \neg G \chi \rightarrow \pi \models F \neg \chi)$:

$\{(\pi \models \neg G \chi) \leftrightarrow (\pi \not\models G \chi) \leftrightarrow (\forall i \geq 1, i \in \mathbb{N}. \pi^i \not\models \chi)\} \rightarrow \{(\exists i \geq 1, i \in \mathbb{N}. \pi^i \not\models \chi) \leftrightarrow (\exists i \geq 1, i \in \mathbb{N}. \pi^i \models \neg\chi) \leftrightarrow (\pi \models F \neg \chi)\}.$

Step 2. We show that $(\pi \models F \neg \chi \rightarrow \pi \models \neg G \chi)$:

$\{(\pi \models F \neg \chi) \leftrightarrow (\exists i \geq 1, i \in \mathbb{N}. \pi^i \models \neg\chi) \leftrightarrow (\exists i \geq 1, i \in \mathbb{N}. \pi^i \not\models \chi)\} \rightarrow \{?\}.$ How do I get back?

Ok. I can semantically understand that if for every model and any path in it, it is true eventually that $\neg \chi$ holds, it cannot be the case that generally for every model and any path in it $\chi$ will hold. How can I write this down formally?

Would for $\{?\}$: $\{\neg (\forall i \geq 1, i \in \mathbb{N}. \pi^i \models \chi) \leftrightarrow (\neg (\pi \models G \chi)) \leftrightarrow (\pi \not\models G \chi) \leftrightarrow (\pi \models \neg G \chi)\}$ be a valid argumentation ? It looks different than Step 1. and anyway is there a rule to pull $\neg$ "out" from $\not\models$ this way ?

$\endgroup$
5
$\begingroup$

The semantics of LTL is (initially) defined with respect to infinite computations. So in that sense, two formulas $\psi_1,\psi_2$ are equivalent if for every computation $\pi$ it holds that $\pi\models \psi_1$ iff $\pi\models \psi_2$.

So in this sense - yes, you need the formulas to unwind the same set of computations.

The semantics is then extended to Kripke structures in the $ALTL$ model, meaning that a formula is satisfied in a structure if all its computations satisfy the formula. However, testing for equivalence should be done with respect to paths.

As for proving formally the equivalence of formulas: if this is an exercise, it will probably be easiest to analyze the formulas and prove that a path satisfies the first iff it satisfies the second. However, if you are handling complex formulas, then the best approach will probably be via nondeterministic Buchi automata, by testing the equivalence of the automata that correspond to the formulas. In practice, there are tools to do just that, but doing it manually may prove quite time-consuming (as the problem is PSPACE complete).

$\endgroup$
3
$\begingroup$

You are in fact asking when two LTL formulas are equivalent. Two formulas are equivalent if they have the same truth value on all models. Given the definition, you should be able to answer your question yourself. Until you can do so, you haven't understood the definition, and so cannot expect to work with it other than mechanically.

$\endgroup$
2
$\begingroup$

Hint: LTL (on infinite strings) is equivalent to Büchi automata.

There are transfer algorithms and many properties of Büchi automata are decidable.

$\endgroup$
  • $\begingroup$ I would be careful using the word equivalent... there are Büchi automata that are not translatable into LTL as LTL capture the star-free regular languages, a strict subset of regular. $\endgroup$ – selig Apr 1 '15 at 9:01
  • $\begingroup$ @selig It has been a while since I wrote this, but note that we deal with infinite strings (i.e. $\omega$-regular languages) here. I'm not sure if there's an equivalent of "star-free" there, and I'm pretty sure I have the equivalence from a credible source. Can you check yours, please? $\endgroup$ – Raphael Apr 1 '15 at 9:40
  • $\begingroup$ @Raphael If the word 'equivalent' means every LTL can be converted to a Büchi and every Büchi can be converted to an LTL, then the statement: LTL (on infinite strings) is equivalent to Büchi automata, is not true. LTL's can capture only non-counting languages. For example, $(00)^*1^\omega$ cannot be captured by an LTL. See slide 12 onwards $\endgroup$ – pranavashok Oct 2 '15 at 21:37
  • $\begingroup$ @pranavashok Huh, true enough. It's been a while; I'll check my notes to see where I went wrong. $\endgroup$ – Raphael Oct 2 '15 at 22:05

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.