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

Research output: Contribution to conferencePaperpeer-review

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Engineering(all)

Fingerprint Dive into the research topics of 'Existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled petri nets is undecidable'. Together they form a unique fingerprint.

Cite this