Difference between revisions of "Contracts of Reactivity"
From Murray Wiki
Jump to navigationJump to search
(Created page with "{{Paper |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) 2...") |
|||
| Line 9: | Line 9: | ||
|Tag=pm19-formats | |Tag=pm19-formats | ||
|Funding=DENSO CPM, NSF VeHICaL | |Funding=DENSO CPM, NSF VeHICaL | ||
|Flags=NCS | |||
}} | }} | ||
Latest revision as of 02:03, 5 September 2021
| 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 | http://www.cds.caltech.edu/~murray/preprints/pm19-formats s.pdf |
| DOI | |
| Tag | pm19-formats |
| ID | 2019g |
| Funding | DENSO CPM, NSF VeHICaL |
| Flags | NCS |
