A Caltech Library Service

Contracts of Reactivity

Phan-Minh, Tung and Murray, Richard M. (2019) Contracts of Reactivity. . (Unpublished)

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


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 compliant with a contract metatheory introduced by Benveniste et al. We also show how to obtain an automated procedure for synthesizing reactive assume-guarantee contracts and implementations that capture ideas like 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.

Item Type:Report or Paper (Discussion Paper)
Related URLs:
URLURL TypeDescription
Murray, Richard M.0000-0002-5785-7481
Additional Information:Submitted, Int'l. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS) 2019. Supported by DENSO International America, Inc., the Jack Kent Cooke Foundation, and the NSF VeHICaL project.
Group:Center for Autonomous Systems and Technologies (CAST)
Funding AgencyGrant Number
DENSO International America, Inc.UNSPECIFIED
Jack Kent Cooke FoundationUNSPECIFIED
Subject Keywords:Design by contracts; Modeling uncertainties; Formal specifications; Reactive synthesis
Record Number:CaltechAUTHORS:20191029-132616005
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:99542
Deposited By: Tony Diaz
Deposited On:29 Oct 2019 20:37
Last Modified:29 Oct 2019 20:37

Repository Staff Only: item control page