An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation

DOI10.1145/3060140zbMath1367.68211OpenAlexW2663462053MaRDI QIDQ5278211

Jan Friso Groote, Jeroen J. A. Keiren, David N. Jansen, Anton Wijs

Publication date: 13 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3060140

zbMATH Keywords

algorithmbranching bisimulationstuttering equivalence

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types, An efficient algorithm to determine probabilistic bisimulation, Geometric Model Checking of Continuous Space, Unnamed Item, Parity game reductions, Probabilistic bisimulation for realistic schedulers, Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications, Unnamed Item, Back-and-forth in space: on logics and bisimilarity in closure spaces, Equivalence checking 40 years after: a review of bisimulation tools, Minimisation of spatial models using branching bisimilarity, Cartesian difference categories, Unnamed Item, From generic partition refinement to weighted tree automata minimization, An O(m log n) algorithm for branching bisimilarity on labelled transition systems, Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities, Unnamed Item, Raiders of the lost equivalence: probabilistic branching bisimilarity, Unnamed Item

Uses Software

• mCRL2
• CADP
• TVT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• CCS expressions, finite state processes, and three problems of equivalence
• An implementation of an efficient algorithm for bisimulation equivalence
• Generalizing the Paige-Tarjan algorithm by abstract interpretation
• Characterizing finite Kripke structures in propositional temporal logic
• A calculus of communicating systems
• Deciding orthogonal bisimulation
• A Cure for Stuttering Parity Games
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• Computation Tree Logic with Deadlock Detection
• Bisimilarity Minimization in O(m logn) Time
• Three Partition Refinement Algorithms
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• Efficient Minimization of DFAs with Partial Transition Functions
• Tools and Algorithms for the Construction and Analysis of Systems
• An Overview of the mCRL2 Toolset and Its Recent Advances