If you have a Kripke structure with just one infinite path, then the path quantifiers don't matter, i.e., E and A become the same, and you can express that in LTL as well. For example, you can check whether your ideas are right as follows using the LTL prover:
First example:
S1 = EF((X(a → b)) ⊕ (a → b))
S2 = EF((a ∧ ¬b) ∧ X(a → b))
You can prove the following to see that you are right:
(!a&b) & (X G(a&!b)) -> F((X(a → b)) ⊕ (a → b))
(!a&b) & (X G(a&!b)) -> !F((a ∧ ¬b) ∧ X(a → b))
and you can see that also with the following traces:
a : 01...
b : 10...
a → b : 10...
X(a → b) : 00...
a ∧ ¬b : 01...
(X(a → b)) ⊕ (a → b) : 10...
(a ∧ ¬b) ∧ X(a → b) : 00...
Second example: First note that G(a⊕b) = ¬F(a↔b), hence, G(a⊕b) ⊕ F(a↔b) is true, so that S1 is always false and we focus on satisfying S2 = XXG((a ⊕ Xa) ∧ (b ⊕ XXb)). I think that you are wrong due to the following traces:
a : 00 11
b : 00 11
Xa : 01 11
a⊕Xa : 01 00
XXb : 11 11
b⊕XXb : 11 00
(a⊕Xa)∧(b⊕XXb) : 01 00
Third example: I guess these were SU (?):
S1 = c ∧ F[b SU G(¬a ↔ X a)]
S2 = c ∧ [(F b) SU G(¬a ↔ X a)]
a : 00 11
b : 00 00
c : 10 00
Xa : 01 11
¬a↔Xa : 01 00
G(¬a↔Xa) : 00 00
and thus the SU will be false.
Maybe I made mistakes, please check!