Assume Guarantee Contracts

Modern cyber–physical systems, such as autonomous multi-agent teams, networked infrastructures, and hybrid dynamical systems are increasingly large, interconnected, and heterogeneous. Ensuring correct and safe behavior in such systems is challenging because global verification and centralized controller synthesis often scale poorly with dimension, communication constraints, and subsystem coupling. Our work leverages assume–guarantee contracts as a principled framework to decompose complex control and verification tasks into manageable components.

Contracts turn system-level requirements into structured assumptions and guarantees that each subsystem must satisfy, enabling compositional reasoning, modular controller synthesis, and scalable safety verification across mixed continuous–time, discrete–time, and hybrid models.

The goal is to build transparent, scalable, and verifiable control architectures in which each subsystem interacts through clearly specified contracts. This allows complex systems to coordinate, collaborate, and satisfy rich specifications, such as temporal logic tasks, without requiring monolithic design or global knowledge of all dynamics.

• Compositional Verification with Contract Semantics

We develop weak and strong semantics for assume–guarantee contracts that determine how local properties compose into global guarantees. These semantics are valid for continuous-time, discrete-time, and hybrid systems and allow scalable controller synthesis and formal verification through subsystem-level reasoning.

• Contract-Based Controller Synthesis under Temporal Logic Tasks

We design assume-guarantee frameworks for cooperative signal temporal logic specifications, enabling distributed agents to coordinate under shared assumptions and local guarantees.

• A. Saoud, A. Girard and L. Fribourg, “Assume-guarantee Contracts for Continuous-time Systems,” Automatica, vol. 66, no. 134, p. 109910, 2021.

• 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.

• S. Liu, A. Saoud and D. V. Dimarogonas, “Controller Synthesis of Collaborative Signal Temporal Logic Tasks for Multi-Agent Systems via Assume–Guarantee Contracts,” IEEE Transactions on Automatic Control, 2025.

• S.B. Alaoui, A. Saoud, “Contract-Based Design for Hybrid Dynamical Systems and Invariance Properties,” IFAC Analysis and Design of Hybrid Systems (IFAC ADHS), IFAC-PapersOnLine. 2024 Jan 1, vol. 58 no. 11, pp. 189-94. 

• N. Monir, Y. Ait Si, R. Das, P. Jagtap, A. Saoud and S. Soudjani, “Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach,” IEEE Conference on Decision and Control (CDC), 2025.

• 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).