what does the "fixed point" in fixpoint algorithms refer to?

Question

I was reading the following powerpoint here to remember something I studied a long time ago.

http://www.cs.cmu.edu/~emc/15-820A/reading/lecture_1.pdf

the 12th slide is labeled fixpoint algorithms, but I can't seem to find anything that explains what this actually means.

On wikipedia the only thing that comes up is: http://en.wikipedia.org/wiki/Fixed_point_(mathematics) http://en.wikipedia.org/wiki/Fixed-point_iteration

The 2nd one seems most likely.

Basically, from the powerpoint, what is happening is that you start with an empty set, then look for a state in which the condition you are looking for is true, then you backtrack to look for a state that can get to the state in which the condition is true. you keep backtracking and if you eventually find a state that is an initial condition, then you have found a path leading to the condition being true.

However, i still do not know what this has to do with the word "fixed point" or fixed points such that a function f(x) = x.

Perhaps my understanding of symbolic model checking is weak (it's been 3 years), so I would really appreciate some enlightenment.

After some further reading, it appears that the goal is to get the set of all states in this path, and you are done checking when you reach "convergence." My guess is that in this context convergence means that you are no longer finding new states and the set of states leading to condition p (which we call U), converges to the same set of states.

However, I don't see how that relates to a fixed point, it seems more like a fixed set. Still rather confused.

Maybe i'm not understanding what is meant by convergence in the lecture.

Answer 1

I recall it as a solution of a system of discrete equations. It is closely related to the methods of searching a root in continuous space. Hope I am not too far since I used the method long time ago.

It is a point in a multiple dimension space, not a set of points. (One can say it gets a set of scalar values.) If the system gets multiple solution, that is another problem.

Answer 2

The term "fixed point" has many uses, but they share the same idea.

Consider the backward reachability for (symbolic) model checking mentioned in the OP. If doing verification for closed systems (those that everything is controlled -- no environment), then the (safety) property $P$ we are interested in is an undesired one. We want to check if any state in the undesired property is reachable from an initial state.

This computation can be expressed in $\mu$-calculus with the formula $\mu X. P \vee \mathrm{next}(X)$. The operator $\mu$ computes the least fixed point, as follows.

1. Set $X$ is initialized to the empty set $X_0 = \emptyset$.
2. $X$ is assigned $X_1 = P \vee \mathrm{next}(X_0) = P \vee \emptyset = P$
3. if $X_1 \neq X_0$, then again $X$ is assigned $X_2 = P \vee \mathrm{next}(X_1)$
4. iterate similarly, until $X_{i + 1} = X_i$

When the condition $X_{i + 1} = X_i$ holds, then a fixed point has been reached.

Given a mapping (function) $f(x)$, a point $x$ in the domain of $f$ is called fixed point of $f$ if it remains unchanged under $f$, i.e., if $f(x) = x$. In the context of backward reachability, the set $X$ reaches a fixed point with respect to the map $g: 2^S \rightarrow 2^S$ (where $S$ the set of all states) that maps a given set of states $Y \subseteq S$ to the set of states $g(Y) = \mathrm{next}^{-1}(Y) \vee P \subseteq S$ that can reach $Y$ in one time step, or are already in $P$.

By definition of the iterations, it is $X_{i + 1} = \mathrm{next}^{-1}(X_i) \vee P$. So when the fixed point iteration terminates, the condition $X_{i + 1} = X_i$ can be rewritten as $\mathrm{next}^{-1}(X_i) \vee P = X_i \iff g(X_i) = X_i$. So $X_i$ (and $X_{i + 1}$) is a fixed point of the mapping $g$.

The set $X_i$ is called a "point", because it is an element of the domain $2^S$ of function $g$. In the context of reachability, the element $X_i$ just happens to be a set of states. But with respect to $g$, it is a point. In another context, e.g., of the fixed points of a real function $f: \mathbb{R}\rightarrow \mathbb{R}$, the fixed point is a point on the real line.

This particular fixed point is called “least”, because it can be the case that a superset of the set $X_i$ is also a fixed point of the map $g$. For example, if $q$ is a state that has a self-loop, but cannot reach the set $P$, then the set $\{q\} \cup X_i$ is also a fixed point of the function $g$, because $g(\{q\} \cup X_i) = \mathrm{next}^{-1}(\{q\} \cup X_i) \cup P = \mathrm{next}^{-1}(\{q\}) \cup (\mathrm{next}^{-1}(X_i) \cup P) = \{q\} \cup X_i$. Clearly, we are not interested in the fixed point $Q = \{q\} \cup X_i$, because state $q$ does not belong to the ancestors of set $P$. This is why we are looking for the smallest set that is a fixed point of map $g$. The smallest set is “least” in the partial order induced by the subset relation. In order to find it, we have to start from “the bottom”, so with the empty set ($X_0 = \emptyset$). Otherwise, we could first reach some other fixed point (a superset of $X_i$), and get stuck with it.