Salty-A Domain Specific Language for GR(1) Specifications and Designs

摘要

Designing robot controllers that correctly react to changes in the environment is a time-consuming and error-prone process. An alternative is to use “correct-by-construction” synthesis approaches to automatically generate controller designs from high-level specifications. In particular, Generalized Reactivity(l) or GR(1) specifications are well-suited to express specifications for robots that must act in dynamic environments, and approaches to generate controller designs from GR(1) specifications are highly computationally efficient. Toward that end, this paper presents Salty, a domain-specific language for GR(1) specifications. While tools exist to synthesize system designs from GR(1) specifications, Salty makes such specifications easier to write and debug by supporting features such as richer input and output types, user-defined macros, common specification patterns, and specification optimization and sanity checking. Salty interfaces with the separately developed synthesis tool Slugs to produce a system or controller design, and Salty translates this design to a software implementation in a variety of languages. We demonstrate Salty on an application involving coordination of multiple unmanned air vehicles (UAVs) and provide a workflow for connecting synthesized UAV controllers to freely available UAV planning and simulation software suites UxAS and AMASE.