Model-based Controller Synthesis
Nowadays, there are increasing demands for designing correct-by-construction controllers in many safety-critical real-life applications such as autonomous vehicles, power grids, etc. As a result, formal synthesis of controllers for these systems has gained significant attention in the past decades, particularly for enforcing complex logical properties, such as those expressed as linear temporal logic (LTL) formulae.
In general, formal synthesis of such controllers can be achieved by leveraging abstraction-based and abstraction-free approaches. In the former cases, finite abstractions with discrete state and input sets are constructed by discretizing the original continuous state and input sets. Then, one can synthesize controllers for the finite abstractions, leveraging those results for reactive synthesis, and refine the discrete controllers back to the original systems. As for abstraction-free methods, building finite abstractions is not required. Instead, one synthesizes controllers by employing appropriate set iterative schemes, reachability analysis, or control barrier functions.
Highlights of the results:
We proposed an abstraction-based approach for synthesizing controllers for discrete-time non-cooperative nonlinear stochastic games against complex logical properties expressed by deterministic finite automata (DFA). Formal probabilistic guarantees for satisfying the desired properties are provided by leveraging the similarity between the original systems and their finite abstractions.
We proposed an abstraction-free, set-based approach for synthesizing controllers for uncertain linear systems against \(\omega\)-regular properties.
Related papers
B. Zhong, M. Zamani, and M. Caccamo, Formal synthesis of controllers for uncertain linear systems against omega-regular properties: A set-based approach, In: IEEE Transactions on Automatic Control, Vol. 69, No. 1, 214-229, 2024. (Preprint)
B. Zhong, A. Lavaei, M. Zamani, and M. Caccamo, Automata-based controller synthesis for stochastic systems: A game framework via approximate probabilistic relations, In: Automatica, 147C, 2023. (Preprint) (Editors’ Choice paper for January 2023)
B. Zhong, M. Zamani, and M. Caccamo, A set-based approach for synthesizing controllers enforcing omega-regular properties over uncertain linear control systems, In: Proceedings of American Control Conference (ACC), pp. 1575 - 1581, 2022.
B. Zhong, A. Lavaei, M. Zamani, and M. Caccamo, Poster abstract: Controller Synthesis for Nonlinear Stochastic Games via Approximate Probabilistic Relations, In: Proceedings of 25th ACM International Conference on Hybrid Systems: Computation and Control, 2022