Coinduction in control of partially observed discrete-event systems

Coalgebra and coinduction provide new results and insights for the supervisory control of discrete-event systems (DES) with partial observations. In the case of full observations, coinduction has been used to define a new operation on languages called supervised product, which represents the language of the closed-loop system. The first language acts as a supervisor and the second as an open-loop system (plant). We show first that the supervised product is equal to the infimal controllable superlanguage of the supervisor's (specification) language with respect to the plant language. This can be generalized to the partial observation case, where the supervised product is shown to be equal to the infimal controllable and observable superlanguage. There are two different control laws for partially observed DES, that give the same closed-loop system if the specification is observable: permissive and antipermissive. A variation on the supervised product is presented, which corresponds to the control policy with the issue of of observability separated from the issue of controllability. It is shown to be equal to the infimal observable superlanguage. Similar idea for the antipermissive control law leads to a maximal observable sublanguage that contains the supremal normal sublanguage. We present an algorithm for its computation.