On automatically explaining bisimulation inequivalence

DOI10.1007/BFB0023750MaRDI QIDQ4037401zbMATH OpenFDO

Authors Rance Cleaveland

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0023750

zbMATH Keywords

bisimulation equivalenceHennessy-Milner logicKanellakis-Smolka bisimulation algorithmverifying finite-state systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An implementation of an efficient algorithm for bisimulation equivalence
• scientific article; zbMATH DE number 2020181
• Deciding bisimulation equivalences for a class of non-finite-state programs
• Deciding bisimulation equivalences for a class of non-finite-state programs
• On the proof method for bisimulation
• An efficient algorithm for computing bisimulation equivalence
• Tools and Algorithms for the Construction and Analysis of Systems
• On the bisimulation proof method
• Deriving bisimulation relations from path based equivalence checkers

Cited in

(18)

• Constructive logical characterizations of bisimilarity for reactive probabilistic systems
• Exploring probabilistic bisimulations. I
• A game for linear-time-branching-time spectroscopy
• Fixpoint theory -- upside down
• Bisimulation for labelled Markov processes
• Process algebra and model checking
• scientific article; zbMATH DE number 177261 (Why is no real title available?)
• Bisimulation and Hennessy-Milner logic for generalized synchronization trees
• Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence
• Deciding all behavioral equivalences at once: a game for linear-time-branching-time spectroscopy
• Generating diagnostic information for behavioral preorders
• Fixpoint Theory -- Upside Down
• Equivalence checking 40 years after: a review of bisimulation tools
• Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities
• Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable
• Minimal depth distinguishing formulas without until for branching bisimulation
• The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
• Quantitative graded semantics and spectra of behavioural metrics

This page was built for publication: On automatically explaining bisimulation inequivalence

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