Stuttering bisimulation is a well-known behavioural equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preorder induces a coarser behavioural 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 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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Ranzato, F., & Tapparo, F. (2009). Computing stuttering simulations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5710 LNCS, pp. 542–556). https://doi.org/10.1007/978-3-642-04081-8_36
Mendeley helps you to discover research relevant for your work.