One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915030810755072 |
|---|---|
| author | Bisping, Benjamin Jansen, David N. |
| author_facet | Bisping, Benjamin Jansen, David N. |
| contents | We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic that we characterize by eight dimensions of formula expressiveness. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_14584 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics Bisping, Benjamin Jansen, David N. Logic in Computer Science F.4.1; F.3.2 We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic that we characterize by eight dimensions of formula expressiveness. |
| title | One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics |
| topic | Logic in Computer Science F.4.1; F.3.2 |
| url | https://arxiv.org/abs/2411.14584 |