Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published June 29, 2021 | Submitted
Book Section - Chapter Open

Contracts of Reactivity

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

Created:
August 22, 2023
Modified:
December 22, 2023