In: The Journal of Systems and Software, Vol. 11, No. 1, pages 53-69. January 1990.
Abstract: The definition of a class of resource-deadlock prone Petri nets is developed using first-order predicate calculus. From this definition characteristics of resource deadlock can be ascertained. These characteristics form the specifications of a program to be written in Prolog which can detect deadlock in parallel processes represented as Petri nets. An important feature of this class is that it characterizes deadlock in networks that contain nested parallel structures. This methodology allows for the prior detection of deadlock, preventing the need for unecessary overhead in dynamic deadlock detection.
Keywords: formal specification; resource deadlock; predicate calculus; Prolog.
Back to the Petri Nets Bibliography