Given a set of relations/equations in some logic like LTL would it be possible to find a least fixed point for those equations?
For example take the equations in LTL
$$ P = Play ~\land X(P \cup S)\\ S = Stop \land X(S)$$
These have a least fixed point with $$ P = Play~ W~ Stop\\ S = G~Stop $$
Are there any algorithms for finding fixed points or is this problem undecidable?
In general, we look at fixed-points of monotone functions over lattices, i.e. with some partial ordering over your elements.
If your lattice is complete (it has a least and greatest element, called a bottom $(\bot)$ and a top $(\top)$), and the function whose fixed-point you're trying to find is monotone, then the Knaster-Tarski Theorem says that a fixed-point always exists.
However, finding this fixed-point may be undecidable. For example, in Hoare logic, there is a function whose fixed-point is the weakest-precondition of a loop. But there's no guarantee that this fixed-point can be found, since finding weakest loop invariants is undecidable.
The basic algorithm, which might not halt, is as follows:
X := bottom
while (X =/= f(X):
X = f(X)
return X
However, you can always find a fixed-point using iteration if you have the Ascending Chain Condition, which basically means that there are no infinite increasing chains in your partial order. When you have this, and your function is monotone, the above algorithm will always halt.
If you have some other "upper bound" on a solution size, then you can use it to ensure the above algorithm halts.
In your case, where you have multiple equations, you just make your lattice contain vectors, and find a fixed-point of a multi-dimensional function.
