RECORD
Enabling Preserving Bisimulation Equivalence
Logic in Computer Science · Submitted 31 Jul 2021
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. | background 1.00 | 0.05 | 0.02 | asserted 0.98 |
| s1 | On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. | background 0.66 | 0.09 | 0.05 | asserted 0.92 |
| s2 | To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. | contribution 1.00 | 0.94 | 0.24 | asserted 1.00 |
| s3 | We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition. | result 0.94 | 0.96 | 0.81 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.
Human review
How the literature uses it
2 arXiv papers cite this in 2 sentences
What it cites · 6 sentences without a confident label
Cites as support 1 paper
-
Despite being commonly used, it has been argued that most fairness assumptions, including weak and strong fairness of instructions, are often too strong or unrealistic, “in the sense that run-of-the-mill implementations tend not to be fair” [ref] .
Progress, Justness and Fairness · Introduction · 0.96
Cites as background 1 paper
-
For decades, researchers have developed notions of fairness and used them in both system specification and verification; the most common ones are surveyed in [ref] .
Progress, Justness and Fairness · Introduction · 1.00
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.