Controller synthesis for cyber-physical systems (CPS) is a very active research area that studies the interaction between physical processes and control software in a rigorous manner. Different approaches have been proposed in the decade by combining tools from control theory and formal methods. Formal methods were originally developed in the computer science community, where models of software programs and digital circuits are generally simple (discrete-state transition systems), while the considered specifications are rather complex and often described as temporal logic formulas. On the other hand, models of systems in control theory are generally complex and given as differential or difference equations with continuous state variables, while the considered specifications are simpler and correspond to stability, reference tracking, invariance..The standard paradigm to connect the two areas is to ”abstract” a continuous-state dynamical model into a discrete-state transition model by partitioning the state space into discrete states and determining which discrete transitions are possible under each control action, followed by an appropriate synthesis technique in the discrete domain.
Symbolic approaches are considered today as a powerful tool to the control of CPS, they present several advantages with respect to the classical control theoretic approaches, including:
Dealing with nonlinear systems subject to constraints;
Complex logic specifications: such as safety, reachability, motion planning with obstacle avoidance or more complex objectives such as those expressed in linear temporal logic (LTL), and which are very representative for modern CPS such as robots or autonomous vehicles. Consider for example an autonomous aerial vehicle that must take photos of areas A and B infinitely often, always avoid obstacles C and D, and return to the charging point P when the battery level goes low, which is a difficult task to deal with using classical control theory tools.
Considering the interaction between control software with physical processes: the symbolic model and the control software inside the digital computation platform are described in a unified framework (for example as a transition system). This allows to take into account the constraints on the cyber part during the controller synthesis;
The approach is automatic and formal: controller synthesis is done in an automatic way, without relying on heuristic techniques (such as PID or MPC controllers for example which needs tuning and testing). Moreover, the guarantees are formal, in the sense that the closed-cloop CPS achieves the given specification.
Focus Areas
Construction of efficient and parsimonious symbolic abstractions
We develop scalable symbolic abstraction-based control methods for different classes of systems. Our work reduces the complexity of symbolic models through multirate and event-based sampling, providing approximately bisimilar abstractions with dramatically fewer transitions. We also design lazy and priority-based safety controllers that exploit system structure, such as incremental stability and monotonicity, to achieve efficient synthesis for large-scale systems.
Compositional abstraction-based controller synthesis
We design compositional control methods using assume–guarantee contracts and symbolic abstractions to enforce safety and temporal-logic specifications in interconnected and multi-agent systems. By exploiting local information and structured communication, we achieve scalable, correct-by-design controllers for complex networked systems.
Related Publications
A. Saoud and A. Girard, “Optimal Multirate Sampling in Symbolic Models for Incrementally Stable Switched Systems ,” Automatica, vol. 98, pp. 58–65, 2018.
K. Hashimoto, A. Saoud, M. Kishida, T. Ushio and D. V. Dimarogonas, “A Symbolic Approach to the Self-Triggered Design for Networked Control Systems,” IEEE Control Systems Letters (L-CSS), vol. 3, no. 4, pp. 1050–1055, 2019.
A. Saoud, A. Girard and L. Fribourg, “Contract-based Design of Symbolic Controllers for Safety in Distributed Multiperiodic Sampled-Data Systems,” IEEE Transactions on Automatic Control, vol. 66, no. 3, pp. 1055–1070, 2020.
A. Saoud, P. Jagtap, M. Zamani and A. Girard, “Compositional Abstraction-based Synthesis for Interconnected Systems: An Approximate Composition Approach,” IEEE Transactions on Control of Network Systems, vol. 8, no. 2, pp. 702–712, 2021.
S. W. Smith, A. Saoud and M. Arcak, “Monotonicity-Based Symbolic Control for Safety in Driving Scenarios ,” IEEE Control Systems Letters (L-CSS), vol. 6, no. 3, pp. 830–835, 2022.
E. Ivanova, A. Saoud and A. Girard, “Lazy Controller Synthesis for Monotone Transition Systems and Directed Safety Specifications,” Automatica, vol. 135, p. 109993, 2022.
Y. Ait si, A. Girard and A. Saoud, “Symbolic control: Unveiling free robustness margins,” European Journal of Control, 2025.
Z. Kader, A. Girard and A. Saoud, “Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling,” IFAC Analysis and Design of Hybrid Systems (IFAC ADHS), IFAC-PapersOnLine, vol. 51, no. 16, pp.253-258, 2018.
Z. Kader, A. Saoud and A. Girard, “Safety Controller Design for Incrementally Stable Switched Systems Using Event-based Symbolic Models,” European Control Conference (ECC), 2019 (pp. 1269-1274).
D. Zonetti, A. Saoud, A. Girard and L. Fribourg, “A Symbolic Approach to Voltage Stability and Power Sharing in Time-varying DC Microgrids,” European control conference (ECC), 2019, (pp. 903-909).
S.B. Alaoui, A. Saoud, P. Jagtap, and A. Swikir, “Symbolic Models for Interconnected Impulsive Systems,” IEEE Conference on Decision and Control (CDC), 2023, (pp. 5900-5905).