Contracts of Reactivity

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.