Polynomial Synthesis of Supervisor for Partially Observed Discrete-Event Systems by Allowing Non-determinism in Control

摘要

We study the supervisory control of discrete-event systems (DESs) under partial observation using non-deterministic supervisors. We formally define a non-deterministic control policy and also a control & observation compatible non-deterministic state machine and prove their equivalence. The control action of a non-deterministic supervisor is chosen online, non-deterministically from among a set of choices determined offline. Also, the control action can be changed online non-deterministically (prior to any new observation) in accordance with choices determined offline. The online choices, once made, can be used to affect the set of control action choices in future. We show that when control is exercised using a non-deterministic supervisor, the specification language is required to satisfy a weaker notion of observability, which we define in terms of recognizability and achievability. Achievability serves as necessary and sufficient condition for the existence of a non-deterministic supervisor, and it is weaker than controllability and observability combined. When all events are controllable, achievability reduces to recognizability. We show that both existence, and synthesis of nondeterministic supervisors can be determined polynomially. (For deterministic supervisors, only existence can be determined polynomially.) Both achievability and recognizability are preserved under union, and also under intersection (when restricted over prefix-closed languages). Using the intersection closure property we derive a necessary and sufficient condition for the range control problem for the prefix-closed case. Unlike the deterministic supervisory setting where the complexity of existence is exponential, our existence condition is polynomially verifiable, and also a supervisor can be polynomially synthesized.