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?

  • $\begingroup$ Your question is unclear. Wht are $P$ and $S$? What is $X$? It looks like $P$ must be a logical statement and a set at the same time. Please be more specific and describe what is what. $\endgroup$ Apr 11 '15 at 15:55
  • 2
    $\begingroup$ The statements are in LTL logic. Here $P$ and $S$ are variables. $\cup$ was supposed to denote the until operator and $X$ is the next operator. $\endgroup$
    – epsilon_0
    Apr 12 '15 at 14:28

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.