Send email Copy Email Address

BOCoSy: Small but Powerful Symbolic Output-Feedback Control


We present BOCoSy, a tool for bounded symbolic output-feedback controller synthesis. BOCoSy synthesizes symbolic output-feedback controllers which interact with a given plant via a pre-defined finite symbolic interface. BOCoSy solves this problem by a new lazy abstraction-refinement technique which starts with a very coarse abstraction of the external trace semantics of the given plant and iteratively removes non-admissible behavior from this abstract model until a controller is found. BOCoSy steers the search for controllers towards small and concise state space representations by utilizing ideas from bounded synthesis. As a result, BOCoSy returns small and explainable controllers that are still powerful enough to solve the given synthesis problem. We show that BOCoSy is able to synthesize small, human readable symbolic controllers quickly on a set of benchmarks.

Conference / Medium

25th ACM International Conference on Hybrid Systems: Computation and Control

Date published


Date last modified

2022-05-06 08:48:33