A small gain theorem for parametric assume-guarantee contracts

Abstract

The problem of verifying properties of large, networked cyberphysical systems (CPS) is beyond the reach of most computational tools today. Two common "divide-and-conquer" techniques for CPS verification are assume-guarantee contracts from the formal methods literature and input-output properties from the control theory literature. Combining these two approaches, we first introduce the notion of a parametric assume-guarantee contract, which lets one reason about system behavior abstractly in a parameter domain. We next show how a finite gain property can be encoded in this form and provide a generalized small-gain theorem for parametric assume-guarantee contracts. This theorem recovers the classical small gain theorem as a special case and its derivation highlights the connection between assume-guarantee reasoning and small-gain results. This new small-gain theorem applies to behaviors beyond bounded deviation from a nominal point to include a fragment of linear temporal logic with parametrized predicates that can encode safety, recurrence, and liveness properties. Our results are validated with an example which certifies that the interconnection of two freeway segments experiences intermittent congestion.