Enforcing the liveness of S⁴PR by using the approach of allocating resources

Liveness is very important for resource allocation systems (RASs) as it means that no deadlock can arise in the system operation. By applying the approach of allocating resources, this paper focuses on enforcing the liveness of RASs that allow for the general resource allocation and flexible routs. These considered RASs can be modeled by a subcalss of systems of sequential systems with shared resources, named as S⁴PRs. Deadlocks in S⁴PR can be characterized by the saturation of a kind of activity-circuits. Based on these circuits, we study the relationship between the number of initial tokens or marking of resource place and the non-saturation of some involved activity-circuits. Further, a liveness condition for S⁴PR is derived which is associated with the numbers of initial tokens or markings of all resource places. An algorithm is proposed to allocate the initial number of resources so that the considered S⁴PR is live. Finally the proposed method is illustrated by examples.