Process theory for supervisory control with partial observation of events and states

We present a process theory that can specify supervisory control feedback loops comprising nondeterministic plants and supervisors with event- and state-based observations. To be able to specify state-based observations we employ the notion of propositional root signal emissions and observation. States of the plant `emit' propositional signals that can be observed by the supervisor by conditioned synchronizing event, thus enforcing supervision by state-based observations. We revisit the notion of partial observation of events and states, which expresses that the supervisor cannot distinguish between traces containing the same observable, but different unobservable events, or between a set of given signals. Existence of a supervisor in such a setting is characterized by the notion of partial bisimilarity, which imposes conditions on the plant and the desired behavior. We give an alternative characterization with respect to the observational power of the supervisor by structurally restricting the form of the supervisor and show that both notions coincide in the deterministic setting.