Name
Abstract | ||
|---|---|---|
We present and compare several algorithms for computing the maximal strong bisimulation, themaximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulationof a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well asthe operational semantics of programs in other languages with operational semantics described by suchGLTSs and relying only on observational equivalence. They can therefore be used to combat the spaceexplosion problem faced in explicit model checking for such languages. We concentrate on algorithms whichwork efficiently when implemented rather than on ones which have low asymptotic growth. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/s00165-016-0366-2 | Formal Asp. Comput. |
Keywords | Field | DocType |
CSP, FDR, Bisimulation, Strong bisimulation, Delay bisimulation, Weak bisimulation, Labelled transition systems, Model-checking | Transition system,Operational semantics,Model checking,Computer science,Observational equivalence,Theoretical computer science,Bisimulation,Semantics | Journal |
Volume | Issue | ISSN |
28 | 3 | 1433-299X |
Citations | PageRank | References |
0 | 0.34 | 16 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexandre Boulgakov | 1 | 79 | 3.72 |
| Thomas Gibson-Robinson | 2 | 105 | 10.12 |
| A. W. Roscoe | 3 | 31 | 25.90 |