Maximally Permissive Deadlock Avoidance for Resource Allocation Systems with R/W-Locks

This paper extends the existing theory on maximally permissive liveness-enforcing supervision of resource allocation systems (RAS) so that it can handle RAS with reader/writer (R/W-) locks. A key challenge that is posed by this new RAS class stems from the fact that the underlying state space is not necessarily finite. We effectively address this obstacle by taking advantage of special structure that exists in the set of inadmissible states and enables a finite representation of this set through its minimal elements.