Supervisory Control of Modular Discrete-Event Systems under Partial Observation: Normality

TL;DR

This paper develops methods for synthesizing maximally permissive normal supervisors in modular discrete-event systems under partial observation, ensuring global properties can be achieved through local supervisors, with practical conditions for verification.

Contribution

It introduces the hierarchical concept of modified observation consistency (MOC) and provides verifiable conditions, like all shared events being observable, to ensure local synthesis of global supervisors.

Findings

All shared events being observable guarantees MOC.

The approach successfully synthesizes supervisors for an MRI scanner case study.

Combines normality with controllability for local supervisor synthesis.

Abstract

Complex systems are often composed of many small communicating components called modules. We investigate the synthesis of supervisory controllers for modular systems under partial observation that, as the closed-loop system, realize the supremal normal sublanguage of the specification. We call such controllers maximally permissive normal supervisors. The challenge in modular systems is to find conditions under which the global nonblocking and maximally permissive normal supervisor can be achieved locally as the parallel composition of local normal supervisors. We show that a structural concept of hierarchical supervisory control called modified observation consistency (MOC) is such a condition. However, the algorithmic verification of MOC is an open problem, and therefore it is necessary to find easily-verifiable conditions that ensure MOC. We show that the condition that all shared events are observable is such a condition. Considering specifications, we examine both local specifications, where each module has its own specification, and global specifications. We combine our results for normality with the existing results for controllability to locally synthesize the nonblocking and maximally permissive controllable and normal supervisor. Finally, we illustrate the results on an industrial case study of the patient table of an MRI scanner.