Synthesis of maximally permissive non-blocking 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 and non-blockingness must be ensured in addition to safety. Our approach is based on the construction of 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 then provide a synthesis algorithm, based on the NB-AIC, that constructs a supervisor that is safe, non-blocking and maximally permissive. This is the first algorithm with such properties.