Formal Synthesis of Controllers for Uncertain Linear Systems against $\omega$-Regular Properties: A Set-based Approach

TL;DR

This paper introduces a set-based method for synthesizing controllers that enforce $$-regular properties on uncertain linear systems using hybrid controlled invariant sets and product automata, with proven termination and case studies.

Contribution

It presents a novel set-based approach for controller synthesis for linear systems with disturbances against $$-regular properties, including new iterative schemes for finite computation.

Findings

Effective controller synthesis demonstrated on case studies.

Finite termination of HCI set computation achieved.

Set-based approach handles bounded disturbances in linear systems.

Abstract

In this paper, 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 compute the maximal HCI set over the state set of the product system by leveraging a set-based approach. To ensure termination of the computation of the HCI sets within a finite number of iterations, we also propose two iterative schemes to compute approximations of the maximal HCI set. Finally, we show the effectiveness of our results via two case studies.