DEADLOCKS AND TRAPS IN PETRI NETS AS HORN-SATISFIABILITY SOLUTIONS AND SOME RELATED POLYNOMIALLY SOLVABLE PROBLEMS

Determining whether a given Petri net is live, or bounded, are major issues in Petri net analysis both from theoretical and practical point of views. Many known results from the literature state necessary and/or sufficient conditions for liveness or boundedness in terms of structural properties, for nets with particular valuations on the arcs. They involve a few basic and remarkable substructures such as deadlocks, traps and preconservative components (pcc) which thus appear to play a very fundamental role in the actual dynamic behaviour of nets. However, the problem of designing efficient (polynomial) algorithms for systematically finding such substructures (possibly satisfying additional properties) doesn't seem to have been addressed so far. We show in this paper that by reformulating the conditions defining deadlocks (respectively traps, pcc's) in terms of logic programming problems featuring the special structure known as Hornsatisfiability, polynomial algorithms can be derived for solving the following problems: (i) find a deadlock (respectively trap, pcc) containing a specified subset of places (or decide that the given Petri net does not contain any), (ii) find a minimal deadlock (respectively minimal trap, minimal pcc) containing a specified subset of places, (iii) find a covering of the places by deadlocks (respectively traps, pcc's) or decide that no such covering exists. The approach presented in this paper thus appears to provide an appropriate framework for addressing algorithmic and computational problems related to Petri net analysis. In particular, it has already proved to be a powerful tool for solving recognition problems relating to special classes of Petri nets (e.g. proving Commoner's structural property in polynomial time, see Minoux and Barkaoui 1988). © 1990.