RiccardoDeMasellis
commented
8 years ago The above translation does not work. The problem relies in the more expressive power of LDL and the fact that we may have an empty trace. In LDL we do have a semantics for the empty trace, whilst in LTL there is no semantics for what happens when the trace is empty (this is something conceotually analogous with the problem of the next step when the trace is finite-length).
Problems rises with negation. For example, what does it mean !a in LTL? It may mean that the empty trace is accepted or it is not. We decide that it is not hence it is translated < ! a > tt, which means that something different from a must be seen. Notice that in LDL there is no such an ambiguity, because, if we want the empty trace to be accepted, we can write [ a ] ff, while if we do require to see at least one world in the trace, we can write < ! a > tt.
In order to formally fix such a semantics mismatch, we could add another negation in LTL (similarly to what we do when we added the "weak next" to solve the problem on finite traces). We did not choose this option because for two main reasons: 1) it is cumbersome; 2) when one write something in LTL, the intuition tells that if the negation occurs right in front of a variable, then we intuitively require the trace not to be empty, while if it occurs in front of a temporal operator, it means that the trace may be empty or not (depending on specific operators).
So when we have an LTL formula, first thing we do is transform it in an anti-nnf form, which works recursively as follows: annf(Prop) = Prop (where Prop is a LOCAL propositional formula!) annf(Phi1 & Phi2) = annf(Phi1) & annf(Phi2) annf(Phi1 || Phi2) = annf(Phi1) || annf(Phi2) annf(Phi1 -> Phi2) = annf(! Phi1 || Phi2) annf(Phi1 <-> Phi2) = annf( (Phi1 -> Phi2) && (Phi2 -> Phi1) ) annf(!Phi) = ! annf(Phi) annf(F Phi) = F annf(Phi) annf(G Phi) = ! (F !annf(Phi)) annf(X Phi) = X annf(Phi) annf(WX Phi) = ! X !annf(Phi) annf(Phi1 U Phi2) = annf(Phi1) U annf(Phi2) annf(Phi1 R Phi2) = ! ( !annf(Phi1) U !annf(Phi2)) annf(Phi1 WU Phi2) = annf((Phi1 U Phi2) || G Phi1))
NOTICE: It is wrong to translate the original LTL formula in nnf (also before the translation), because we intuitively assume that the negation in front of variables has a meaning, while in front of temporal operators has another meaning!
After this transformation we can finally translate the formula in LDL following the recursive procedure: tr(Prop) = < Prop > tt (where Prop is a local propositional formula, hence tr(!Prop) = < ! Prop > tt) tr(!!Phi) = tr(Phi) tr(X Phi) = < true > tr(Phi) tr(!X Phi) = ! tr(X Phi) tr(F Phi) = < true * > tr(Phi) tr(! F Phi) = ! tr(F Phi) tr(Phi1 U Phi2) = < (tr(Phi1)? ; true) * > tr(Phi2) tr(!(Phi1 U Phi2)) = !(tr(Phi1 U Phi2)) tr(Phi1 & Phi2) = tr(Phi1) & tr(Phi2) tr(! (Phi1 & Phi2)) = tr( ! Phi1 ) || tr( ! Phi2 ) tr(Phi1 || Phi2) = tr(Phi1) || tr(Phi2) tr(! (Phi1 || Phi2)) = tr( ! Phi1) & tr( ! Phi2)
\ WARNING The markdown syntax may cause errors with < > which is the LDL operator**
The new translation has been implemented in the branch LTL->LDLNewTranslation. Should work properly. But still have to be revised from a theoretical viewpoint.
The new translation works as follows: --- UNTIL --- 1) a U b --> < a * > < b >tt (Giuseppe said it)
2) a U psi --> < a * > psi (me)
3) phi U b --> < (phi? ; true) *> < b >tt (me)
4) phi U psi --> < (phi? ; true) * >psi
--- RELEASE --- (Ottenuto negando l'UNTIL nell'LDL) 1) a R b = !(!a U !b) ma (!a U !b) --> < (!a) * >< !b >tt hence considering outer not [(!a) *] [!b]ff
2) a R psi = !(!a U !psi) ma (!a U !psi) --> < (!a) * > !psi hence considering outer not [ (!a) * ]psi
3) phi R b = !(!phi R !b) ma (!phi R !b) --> < (!phi)? ; true) * > < !b >tt hence considering outer not [ (!phi)? ; true) * ] [ !b ]ff
4) phi R psi = !(!phi U !psi) ma (!phi U !psi) --> < ((!phi)? ; true) * > !psi hence considering outer not [ ((!phi)? ; true) * ]psi
--- GLOBALLY --- G a --> [ true *] [ not a ]ff (Giuseppe said it) (equivalently (false R a) and matches with release's case 1) )
G phi equivalently false R phi hence !(!false U phi) hence equivalent to case 2) then --> [(!false) ]phi = [true \ ]phi
--- EVENTUALLY --- F a --> < true * >< a >tt (Giuseppe) (equivalently (true U a) and matches with until's case 1) )
F phi equivalently true U phi then cequals to case 2) hence --> < true * > phi