Maximally Permissive Supervisors for Nonblocking Similarity Control of Nondeterministic Discrete-Event Systems

This article investigates a nonblocking similarity control problem for nondeterministic discrete-event systems, which is a problem of synthesizing a nonblocking supervisor such that the supervised system is simulated by the given specification. In this article, the state of the system is not required to be observable, and the event occurrence is allowed to be partially observed. We propose an algorithm that computes a nonblocking supervisor from a possibly blocking one by iteratively removing certain states. Then, we identify two key properties of input supervisors, named state-unmergedness and strong maximal permissiveness, which together guarantee the maximal permissiveness of output nonblocking supervisors. The algorithm is applied to a supervisor with these two properties to obtain a maximally permissive nonblocking supervisor. In addition, we show that a nonblocking supervisor is generated by the algorithm if and only if there exists a solution to the nonblocking similarity control problem.

Automated summary

This article investigates the problem of synthesizing a nonblocking supervisor for nondeterministic discrete-event systems, such that the supervised system follows a given specification. The article proposes an algorithm that converts a possibly blocking supervisor to a nonblocking one by iteratively removing certain states. Additionally, the article identifies key properties for input supervisors that guarantee the maximal permissiveness of the output nonblocking supervisors.