We are given a labelled directed graph, where both vertices (or states) and edges (or transitions) have labels. Informally, two states are bisimilar when they have the same label and they can simulate each other's transitions. On the states the two states evolve to, the same again is true.

More formally, a binary relation $R \subseteq S \times S$ is a simulation iff $\forall (p,q) \in R$

  • $p$ and $q$ have the same label, and
  • if $p \overset{a}{\longrightarrow} p'$ then $\exists q', q \overset{a}{\longrightarrow} q'$ and $(p',q') \in R$.

A relation $R$ is a bisimulation iff $R$ and $R^{-1}$ are simulations. The largest bisimulation on the given system is called the bisimilarity relation.

There are algorithms for finding the bisimilarity relation, that run in $O(m \log n)$ time and $O(m+n)$ space, where $n$ is the number of states and $m$ the number of transitions. An example is the Paige-Tarjan RCP algorithm from 1987.

However, consider a simpler problem. Instead of finding all the bisimulations, I just want to find a few of them. Can it be done faster than in loglinear time? If so, how? For example, let's say one is given two states $p,q \in S$ such that they have the same label and they can make the same transitions. What I find problematic is to check that the states they lead to are once again bisimulations. In other words, one could also ask if there is a quick way to decide if two given states are a bisimulation.


You can always return the bisimulation $∅$ in constant time.

You are right about the fact that in order to return $R$, you will have at least some sanity checks.

For example you could think that returning all bisimulations of the form $\{(p,q)\}$ when $p$ and $q$ have the same label and such that $p\not→$ and $q\not→$ is easy, but not that much: you need to proceed through $O(m+n)$ time and $O(n)$ space! (Or $O(mn^2)$ time and $O(1)$ space (not counting the output)). Checking that a small relation is a bisimulation is not a lot easier than finding the relation $\sim$.

The computation of $\sim$ uses clever properties specific to $\sim$ and fusing states tricks. These techniques would not be useful for several relations and doing better than $O(m\log n)$ (not loglinear) is hard. Also, computing "a few" bisimulation is of arguable interest.

Another thing: deciding if $p\sim q$ implies computing the relation $\sim$ on the union of the directed graphs $G_p=\{x ∣ p \stackrel{a_1\dots a_n}{\longrightarrow}x\}$ and $G_q=\{x ∣ q \stackrel{b_1\dots b_m}{\longrightarrow}x\}$ which can be a significant part of the graph. If however you know have information like the size of $G_p$ and $G_q$ then you can compute $\sim$ on smaller graphs. Keep in mind that algorithms with Tarjan in their name tend to have very tight bounds. This is not an exception.

| cite | improve this answer | |
  • $\begingroup$ Thank you! Do you know any work on algorithms for finding just a few bisimulations? Or are you aware of applications that would need just a few bisimulations? Can you maybe suggest some further reading? $\endgroup$ – Juho Nov 17 '12 at 6:17
  • $\begingroup$ @Juho: I don't, and I really don't see the point of finding "a few" bisimulations, but maybe there are applications that I'm not aware of. (Usually one only wants to prove that $p\sim q$ or $p\not\sim q$.) $\endgroup$ – jmad Nov 17 '12 at 13:31
  • $\begingroup$ Just a further note. "A few" bisimulations might be easier to find if the graph has a certain structure. For example, the leaves of a tree with the same label are bisimulations (they have an outdegree of zero). $\endgroup$ – Juho Dec 7 '12 at 18: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.