We tried this out in Sascha Scherrer's Bachelor's thesis (An Algorithm for Computing Bisimulations in Planning, July 2012). Performance there was somewhat worse than our current implementation, although this may be due to low-level details rather than the algorithm.

According to Silvan, bisimulation is not currently the main bottleneck in M&S, and there has been no movement on this issue since 2011, so I am marking this one as resolved (as in: we are no longer planning to do this).

I think efficiency improvements are likely still possible here, so if someone would be interested in concretely working on this, they could reopen this issue.

Addendum: in some cases, e.g. with "strictly greedy bisimulation" without
zero-cost operators, there are additional structural properties of the
transition system that we might want to exploit. In that case, it is a DAG and
we already know a topological order (by h value), which should allow
significantly more efficient algorithms. (For example, it should be very easy to
make them quite a bit more efficient in terms of space usage.)

Our current bisimulation algorithms are rather inefficient. I haven't read the
literature closely, but I think it's structurally similar to Moore's 1956
algorithm for minimizing DFAs (in "Gedanken-experiments on sequential
machines"); other algorithms for the same problem or related problems include:

 - Hopcroft 1971: "An n log n algorithm for minimizing states in a finite
   automaton" (I could only find the TR for that one)
 - Paige and Tarjan 1987: "Three Partition Refinement Algorithms"
 - Blum 1996: "An O(n log n) implementation of the standard method for
   minimizing n-state finite automata"
 - Dovier et al. 2004: "An efficient algorithm for computing bisimulation
   equivalence"

We could and probably should use one of these algorithms at least in the case
where we do bisimulation without bounds (whether it is exact bisimulation,
"somewhat greedy" or greedy).

We could also try to adapt these algorithms to the size-limited bisimulation
case, but since this might affect the refinement order, it could also affect
which abstraction is computed. A priori, it's not clear whether the effect on
this should be negative or positive, so experiments would be needed in that case.