Synthesis of maximally-permissive liveness-enforcing control policies for Gadara petri nets

This paper studies the synthesis of maximally-permissive liveness-enforcing control policies for Gadara nets. Gadara nets are a special class of Petri nets that model allocation of locks in multithreaded computer programs for the purpose of deadlock avoidance. We propose a new control synthesis algorithm that can be used for liveness enforcement of Gadara nets. The algorithm employs structural analysis of the net and synthesizes monitor places to control a special class of siphons, termed resource-induced deadly-marked siphons. We present an iterative control methodology based on this algorithm that converges in a finite number of iterations. The methodology exploits a covering of the unsafe states that is updated at each iteration. Both the proposed algorithm and the associated iterative control methodology are shown to be correct and maximally permissive with respect to the goal of liveness enforcement.