0
$\begingroup$

In safety games there are these mathematical notation about greatest fix points and least fix points but I don't get it. How would we describe them plain English without mathematical symbols.

$\endgroup$
  • 3
    $\begingroup$ What's a safety game? A reference might help – Google doesn't. $\endgroup$ – Dave Clarke May 12 '15 at 10:29
  • 3
    $\begingroup$ You're asking a question about mathematics. Concepts in mathematics can't necessarily be described "in plain English without mathematical symbols": that's why the symbols were invented in the first place! $\endgroup$ – David Richerby May 12 '15 at 10:41
  • $\begingroup$ @DaveClarke It's a concept in modal $\mu$-calculus. $\endgroup$ – Pål GD May 12 '15 at 22:49
  • $\begingroup$ @DavidRicherby I disagree with the statement that we invented mathematical symbols because we can't explain them in plain English. Especially, a symbol for greatest fix point is probably possible to explain without using symbols at all. $\endgroup$ – Pål GD May 12 '15 at 22:50
  • 1
    $\begingroup$ @PålGD Feel free to back up that statement by rewriting either of the answers to this question without using symbols. $\endgroup$ – David Richerby May 12 '15 at 22:52
6
$\begingroup$

Probably the most common fixpoint expressions in model checking are things like $\mu X.A\cup(B\cap\circ X)$ and $\nu X.A\cap(B\cup\circ X)$, where $\circ$ is some flavour of "next state" operator. That is, the least $X$ such that $X = A\cup(B\cap\circ X)$, and the greatest $X$ such that $X = A\cap(B\cup\circ X)$, respectively. More generally, we are talking about fixpoints of monotonic set transformers, i.e. functions $P({\cal S})\to P({\cal S})$ operating on the subsets of a given set $\cal S$.

An intuitive way of thinking about least fixpoints is that they represent sets constructed bottom-up using constructors. Suppose you wanted to define the natural numbers as a subset of the reals: $n$ is a natural number iff it is $0$, or the successor of another natural number. This means that $\mathbb{N}$ is a fixpoint of the set transformer $F:S\mapsto\{0\}\cup succ(S)$. This is not enough, though: the set of all real numbers is also such a fixpoint. $\mathbb{N}$ is the least fixpoint, though, meaning that it only contains those elements which it has to in order to be a fixpoint. Computationally, this fixpoint is the limit you obtain by iterating the given set transformer $F$ on the empty set, gradually assembling the elements of $S$, i.e. the limit of $\emptyset,F(\emptyset),F(F(\emptyset)),\dots$.

In the case of $S:=\mu X.A\cup(B\cap\circ X)$ this means that $S$ contains exactly those elements which can reach $A$, satisfying $B$ until they get there; not requiring the least fixpoint would mean that you could additionally have arbitrary $B$-cycles, infinite $B$-paths never satisfying $A$, etc in your set.

For greatest fixpoints, you have the dual situation: the set contains all elements which are not explicitly eliminated by the given conditions. For $S=\nu X.A\cap(B\cup\circ X)$, this includes any element which satisfies $A$, and either also satisfies $B$ or has a successor in $S$. We pick the greatest fixpoint because we want to include everything which doesn't violate the requirements. Otherwise we might end up with an excessively restrictive set (such as the least fixpoint, which is just $A\cap B$ in this case). Computationally, this is the limit you get by iterating the transformer on the full set $\cal{S}$ of states, gradually eliminating all which fail the specification, i.e. the limit of ${\cal S},F({\cal S}),F(F({\cal S})),\dots$.

$\endgroup$
2
$\begingroup$

A fixed point of a function $f$ is a value $x$ such that $f(x)=x$. A function might have no fixed points (e.g., $f(x)=x+1$), a finite number of them (e.g., $f(x)=x^2+x-1$) or infinitely many (e.g., $f(x)=x$ where $x$ comes from some infinite set).

If $x$ comes from a set with an ordering relation, such as $\leq$ on some kind of numbers, or $\subseteq$ on sets and a function $f$ has at least one fixed point, it makes sense to talk about the least or greatest fixed point of $f$ with respect to that ordering. For example, on the real numbers, the fixed points of $f(x)=x^2+x-1$ are $x=\pm 1$: the greatest fixed point is $+1$ and the least fixed point is $-1$.

I suspect the functions you're dealing with aren't functions on the real numbers but the same principles apply.

$\endgroup$
  • 1
    $\begingroup$ If I have a set of nodes in a directed graph and have to find an infinite path. The graph has one Bad Node which cannot be included in the path. So, in such graph, what would a least fix point or greatest fix point mean? $\endgroup$ – kaitlynrutledge May 12 '15 at 10:43
  • $\begingroup$ Fixed point of what? $\endgroup$ – David Richerby May 12 '15 at 10:43

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.