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

Research output: Contribution to journalArticleAcademic

2 Downloads (Pure)

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 et al. with the ideas from Valmari. 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.
Original languageEnglish
Article number1909.10824
Number of pages27
JournalarXiv
Publication statusPublished - 24 Sep 2019

Fingerprint

Data storage equipment

Bibliographical note

Also appeared as CSR-19-03

Cite this

@article{20c35fcd125b42459a57290162cea8d0,
title = "A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems",
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 et al. with the ideas from Valmari. 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.",
author = "Jansen, {David N.} and Groote, {Jan Friso} and Keiren, {Jeroen J.A.} and Anton Wijs",
note = "Also appeared as CSR-19-03",
year = "2019",
month = "9",
day = "24",
language = "English",
journal = "arXiv",
publisher = "Cornell University Library",

}

A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems. / Jansen, David N.; Groote, Jan Friso; Keiren, Jeroen J.A.; Wijs, Anton.

In: arXiv, 24.09.2019.

Research output: Contribution to journalArticleAcademic

TY - JOUR

T1 - A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems

AU - Jansen, David N.

AU - Groote, Jan Friso

AU - Keiren, Jeroen J.A.

AU - Wijs, Anton

N1 - Also appeared as CSR-19-03

PY - 2019/9/24

Y1 - 2019/9/24

N2 - 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 et al. with the ideas from Valmari. 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.

AB - 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 et al. with the ideas from Valmari. 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.

M3 - Article

JO - arXiv

JF - arXiv

M1 - 1909.10824

ER -