Correct-by-design output feedback of LTI systems

Current state-of-the-art correct-by-design controllers are designed for full-state measurable systems. This work extends the applicability of correct-by-design controllers to partially observable linear, time-invariant (LTI) models. Towards the certification of the synthesised controllers, approximate simulation relations are leveraged to attain a quantification for the accuracy of introduced approximations. Additionally, the robustness of the approach allows the extension to models with the presence of probabilistic disturbances on state transitions and on output measurements. In a case study from smart buildings we evaluate the new output-based correct-by-design controller on a physical system with limited sensor information.