CPS:Small: Syntax-Guided Synthesis for Cyber-Physical Systems

Abstract: Nowadays, anyone can buy and put together sensors, actuators, and computation components, but typically only highly trained engineers are able to compose systems that can autonomously perform complex tasks. This project makes the design of cyber-physical systems (CPS) accessible to anyone by creating computational tools that enable people to choose a set of building blocks and define what a system should do. The tools then automatically create a simple and easy to understand description of how to assemble the components and provide the control needed to accomplish the task. If the task cannot be done with a single system, the tools provide either multiple systems that need to be assembled and/or explanations as to why the task cannot be done, for example due to physical constraints. The project includes designing a competition to accelerate the development of design tools, and mentoring of students from underrepresented groups. Inspired by advances in program synthesis, control synthesis and modular CPS, this project (i) defines formal specifications and synthesis processes for CPS whose task requires motion in the physical environment, and (ii) creates automated design tools that synthesize both the structure and control of the CPS and that guarantee either full or partial task satisfaction. The formalisms and tools are based on the Syntax-Guided Synthesis (SyGuS) paradigm where the design space is reduced by considering additional structure and leverages computational methods from satisfiability-modulo-theories (SMT) solvers to program synthesis tools, inverse kinematics solvers, motion planners and design optimization. The tools are evaluated on two physical and two simulated platforms.