<p>In general, we look at fixed-points of monotone functions over lattices, i.e. with some partial ordering over your elements.</p>

<p>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 <a href="http://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem" rel="nofollow">Knaster-Tarski Theorem</a> says that a fixed-point always exists.</p>

<p>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.</p>

<p>The basic algorithm, which might not halt, is as follows:</p>

<pre><code>X := bottom
while (X =/= f(X):
  X = f(X)
return X
</code></pre>

<p>However, you can always find a fixed-point using iteration if you have the <a href="http://en.wikipedia.org/wiki/Ascending_chain_condition" rel="nofollow">Ascending Chain Condition</a>, 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.</p>

<p>If you have some other "upper bound" on a solution size, then you can use it to ensure the above algorithm halts.</p>

<p>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.</p>

CC BY-SA 3.0
2015-04-12T11:32:37.753Z
2015-04-12T11:32:37.753Z
Joey Eremondi
<p>Given a set of relations/equations in some logic like LTL would it be possible to find a least fixed point for those equations?</p>

<p>For example take the equations in LTL</p>

<p>$$ P = Play ~\land X(P \cup S)\\
   S = Stop \land X(S)$$</p>

<p>These have a least fixed point with 
$$ P = Play~ W~ Stop\\
   S = G~Stop $$</p>

<p>Are there any algorithms for finding fixed points or is this problem undecidable?</p>

CC BY-SA 3.0
2015-04-11T15:55:54.177Z
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.
Andrej Bauer
CC BY-SA 3.0
2015-04-12T14:28:33.463Z
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.
epsilon_0
<lo.logic><temporal-logic><linear-temporal-logic>
Calculating least fixed points in equations
epsilon_0
# Calculating least fixed points in equations

(Asked by: username_0 on 2015-04-11)

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?

**Tags:** lo.logic, temporal-logic, linear-temporal-logic

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2015-04-12. Score: 4 | Accepted answer

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.


---

