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. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/978-3-319-11737-9_2 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Transition system,Operational semantics,Model checking,Computer science,Observational equivalence,Theoretical computer science,Bisimulation,Equivalence class,Semantics | Conference | 8829 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.42 |
References | Authors | |
10 | 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 |