Abstract
We consider discrete-state plants represented by Controlled Petri nets ((CtlPNs) cf. [6, 2, 3, 4]). A supervisory policy can be thought as an implicitly defined table that lists the transitions permitted to fire for each reachable marking. The set of transitions in a CtlPN is partitioned into controllable, and uncontrollable transitions. Any transition in a CtlPN is state-enabled at a given marking if every input place to the said transition has a nonzero token-load. Similarly, a transition in a CtlPN is control-enabled at a given marking if the supervisory policy permits the firing of the said transition. Uncontrollable transitions are always control-enabled, while controllable transition can be control-disabled, if deemed necessary. A transition in a CtlPN has to be state-enabled and control-enabled to fire. The set of valid firing sequences for a given marking is defined accordingly. 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 is control-enabled and state-enabled (cf. level 4 liveness, section 4.1.4, [9]). 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.
Original language | English (US) |
---|---|
Pages | 548-553 |
Number of pages | 6 |
State | Published - 1996 |
Event | Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design - Dearborn, MI, USA Duration: Sep 15 1996 → Sep 18 1996 |
Other
Other | Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design |
---|---|
City | Dearborn, MI, USA |
Period | 9/15/96 → 9/18/96 |
ASJC Scopus subject areas
- General Computer Science
- General Engineering