Contracts of Reactivity

From Murray Wiki
Revision as of 02:03, 5 September 2021 by Murray (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search
Title Contracts of Reactivity
Authors Tung Phan-Minh and Richard M. Murray
Source Submitted, Int'l Conf on Formal Modeling and Analysis of Timed Systems (FORMATS) 2019
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 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.
Type Conference paper
URL s.pdf
Tag pm19-formats
ID 2019g
Flags NCS