Modelling Mutual Exclusion in a Process Algebra with Time-outs
Logic in Computer Science
2023-08-16 v2
Abstract
I show that in a standard process algebra extended with time-outs one can correctly model mutual exclusion in such a way that starvation-freedom holds without assuming fairness or justness, even when one makes the problem more challenging by assuming memory accesses to be atomic. This can be achieved only when dropping the requirement of speed independence.
Cite
@article{arxiv.2106.12785,
title = {Modelling Mutual Exclusion in a Process Algebra with Time-outs},
author = {Rob van Glabbeek},
journal= {arXiv preprint arXiv:2106.12785},
year = {2023}
}
Comments
Mild revision in response to I&C reviewing, with added conclusion. arXiv admin note: text overlap with arXiv:2008.13357