6
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ The least fixed point is the empty relation right? $\endgroup$
    – Janmar
    Oct 23, 2021 at 12:40

1 Answer 1

2
+25
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.