Gastvortrag: David Jansen: A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems

Mittwoch, 02.10.2019, 10.30 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E2, Raum 5056

Vortragender: David Jansen

 

Abstract:

Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms 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 has recently been replaced by an O(m log n) algorithm, which is unfortunately rather complex. This paper combines the ideas from [Groote/Jansen/Keiren/Wijs, ACM TOCL 18(2), article 13. 2017] with the ideas from [Valmari, PETRI NETS (LNCS 5606). 2009]. This results in a simpler O(m log n) algorithm. Benchmarks show that this new algorithm is faster and more memory efficient than all its predecessors.