Problem Detail: 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 notmodels G chi) leftrightarrow (forall i geq 1, i in mathbb{N}. pi^i notmodels chi)} rightarrow {(exists i geq 1, i in mathbb{N}. pi^i notmodels chi) leftrightarrow (exists i geq 1, i in mathbb{N}. pi^i models negchi) 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 negchi) leftrightarrow (exists i geq 1, i in mathbb{N}. pi^i notmodels 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 notmodels 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 $notmodels$ this way ?
Asked By : panny
Answered By : Shaull
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 $pimodels psi_1$ iff $pimodels 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).
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/13092
