Howto formally go about proving that two LTL formulas are equivalent?

Question

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 ?

Answer 1

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

Answer 2

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.

Answer 3

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

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