@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{kim-hscc17,
 author    = {Eric S. Kim and Murat Arcak and
               Sanjit A. Seshia},
 title     = {A Small Gain Theorem for Parametric Assume-Guarantee Contracts}
 booktitle = {Proceedings of the 10th International Conference on Hybrid Systems: Computation and Control (HSCC)},
 month = "April",
 year = {2017},
 pages     = {207--216},
 abstract = {The problem of verifying properties of large, networked cyber-physical 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. Although both techniques have been used for control synthesis and verification, to our knowledge there does not exist a formal investigation connecting these two methodologies.
We introduce the notion of a parametric assume-guarantee contract, which lets a system's guarantee depend on the behavior of its environment, and show how a finite gain property can be encoded in this form. A small-gain theorem is then provided 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.},
}