On Properties of Concurrent System Based on Petri Net Language
Jiang Chang · 2001
In this paper, two language characterizations for weak liveness (free deadlock) and liveness of Petri nets are given. Some language properties of synchronous composed Petri nets are discussed. Based on Petri net language, a necessary and sufficient condition is given for live Petri net (bounded), and then the liveness presevation in a synchronous composed net is studied and a necessary and sufficient condition is obtained. Those results give a formal language method for net liveness testing and liveness controlling.