Linear parallel algorithms to compute strong and branching bisimilarity

Jan Martens; Jan Friso Groote; Lars B.van den Haak; Pieter Hijma; Anton Wijs

doi:10.1007/s10270-022-01060-7

Linear parallel algorithms to compute strong and branching bisimilarity

Jan Martens^*, Jan Friso Groote, Lars B.van den Haak, Pieter Hijma, Anton Wijs

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions and | Act| action labels, we introduce an algorithm that decides strong bisimilarity in O(n+ | Act|) time on max (n, m) processors and an algorithm that decides branching bisimilarity in O(n+ | Act|) time using up to max (n², m, | Act| n) processors.

Original language	English
Pages (from-to)	521-545
Number of pages	25
Journal	Software and Systems Modeling
Volume	22
Issue number	2
Early online date	6 Dec 2022
DOIs	https://doi.org/10.1007/s10270-022-01060-7
Publication status	Published - Apr 2023

Bibliographical note

Funding Information:
This work is carried out in the context of the NWO AVVA project 612.001751 and the NWO TTW ChEOPS project 17249. We thank the reviewers for their careful reviews and helpful comments.

Publisher Copyright:
© 2022, The Author(s).

Funding

This work is carried out in the context of the NWO AVVA project 612.001751 and the NWO TTW ChEOPS project 17249. We thank the reviewers for their careful reviews and helpful comments.

Funders	Funder number
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	17249, 612.001751
Nederlandse Organisatie voor Wetenschappelijk Onderzoek

Keywords

Branching bisimulation
Parallel algorithms
PRAM
RCPP
Strong bisimulation

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/s10270-022-01060-7

Persistent URL (handle)

Persistent link

Cite this

@article{b65288b8fb61465e90de3f72e29c9f68,

title = "Linear parallel algorithms to compute strong and branching bisimilarity",

abstract = "We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions and | Act| action labels, we introduce an algorithm that decides strong bisimilarity in O(n+ | Act|) time on max (n, m) processors and an algorithm that decides branching bisimilarity in O(n+ | Act|) time using up to max (n2, m, | Act| n) processors.",

keywords = "Branching bisimulation, Parallel algorithms, PRAM, RCPP, Strong bisimulation",

author = "Jan Martens and Groote, {Jan Friso} and Haak, {Lars B.van den} and Pieter Hijma and Anton Wijs",

note = "Funding Information: This work is carried out in the context of the NWO AVVA project 612.001751 and the NWO TTW ChEOPS project 17249. We thank the reviewers for their careful reviews and helpful comments. Publisher Copyright: {\textcopyright} 2022, The Author(s).",

year = "2023",

month = apr,

doi = "10.1007/s10270-022-01060-7",

language = "English",

volume = "22",

pages = "521--545",

journal = "Software and Systems Modeling",

issn = "1619-1366",

publisher = "Springer",

number = "2",

}

TY - JOUR

T1 - Linear parallel algorithms to compute strong and branching bisimilarity

AU - Martens, Jan

AU - Groote, Jan Friso

AU - Haak, Lars B.van den

AU - Hijma, Pieter

AU - Wijs, Anton

N1 - Funding Information: This work is carried out in the context of the NWO AVVA project 612.001751 and the NWO TTW ChEOPS project 17249. We thank the reviewers for their careful reviews and helpful comments. Publisher Copyright: © 2022, The Author(s).

PY - 2023/4

Y1 - 2023/4

N2 - We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions and | Act| action labels, we introduce an algorithm that decides strong bisimilarity in O(n+ | Act|) time on max (n, m) processors and an algorithm that decides branching bisimilarity in O(n+ | Act|) time using up to max (n2, m, | Act| n) processors.

AB - We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions and | Act| action labels, we introduce an algorithm that decides strong bisimilarity in O(n+ | Act|) time on max (n, m) processors and an algorithm that decides branching bisimilarity in O(n+ | Act|) time using up to max (n2, m, | Act| n) processors.

KW - Branching bisimulation

KW - Parallel algorithms

KW - PRAM

KW - RCPP

KW - Strong bisimulation

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

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

U2 - 10.1007/s10270-022-01060-7

DO - 10.1007/s10270-022-01060-7

M3 - Article

AN - SCOPUS:85143387594

SN - 1619-1366

VL - 22

SP - 521

EP - 545

JO - Software and Systems Modeling

JF - Software and Systems Modeling

IS - 2

ER -

Linear parallel algorithms to compute strong and branching bisimilarity

Abstract

Bibliographical note

Funding

Keywords

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this