We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

An O(m log n) algorithm for branching bisimilarity on labelled transition systems

Formal Metadata

Title
An O(m log n) algorithm for branching bisimilarity on labelled transition systems
Title of Series
Number of Parts
22
Author
Contributors
License
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
Branching bisimilarity is a behavioural equivalence relation on labelled transition systems (LTSs) that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than ones for other weak behavioural equivalences, especially weak bisimilarity. With m the number of transitions and n the number of states, the classic O(mn) algorithm was recently replaced by an O(m(log |Act| + log n)) algorithm [Groote/Jansen/Keiren/Wijs, ACM ToCL 2017], which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari [PETRI NETS 2009], resulting in a simpler O(m log n) algorithm. Benchmarks show that in practice this algorithm is also faster and often far more memory efficient than its predecessors, making it the best option for branching bisimulation minimisation and preprocessing for calculating other weak equivalences on LTSs.
Keywords