Stuttering equivalence is too slow

Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in \(\mathcal{O}(m \log n)\) time. Unfortunately, the algorithm does not always meet the acclaimed running time. In this paper, we present two counterexamples...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2016-09
Main Authors: Jansen, David N, Keiren, Jeroen J A
Format: Article
Language:English
Subjects:
Algorithms
Equivalence
Run time (computers)
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in \(\mathcal{O}(m \log n)\) time. Unfortunately, the algorithm does not always meet the acclaimed running time. In this paper, we present two counterexamples where the algorithms uses \(\Omega(md)\) time. A third example shows that the correction is not trivial. In order to analyse the problem we present pseudocode of the algorithm, and indicate the time that can be spent on each part of the algorithm in order to meet the desired bound. We also propose fixes to the algorithm such that it indeed runs in \(\mathcal{O}(m \log n)\) time.
ISSN:2331-8422