These kind of exercises ask for your intuition and understanding of the formulas even though there are also algorithms that could be used to decide the equivalence and satisfiability of LTL/CTL/CTL* formulas.

Answer to Query 1: In most cases, the structures do only have a single path. Here, CTL* and LTL become the same since the E and A quantifiers can only consider the only existing path. Hence, you can use the LTL tool for checking those formulas (see below).

There is no teaching tool for satisfiability of CTL*, but there is a preliminary tool that you can find under

https://es.cs.uni-kl.de/tools/teaching/PreStructures.html. The tool computes a so-called pre-structure that consists of states and transitions that could satisfy the given formula. You need however check whether it is possible to satisfy the reachability constraints of the formula. Still, the computed structure is often of great help.

Answer to Query 2: As many formulas, the formulas F(a<->b) or GF(a<->b) have more than one model, so that many answers are possible (in general also every bisimular structure to the given one could be used also). Since the LTL tool is only about satisfiability/validity of LTL formulas, you have to describe your single-path structure as an LTL formula. For your second example, this may look as follows:

(!a & !b) & X(a & b) & X X G(a & !b) -> F(a<->b)

If you use

https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html, it will tell you that the above LTL formula is valid and therefore is an example that satisfies F(a<->b). If you try the following

(!a & !b) & X(a & b) & X X G(a & !b) -> G(a<->b)

you will get a counterexample (ignore the _q* variables and it is a path of your structure).

Answer to Query 3: Your idea to get rid of the XX using the two states you mentioned is fine! However, you need to make sure that from s2 onwards one of the formulas without the XX is true while the other (without the XX) is false. That is not the case with your example. Check the following:

(!a & !b) & X(!a & !b) & X X G(a & !b) -> X X (G(a⊕b) ⊕ F(a<->b))

(!a & !b) & X(!a & !b) & X X G(a & !b) -> X X ((G(a⊕b))∨(G(a<->b)))

Note that from s2 onwards, G(a⊕b) holds, and F(a<->b) is false. Thus, G(a⊕b) ⊕ F(a<->b) and also (G(a⊕b))∨(G(a<->b)) are both true.