Contracts of Reactivity
?
Tung Phan-Minh
1
and Richard M. Murray
2
1
Department of Mechanical Engineering
tung@caltech.edu
2
Department of Control and Dynamical Systems
California Institute of Technology, Pasadena CA 91125, USA
Abstract.
We present a theory of contracts that is centered around
reacting to failures and explore it from a general assume-guarantee per-
spective 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.
Keywords:
Design by contracts
·
Modeling uncertainties
·
Formal spec-
ifications
·
Reactive synthesis.
1 Introduction
Automating correctness and improving productivity motivate the development
of formal contracts in the compositional design of large and complex engineer-
ing systems (e.g., [20]). Abstractly speaking, a contract [5] is a su