In: Procs. of the European Control Conference, ECC'93, J.W. Nieuwenhuis and C. Praagman and H.L. Trentelman (eds.), Groningen, The Netherlands, pages 513-518. 1993.
Abstract: Competition for limited resources in concurrent systems can lead to deadlock states, a situation that is usually ruled out by the specification of reactive systems. This paper presents some new results concerning the structural analysis of deadlock-freeness using Petri net models. Our approach considers the state equation as the basic description of the behaviour of the net system. Actually, this description is a linear relaxation, so, in general, it leads to necessary or sufficient conditions on certain behavioural properties of the system. Nevertheless, the method is useful to uncover possible design errors leading to deadlock states, or to prove absence of such problems, and it can greatly reduce the space and time cost associated with the classical techniques based on reachability or even on the computation of the set of minimal invariants.