Verifying specifications for large-scale modern engineering systems can be a time-consuming task, as most formal verification methods are limited to systems of modest size. Recently, contract-based design and verification has been proposed as a modul
ar framework for specifications, and linear-programming-based techniques have been presented for verifying that a given system satisfies a given contract. In this paper, we extend this assume/guarantee framework by presenting necessary and sufficient conditions for a collection of contracts on individual components to refine a contract on the composed system. These conditions can be verified by solving linear programs, whose number grows linearly with the number of specifications defined by the contracts. We exemplify the tools developed using a case study considering safety in a car-following scenario, where noise and time-varying delay are considered.
This paper studies model order reduction of multi-agent systems consisting of identical linear passive subsystems, where the interconnection topology is characterized by an undirected weighted graph. Balanced truncation based on a pair of specificall
y selected generalized Gramians is implemented on the asymptotically stable part of the full-order network model, which leads to a reduced-order system preserving the passivity of each subsystem. Moreover, it is proven that there exists a coordinate transformation to convert the resulting reduced-order model to a state-space model of Laplacian dynamics. Thus, the proposed method simultaneously reduces the complexity of the network structure and individual agent dynamics, and it preserves the passivity of the subsystems and the synchronization of the network. Moreover, it allows for the a priori computation of a bound on the approximation error. Finally, the feasibility of the method is demonstrated by an example.
