TY - CHAP
T1 - On supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled Petri nets
AU - Sreenivas, Ramavarapu S
PY - 1996
Y1 - 1996
N2 - We consider discrete-state plants represented by Controlled Petri nets ((CtlPNs) cf. [3, 1, 2]). A transition in a CtlPN is live if for every marking reachable under supervision, there exists a valid firing sequence that results in a marking under which the said transition can fire (cf. level 4 liveness, section 4.1.4, [5], [4]). A supervisory policy enforces liveness if every transition in the CtlPN is live under supervision. In this paper we show that the existence of a supervisory policy that enforces liveness for an arbitrary CtlPN is undecidable.
AB - We consider discrete-state plants represented by Controlled Petri nets ((CtlPNs) cf. [3, 1, 2]). A transition in a CtlPN is live if for every marking reachable under supervision, there exists a valid firing sequence that results in a marking under which the said transition can fire (cf. level 4 liveness, section 4.1.4, [5], [4]). A supervisory policy enforces liveness if every transition in the CtlPN is live under supervision. In this paper we show that the existence of a supervisory policy that enforces liveness for an arbitrary CtlPN is undecidable.
UR - http://www.scopus.com/inward/record.url?scp=0030407076&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0030407076&partnerID=8YFLogxK
M3 - Chapter
AN - SCOPUS:0030407076
T3 - Proceedings of the IEEE Conference on Decision and Control
SP - 4439
EP - 4444
BT - Proceedings of the IEEE Conference on Decision and Control
A2 - Anon, null
T2 - Proceedings of the 35th IEEE Conference on Decision and Control. Part 4 (of 4)
Y2 - 11 December 1996 through 13 December 1996
ER -