Bisimulation and the Knaster–Tarski theorem: What does the least fixed point mean?

Question

Given a suitable lattice and a monotonic function $F$, we can compute the bisimilarity of a labeled transition system (its greatest bisimulation) by computing the greatest fixed point of $F$ using Knaster–Tarski. I was wondering if the least fixed point of $F$ has any meaning to us or if it's worth computing. It is clearly not the smallest bisimulation, so what does it mean?

Answer 1

Let me start by pointing out that, as Janmar mentioned, an empty set is always the least fixed point of $F$. But since bisimulation is often required to be non-empty (to avoid the silly situation that every two transition systems are bisimilar), it makes sense to re-define $F$ as a mapping

$$F^*:(\mathcal{P}(S\times S) \backslash \{\varnothing\}) \to (\mathcal{P}(S\times S) \backslash \{\varnothing\})$$

Now, the simple reason that people compute greatest fixed point instead of least fixed point is that the least fixed point doesn't always exists. To see this, consider (for instance) the following transition systems:

1. $(\{p_0,p_1,p_2,p_3\},\{\alpha\},\{(p_0,\alpha,p_1),(p_2,\alpha,p_3)\})$
2. $(\{q_0,q_1,q_2,q_3\},\{\alpha\},\{(q_0,\alpha,q_1),(q_2,\alpha,q_3)\})$

Viewing these transition systems as disjoint unions of two smaller transition systems, there is a bisimulation $R_1 = \{(p_0,q_0),(p_1,q_1)\}$ between the transition systems $(\{p_0,p_1\},\{\alpha\},\{(p_0,\alpha,p_1)\})$ and $(\{q_0,q_1\},\{\alpha\},\{(q_0,\alpha,q_1)\})$, and there is also a bisimulation $R_2 = \{(p_2,q_2),(p_3,q_3)\}$ between $(\{p_2,p_3\},\{\alpha\},\{(p_2,\alpha,p_3)\})$ and $(\{q_2,q_3\},\{\alpha\},\{(q_2,\alpha,q_3)\})$. Both of these are fixed points of $F^*$, and furthermore $R_1 \cap R_2 = \varnothing$. Thus $F^*$ does not have, in this case, a least fixed point.

More generally (and loosely) speaking, the various fixed points of $F^*$ can be interpretated as bisimulations between local parts of the relevant transition systems.