Configuration of liveness-enforcing initial marking with the minimum resources for resource allocation systems

• Published in: Information sciences 2025-02, Vol.691, p.121623, Article 121623
• Main Authors: Feng, Yanxiang, Ren, Sida, Xing, Keyi, Yang, Yikang, Zhou, MengChu
• Format: Article
• Language: English
• Subjects: Liveness-enforcing initial markings; Minimum marking configuration; Petri nets; Resource allocation systems
• ISSN: 0020-0255
• DOI: 10.1016/j.ins.2024.121623

The enforcement of liveness is crucial for Petri nets models of resource allocation systems (RASs). It is interesting yet very challenging to establish an initial marking for Petri net plants so that the net is live. Such an initial marking is referred to as liveness-enforcing initial marking (LIM). Despite existing literature presenting various LIMs, no studies have addressed the issue of minimizing the number of resources in an LIM. This work focuses on designing an LIM with the minimum resources (LIM-MR) for a class of Petri nets called systems of sequential systems with shared resources (S4PRs) by assigning a token capacity to each resource place, such that the sum of all involved resources is minimized. This work first establishes a kind of necessary and sufficient liveness condition for S4PR, which is then encoded into a series of variables and constraints in a mixed-integer programming (MIP) formulation. Although LIM-MR may not be unique, solving the proposed MIP formulation can obtain at least one LIM-MR for S4PR under consideration. The experimental results show the solvability of this approach for S4PRs.