Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable

Research output: Contribution to conferencePaper

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 languageEnglish (US)
Pages548-553
Number of pages6
StatePublished - Jan 1 1996
EventProceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design - Dearborn, MI, USA
Duration: Sep 15 1996Sep 18 1996

Other

OtherProceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design
CityDearborn, MI, USA
Period9/15/969/18/96

Fingerprint

Petri nets
Dynamical systems
Fires

ASJC Scopus subject areas

  • Computer Science(all)
  • Engineering(all)

Cite this

Sreenivas, R. S. (1996). Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable. 548-553. Paper presented at Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design, Dearborn, MI, USA, .

Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable. / Sreenivas, Ramavarapu S.

1996. 548-553 Paper presented at Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design, Dearborn, MI, USA, .

Research output: Contribution to conferencePaper

Sreenivas, RS 1996, 'Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable' Paper presented at Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design, Dearborn, MI, USA, 9/15/96 - 9/18/96, pp. 548-553.
Sreenivas RS. Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable. 1996. Paper presented at Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design, Dearborn, MI, USA, .
Sreenivas, Ramavarapu S. / Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable. Paper presented at Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design, Dearborn, MI, USA, .6 p.
@conference{9f819f85fd4448e182d6451f18de5b09,
title = "Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable",
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.",
author = "Sreenivas, {Ramavarapu S}",
year = "1996",
month = "1",
day = "1",
language = "English (US)",
pages = "548--553",
note = "Proceedings of the 1996 IEEE International Symposium on Computer-Aided Control System Design ; Conference date: 15-09-1996 Through 18-09-1996",

}

TY - CONF

T1 - Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable

AU - Sreenivas, Ramavarapu S

PY - 1996/1/1

Y1 - 1996/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0029726727&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0029726727&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:0029726727

SP - 548

EP - 553

ER -