Computing maximal weak and other bisimulations. (May 2016)

• Record Type: Journal Article
• Authors: Boulgakov, Alexandre; Gibson-Robinson, Thomas; Roscoe, A.
• Is Part Of: Formal aspects of computing. Volume 28:Number 3(2016)
• Page Start: 381
• Page End: 407
• Publication Date: 2016-05
• Subjects: CSP -- FDR -- Bisimulation -- Strong bisimulation -- Delay bisimulation -- Weak bisimulation -- Labelled transition systems -- Model-checking; Computer science -- Periodicals; 004.05
• DOI: 10.1007/s00165-016-0366-2
• Languages: English
• ISSNs: 0934-5043

Abstract

Abstract We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.