SE PhD Prospectus Defense of Kasra Ghasemi

TITLE: Compositional Verification and Synthesis for Linear Systems via Convex Optimization of Assume-Guarantee Contract

ABSTRACT: We take a divide and conquer approach to design controllers for the problem of finite-time reach and avoid or infinite-time invariance of the large-scale linear systems with polyhedral constraints on states, controls, and disturbances. Each subsystem can design and implement its robust decentralized controller locally subject to its own constraints and contracts. The system is broken into small subsystems with coupled dynamics where couplings are treated as additional disturbances and assume-guarantee contracts are used to characterize these new disturbance sets.

The contracts describe the admissible set of states and controls for individual subsystems which are the compositions of the disturbance sets in the described decoupling method. 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.

Our main contribution is a method to derive the contracts via a novel parameterization and a corresponding potential function that characterize the distance to the correct composition of controllers and contracts. We show that the potential function becomes a convex function of the contract parameters. Thus, the subsystems negotiate the contracts with the gradient information from the dual of their local synthesis optimization problems in a distributed way, facilitating compositional control synthesis that scales to large systems. In other words, the verification and synthesis for the large-scale system are broken to solving small convex programs for individual subsystems, where correctness is ultimately achieved in a compositional way.

We present numerical examples, including a scalability study on tens of thousands of dimensions and a case study on applying our method to distributed Model Predictive Control (MPC) for power systems.

COMMITTEE: Advisor/Chair Calin Belta, SE, ME; Yannis Paschalidis, SE, ECE, BME; Wenchao Li, SE, ECE; Roberto Tron, SE, ME