Verifying O-observability for Discrete Event Systems under Nondeterministic Observations

In practical systems, due to reasons such as sensor limitations, sensor faults and packet losses in networks, the observations of events become nondeterministic. The supervisory control problem of discrete event systems becomes more complicated. In our previous work, we investigate the supervisory control problem under nondeterministic observations. O-observability is introduced and plays an important role on solving the supervisory control problem. In this paper, we try to find an effective algorithm to check it. By introducing the subset of conflict states, we only need to check the subset of conflict states for every state and each event generated from it. We then construct a transformed automaton which has deterministic observations. Based on the transformed automaton, we find all the invalid strings that violate O-observability. By removing all the invalid strings from the transformed automaton, we obtain an automaton consisting of all valid strings. We show that O-observability holds if and only if the set of all valid strings equals the specification language.