Stuttering equivalence is too slow!

TL;DR

This paper critically examines a claimed efficient algorithm for deciding stuttering equivalence, providing counterexamples, analyzing its inefficiencies, and proposing fixes to ensure it runs within the intended time complexity.

Contribution

The paper identifies flaws in Groote and Wijs's algorithm, offers detailed analysis, and proposes modifications to achieve the claimed $ ext{O}(m ext{ log } n)$ runtime.

Findings

Counterexamples show the algorithm can use $ ext{Omega}(md)$ time

Analysis reveals where the algorithm's inefficiencies occur

Proposed fixes ensure the algorithm runs in $ ext{O}(m ext{ log } n)$ time

Abstract

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.