I was reading the following powerpoint here to remember something I studied a long time ago.
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.