Formal theory of state loss of Siphon-based deadlock prevention

Deadlocks stop a system completely, leading to significant financial loss to a company. Uzam and Zhou propose selecting first-met bad marking (FBM) from the reachability graph of a given Petri net model. A monitor (hence a P-invariant) is added and marked with the number of tokens less than the sum of tokens in all marked operation places. This causes some live states to no longer be reachable. Piroddi et al. further increase it to maximally permissive states using the set-covering approach. However, there are weighted control (WC) arcs, which are more difficult to analyse than the ordinary control net by Uzam and Zhou. Huang et al. also employ WC near the end of the mixed integer programming (MIP) iteration steps and avoid reachability analysis (unlike the above two approaches). Experimentally, it runs faster than the above two approaches. However, all WC places are redundant. To avoid WC while not losing live states, the authors need to understand why state loss occurs. This study proposes developing a formal theory for state loss.