Computing Stuttering Simulations

TL;DR

This paper introduces a novel algorithm for computing the stuttering simulation preorder and equivalence in finite state systems, extending the existing methods for stuttering bisimulation.

Contribution

It provides the first known algorithm for stuttering simulation preorder and equivalence, which were previously not computable.

Findings

Algorithm efficiently computes stuttering simulation preorder.

Algorithm computes stuttering simulation equivalence.

Extends the applicability of behavioral equivalence analysis.

Abstract

Stuttering bisimulation is a well-known behavioral equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preorder induces a coarser behavioral equivalence that preserves the existential fragment ECTL-{X,G}, namely ECTL without the next-time X and globally G operators. While stuttering bisimulation equivalence can be computed by the well-known Groote and Vaandrager's [1990] algorithm, to the best of our knowledge, no algorithm for computing the stuttering simulation preorder and equivalence is available. This paper presents such an algorithm for finite state systems.