Deadlock-free output feedback controller design based on approximately abstracted observers

In this paper, we design a deadlock-free symbolic output feedback controller. A physical plant is modeled by an infinite transition system, whose verification and synthesis problems are generally undecidable in finite time steps. Then, we consider an abstracted model of the physical plant. Assume that a controller for the abstracted plant model is given if the state of the physical plant is fully measured. For the application to the case of partial observation, we design an observer induced by the abstracted plant model and obtain an output feedback controller. The proposed observer computes sets of candidates of the current state with injected inputs and observed outputs. The control input is determined in such a way that every candidate state listed by the observer satisfies the control specification that had been achieved by the controller in the case of full observation, which implies that the proposed approach suppresses the effects of the partial observation. A deadlock-free controller is computed iteratively by eliminating transitions to deadlock states.