In: Science in China (Series A), Vol. 32, No. 4, pages 459-469. 1989.
Abstract: A concurrent system can be modeled by a Petri net. A live Petri net may have frozen tokens. It is shown that such tokens can be deleted if they are superfluous, and, while they are useful, can be defrozen due to unfair occurrences of transitions, and, finally, some frozen tokens lead to more process.