Abstract
Fairness is a rich phenomenon: we have weak and strong fairness, and many different variants of those concepts: transition fairness, object/process fairness, actor fairness, position fairness, and so on, associated with specific models or languages, but lacking a common theoretical framework. This work uses rewriting semantics as a common theoretical framework for fairness. A common thread tying together the different fairness variants is the notion of localization: fairness must often be localized to specific entities in a system. For systems specified as rewrite theories localization can be formalized by making explicit the subset of variables in a rule corresponding to the items that must be localized. In this way, localized fairness becomes a parametric notion, that can be easily specialized to model a very wide range of fairness phenomena. After formalizing these concepts and proving basic results, the paper studies in detail both a relative and an absolute LTL semantics for rewrite theories with localized fairness requirements, and shows that it is always possible to pass from the relative to the absolute semantics by means of a theory transformation. This allows using a standard LTL model checker to check properties under fairness assumptions.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 250-263 |
| Number of pages | 14 |
| Journal | Lecture Notes in Computer Science |
| Volume | 3467 |
| State | Published - Sep 26 2005 |
| Event | 16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan Duration: Apr 19 2005 → Apr 21 2005 |
Fingerprint
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Cite this
Localized fairness : A rewriting semantics. / Meseguer, José.
In: Lecture Notes in Computer Science, Vol. 3467, 26.09.2005, p. 250-263.Research output: Contribution to journal › Conference article
}
TY - JOUR
T1 - Localized fairness
T2 - A rewriting semantics
AU - Meseguer, José
PY - 2005/9/26
Y1 - 2005/9/26
N2 - Fairness is a rich phenomenon: we have weak and strong fairness, and many different variants of those concepts: transition fairness, object/process fairness, actor fairness, position fairness, and so on, associated with specific models or languages, but lacking a common theoretical framework. This work uses rewriting semantics as a common theoretical framework for fairness. A common thread tying together the different fairness variants is the notion of localization: fairness must often be localized to specific entities in a system. For systems specified as rewrite theories localization can be formalized by making explicit the subset of variables in a rule corresponding to the items that must be localized. In this way, localized fairness becomes a parametric notion, that can be easily specialized to model a very wide range of fairness phenomena. After formalizing these concepts and proving basic results, the paper studies in detail both a relative and an absolute LTL semantics for rewrite theories with localized fairness requirements, and shows that it is always possible to pass from the relative to the absolute semantics by means of a theory transformation. This allows using a standard LTL model checker to check properties under fairness assumptions.
AB - Fairness is a rich phenomenon: we have weak and strong fairness, and many different variants of those concepts: transition fairness, object/process fairness, actor fairness, position fairness, and so on, associated with specific models or languages, but lacking a common theoretical framework. This work uses rewriting semantics as a common theoretical framework for fairness. A common thread tying together the different fairness variants is the notion of localization: fairness must often be localized to specific entities in a system. For systems specified as rewrite theories localization can be formalized by making explicit the subset of variables in a rule corresponding to the items that must be localized. In this way, localized fairness becomes a parametric notion, that can be easily specialized to model a very wide range of fairness phenomena. After formalizing these concepts and proving basic results, the paper studies in detail both a relative and an absolute LTL semantics for rewrite theories with localized fairness requirements, and shows that it is always possible to pass from the relative to the absolute semantics by means of a theory transformation. This allows using a standard LTL model checker to check properties under fairness assumptions.
UR - http://www.scopus.com/inward/record.url?scp=24944559770&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=24944559770&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:24944559770
VL - 3467
SP - 250
EP - 263
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SN - 0302-9743
ER -