The function Tp2Od translates LTL formulas to LO1 which is the opposite direction. The exercise mentioned above shall translate an LO1 formula to LTL. In general, that is quite difficult, and algorithms for this problem are quite complex.
However, when you consider the formula, you will find patterns that occur in the definition of the semantics of the temporal logic operators (see chapter temporal logic). For instance, formula G p holds at time t0 iff
∀t1 (t0≤t1 → p(t1))
and [c SU b] holds at time t1 iff
∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → c[t2])) ∧ b[t0]
and thus, you can see that G(a | [c SU b]) is equivalent to
∀t1. (t0≤t1 → (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → c[t2])) ∧ b[t0]) ∨ a[t1])
So, while you cannot apply function Tp2Od, you may think of which LTL formula has been translated by that function to the given LO1 formula. To that end, you have to match the patterns of the result of the Tp2Od formula to the given formula.
