Formal Synthesis of Controllers for Uncertain Linear Systems Against ω-Regular Properties: A Set-Based Approach

In this article, we present how to synthesize controllers to enforce $\omega$-regular properties over linear control systems affected by bounded disturbances. In particular, these controllers are synthesized based on so-called hybrid controlled invariant (HCI) sets. To compute these sets, we first construct a product system between the linear control system and the deterministic Streett automata (DSA) modeling the desired property. Then, we propose a set-based approach, which exploits a new iterative scheme over hybrid state sets of the product system, to compute the maximal HCI set. To ensure the termination of the iterative scheme within a finite number of steps, we propose two alternative approaches to compute approximations of the maximal HCI set. Moreover, we show the relations between the (worst-case) complexities of the proposed iterative schemes over hybrid sets and the structure of the DSA modeling $\omega$-regular properties. Finally, we demonstrate the effectiveness of our results via two case studies.