Formal Composition of Robotic Systems as Contract Programs

Abstract

Robotic systems are often composed of modular algorithms that each perform a specific function within a larger architecture, ranging from state estimation and task planning to trajectory optimization and object recognition. Existing work for specifying these systems as a formal composition of contract algorithms has limited expressiveness compared to the variety of sophisticated architectures that are commonly used in practice. Therefore, in this paper, we (1) propose a novel metareasoning framework for formally composing robotic systems as a contract program with programming constructs for functional, conditional, and looping semantics and (2) introduce a recursive hill climbing algorithm that finds a locally optimal time allocation of a contract program. In our experiments, we demonstrate that our approach outperforms baseline techniques in a simulated pick-and-place robot domain.