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.
Cite
@article{arxiv.2002.06494,
title = {Compositional Synthesis via a Convex Parameterization of Assume-Guarantee Contracts},
author = {Kasra Ghasemi and Sadra Sadraddini and Calin Belta},
journal= {arXiv preprint arXiv:2002.06494},
year = {2020}
}