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

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?

• The least fixed point is the empty relation right? Oct 23, 2021 at 12:40

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\})$$
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.