In earlier work, we have shown that two variants of weak fairness can be expressed comparatively easily in the timed process algebra PAFAS. To demonstrate the usefulness of these results, we complement work by Walker [11] and study the liveness property of Dekker’s mutual exclusion algorithm within our process algebraic setting. We also present some results that allow to reduce the state space of the PAFAS process representing Dekker’s algorithm, and give some insight into the representation of fair behaviour in PAFAS
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
Titolo: | Checking a Mutex Algorithm in a Process Algebra with Fairness |
Autori: | |
Data di pubblicazione: | 2006 |
Abstract: | In earlier work, we have shown that two variants of weak fairness can be expressed comparatively easily in the timed process algebra PAFAS. To demonstrate the usefulness of these results, we complement work by Walker [11] and study the liveness property of Dekker’s mutual exclusion algorithm within our process algebraic setting. We also present some results that allow to reduce the state space of the PAFAS process representing Dekker’s algorithm, and give some insight into the representation of fair behaviour in PAFAS |
Handle: | http://hdl.handle.net/11581/202316 |
ISBN: | 9783540373766 |
Appare nelle tipologie: | Contributo in atto di convegno su volume |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.