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

David N. Jansen; Jan Friso Groote; Jeroen J.A. Keiren; Anton Wijs

doi:10.1007/978-3-030-45237-7_1

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

David N. Jansen, Jan Friso Groote, Jeroen J.A. Keiren, Anton Wijs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

15 Citations (Scopus)

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, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari resulting in a simpler O(m log n) algorithm.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II
Editors	Armin Biere, David Parker
Publisher	Springer
Pages	3-20
Number of pages	18
ISBN (Print)	9783030452360
DOIs	https://doi.org/10.1007/978-3-030-45237-7_1
Publication status	Published - 2020
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12079 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Funding

erated and analysed during the current study are available in the figshare repository: https://doi.org/10.6084/m9.figshare.11876688.v1. This work is partly done during a visit of the first author at Eindhoven University of Technology, and a visit of the second author at the Institute of Software, Chinese Academy of Sciences. The first author is supported by the National Natural Science Foundation of China, Grant No. 61761136011.

Funders	Funder number
National Natural Science Foundation of China	61761136011
Chinese Academy of Sciences, Beijing
Eindhoven University of Technology

Keywords

Algorithm
Branching bisimilarity
Labelled transition systems

Access to Document

10.1007/978-3-030-45237-7_1

Cite this

Jansen, D. N., Groote, J. F., Keiren, J. J. A., & Wijs, A. (2020). An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II (pp. 3-20). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS). Springer. https://doi.org/10.1007/978-3-030-45237-7_1

Jansen, David N. ; Groote, Jan Friso ; Keiren, Jeroen J.A. et al. / An O(m log n) algorithm for branching bisimilarity on labelled transition systems. Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. editor / Armin Biere ; David Parker. Springer, 2020. pp. 3-20 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d002ba9d3e064b19b097a2e0cc98baea,

title = "An O(m log n) algorithm for branching bisimilarity on labelled transition systems",

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, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari resulting in a simpler O(m log n) algorithm.",

keywords = "Algorithm, Branching bisimilarity, Labelled transition systems",

author = "Jansen, {David N.} and Groote, {Jan Friso} and Keiren, {Jeroen J.A.} and Anton Wijs",

year = "2020",

doi = "10.1007/978-3-030-45237-7_1",

language = "English",

isbn = "9783030452360",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--20",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II",

address = "Germany",

note = "26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

}

Jansen, DN , Groote, JF , Keiren, JJA & Wijs, A 2020, An O(m log n) algorithm for branching bisimilarity on labelled transition systems. in A Biere & D Parker (eds), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12079 LNCS, Springer, pp. 3-20, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45237-7_1

An O(m log n) algorithm for branching bisimilarity on labelled transition systems. / Jansen, David N.; Groote, Jan Friso ; Keiren, Jeroen J.A. et al.
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. ed. / Armin Biere; David Parker. Springer, 2020. p. 3-20 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - An 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

PY - 2020

Y1 - 2020

N2 - 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, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari resulting in a simpler O(m log n) algorithm.

AB - 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, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari resulting in a simpler O(m log n) algorithm.

KW - Algorithm

KW - Branching bisimilarity

KW - Labelled transition systems

UR - http://www.scopus.com/inward/record.url?scp=85083970192&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45237-7_1

DO - 10.1007/978-3-030-45237-7_1

M3 - Conference contribution

AN - SCOPUS:85083970192

SN - 9783030452360

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 20

BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

Jansen DN , Groote JF , Keiren JJA , Wijs A. An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In Biere A, Parker D, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Springer. 2020. p. 3-20. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45237-7_1