2026-07-20T05:10:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23968 2025-11-12T13:25:07Z ddc:004 open_access

A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity Groote, Jan Friso Jansen, David N. Algorithm Branching bisimulation Partition refinement of states We present a new O(mlog n) algorithm to calculate branching bisimulation equivalence, which is the finest commonly used behavioural equivalence on labelled transition systems that takes the internal action τ into account. This algorithm combines the simpler data structure of an earlier algorithm for Kripke structures (without action labels) with the memory-efficiency of a later algorithm partitioning sets of labelled transitions. It employs a particularly elegant four-way split of blocks of states, which refines a block under two splitters and isolates all new bottom states, simultaneously. Benchmark results show that this new algorithm outperforms the best known algorithm for branching bisimulation both in time and space. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan Friso Groote and David N. Jansen 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.18 urn:nbn:de:0030-drops-239688 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.18 eng https://creativecommons.org/licenses/by/4.0/legalcode