Petri net is a mathematical model for concurrent Systems. Liveness is one of important properties of Petri net. Liveness problem of general Petri net is of exponential space complexity and subclasses are suggested with less computational complexity. It is well known that liveness problem of trap cycle (TC) net and bounded free choice (EFC) net is solved in deterministic polynomial time. It is also known that liveness problem of general (unbounded) EFC net is NP-complete. This paper treats liveness problem of trap containing cycle (TCC), which is a superclass of TC net. Liveness problem of TCC net is shown to be NP-hard by reducing satisfiability problem to the problem Given a TCC net, it is shown to be decidable in deterministic polynomial time whether the net is live and bounded.
展开▼