Solving liveness problem for marked nets by exhaustive coverability trees

It is well known that a coverability tree of a Petri net cannot solve reach ability and liveness problems of the net because using symbol omega (infini ty) may lose some information. A solution to this problem is presented for a special kind of Petri net, marked net. With the combination of omega and the increasing/decreasing information of token number, a new kind of covera bility tree of marked nets, called exhaustive coverability tree (ECT), is p roposed. It is shown with an example that an ECT can be used to detect dead lock.