Published June 29, 2021
| Submitted
Book Section - Chapter
Open
Contracts of Reactivity
- Creators
- Phan-Minh, Tung
-
Murray, Richard M.
Chicago
Abstract
We present a theory of contracts that is centered around reacting to failures and explore it from a general assume-guarantee perspective as well as from a concrete context of automated synthesis from linear temporal logic (LTL) specifications, all of which are compatible with a contract metatheory introduced by Benveniste et al. We also provide an automated procedure for synthesizing reactive assume-guarantee contracts and implementations that capture ideas such as optimality and robustness based on assume-guarantee lattices computed from antitone Galois connection fixpoints. Lastly, we provide an example of a reactive GR(1) contract and a simulation of its implementation.
Additional Information
© 2021 EUCA. Supported by DENSO International America, Inc., the Jack Kent Cooke Foundation, and the NSF VeHICaL project (NSF grant #1545126). The authors would like to thank the anonymous reviewers and Íñigo Íncer Romeo for their helpful comments and suggestions.Attached Files
Submitted - pm19-formats_s.pdf
Files
pm19-formats_s.pdf
Files
(3.2 MB)
Name | Size | Download all |
---|---|---|
md5:f0b6402335d06841b97e5b20351c5273
|
3.2 MB | Preview Download |
Additional details
- Eprint ID
- 99542
- Resolver ID
- CaltechAUTHORS:20191029-132616005
- DENSO International America, Inc.
- Jack Kent Cooke Foundation
- NSF
- CNS-1545126
- Created
-
2019-10-29Created from EPrint's datestamp field
- Updated
-
2022-04-11Created from EPrint's last_modified field
- Caltech groups
- Center for Autonomous Systems and Technologies (CAST), Division of Biology and Biological Engineering