Computing Stuttering Simulations

DOI10.1007/978-3-642-04081-8_36MaRDI QIDQ3184698zbMATH OpenOpenAlexFDO

Authors Francesco Tapparo, Francesco Ranzato

Publication date 22 October 2009

Published in CONCUR 2009 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0904.1488

Mathematics Subject Classification ID

Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Characterization and verification of stuttering equivalence
• An O(m n) algorithm for computing stuttering equivalence and branching bisimulation
• An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
• scientific article; zbMATH DE number 177845

Cites work

• Characterizing finite Kripke structures in propositional temporal logic
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Generalizing the Paige-Tarjan algorithm by abstract interpretation
• scientific article; zbMATH DE number 177845 (Why is no real title available?)
• scientific article; zbMATH DE number 1306878 (Why is no real title available?)
• Introduction to algorithms
• Three logics for branching bisimulation

Cited in

(6)

• Investigating single-type structural elements of a component Petri net during component modeling and analysis of a complex system with parallelism
• The stuttering principle revisited
• Algebraic stuttering simulations
• Cooking Your Own Parity Game Preorders Through Matching Plays
• Model Checking Software
• Game-theoretic simulation checking tool

This page was built for publication: Computing Stuttering Simulations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3184698)