In: Jensen, K.: Lecture Notes in Computer Science, Vol. 616; 13th International Conference on Application and Theory of Petri Nets 1992, Sheffield, UK, pages 134-153. Springer-Verlag, June 1992.
Abstract: A net is called well-formed if it can be marked with a live and bounded marking. The Rank Theorem characterises well-formed extended free choice nets, employing only the linear algebraic representation of a net. The paper presents a proof of the Rank Theorem which is based on the characterisation of liveness by deadlocks and traps and the coverability of well-formed extended free choice nets by S- and T-components. Consequences of the Rank Theorem include the Duality Theorem, a polynomial algorithm for deciding well-formedness, and simple proofs of other results concerning extended free choice nets. Moreover, the Rank Theorem implies a sufficient condition for liveness which applies to arbitrary nets.