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

  • General Computer Science
  • General Engineering

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