Jan Friso Groote: A simplified algorithm for branching bisimulation


Event Details


According to my gut feeling the last algorithm for branching bisimulation on labelled transition systems is too complicated and
should be simplified. This talk will present a new algorithm that — although definitely simpler — is still quite complex.
The gut feeling also told me that memory use and speed should both be better in the new algorithm. Unfortunately, this did
not out to be so easy to accomplish in an implementation of the new algorithm, and for a long time the new algorithm was slower
than the old. Things look better now. I will report on the state of affairs with the new algorithm in this talk.

One of the reasons that the old algorithm is hard to beat is that it is already very fast. Both the new and old algorithm are faster
than calculating strongly connected tau-components, which is a linear algorithm, whereas branching bisimulation is O(m log n).
The ‘old’ fast algorithm is the default branching-bisimulation reduction algorithm in the toolset. The new one is experimental
and available with the flag -ebranching-bisim-gj in the tool ltsconvert.