Compositional Synthesis via a Convex Parameterization of Assume-Guarantee Contracts

Abstract

We develop an assume-guarantee framework for control of large scale linear (time-varying) systems from finite-time reach and avoid or infinite-time invariance specifications. The contracts describe the admissible set of states and controls for individual subsystems. A set of contracts compose correctly if mutual assumptions and guarantees match in a way that we formalize. We propose a rich parameterization of contracts such that the set of parameters that compose correctly is convex. Moreover, we design a potential function of parameters that describes the distance of contracts from a correct composition. Thus, the verification and synthesis for the aggregate system are broken to solving small convex programs for individual subsystems, where correctness is ultimately achieved in a compositional way. Illustrative examples demonstrate the scalability of our method.

References in corpus (1)

• Lectures on 0/1-polytopes

Cited by in corpus (7)

• Categorical Semantics of Cyber-Physical Systems Theory
• Compositional Abstraction-based Synthesis for Interconnected Systems: An Approximate Composition Approach
• Handling state space explosion in verification of component-based systems: A review
• Controller Synthesis of Collaborative Signal Temporal Logic Tasks for Multi-Agent Systems via Assume-Guarantee Contracts
• Verifying Contracts for Perturbed Control Systems using Linear Programming
• Verifying Compositional Refinement of Assume/Guarantee Contracts using Linear Programming
• Consensus-Based Set-Theoretic Control in Power Systems