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

Formale Metadaten

Titel
An O(m log n) algorithm for branching bisimilarity on labelled transition systems
Serientitel
Anzahl der Teile
22
Autor
Mitwirkende
Lizenz
CC-Namensnennung 3.0 Deutschland:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
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.
Schlagwörter