Synthesis of Maximally Permissive Supervisors for Partially-Observed Discrete-Event Systems

We present new results on the synthesis of safe, non-blocking, and maximally permissive supervisors for partially observed discrete event systems. We consider the case where the legal language is a non-prefix-closed sublanguage of the system language, i.e., non-blockingness must be ensured in addition to safety. To solve this problem, we define a new bipartite transition system, called the Non-blocking All Inclusive Controller (NB-AIC), that embeds all safe and non-blocking supervisors. We present an algorithm for the construction of the NB-AIC and discuss its properties. We obtain the necessary and sufficient conditions for the solvability of the maximally permissive control problem. We then provide a synthesis algorithm, based on the NB-AIC, that constructs a supervisor that is safe, non-blocking and maximally permissive, if one exists. This is the first algorithm with such properties.