Computing maximal weak and other bisimulations
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...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Published: |
Springer London
2015
|
| _version_ | 1797100585685614592 |
|---|---|
| author | Roscoe, A Boulgakov, A Gibson-Robinson, T |
| author_facet | Roscoe, A Boulgakov, A Gibson-Robinson, T |
| author_sort | Roscoe, A |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T05:39:37Z |
| format | Journal article |
| id | oxford-uuid:e51ea87a-b676-4f87-a931-4e9125cc7f5e |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:39:37Z |
| publishDate | 2015 |
| publisher | Springer London |
| record_format | dspace |
| spelling | oxford-uuid:e51ea87a-b676-4f87-a931-4e9125cc7f5e2022-03-27T10:21:38ZComputing maximal weak and other bisimulationsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e51ea87a-b676-4f87-a931-4e9125cc7f5eSymplectic Elements at OxfordSpringer London2015Roscoe, ABoulgakov, AGibson-Robinson, TWe 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. |
| spellingShingle | Roscoe, A Boulgakov, A Gibson-Robinson, T Computing maximal weak and other bisimulations |
| title | Computing maximal weak and other bisimulations |
| title_full | Computing maximal weak and other bisimulations |
| title_fullStr | Computing maximal weak and other bisimulations |
| title_full_unstemmed | Computing maximal weak and other bisimulations |
| title_short | Computing maximal weak and other bisimulations |
| title_sort | computing maximal weak and other bisimulations |
| work_keys_str_mv | AT roscoea computingmaximalweakandotherbisimulations AT boulgakova computingmaximalweakandotherbisimulations AT gibsonrobinsont computingmaximalweakandotherbisimulations |