CSR-EHCS(EHS), SM: A formal approach to control of hybrid systems with applications to mobile robotics

Trustees Of Boston University, Boston

Investigators

Abstract

In formal verification, finite models of computer programs or digital circuits are checked against temporal logic properties such as safety (something bad never happens) and liveness (something good eventually happens). While formal verification received a lot of attention, the dual problem of formal synthesis, where the focus is to construct a provably correct system (e.g., safe by design) is still in its infancy. In addition, most systems, such as models of unmanned vehicles, are hybrid, combining continuous models of vehicle dynamics with finite state automata that model embedded controllers and communication protocols. This project develops theoretical frameworks and computational tools for synthesis of provably-correct control and communication strategies for hybrid systems and distributed hybrid systems from specifications given in rich, human-like language. Central to the approach in this project is the notion of abstraction, which is used to construct finite descriptions of control systems. Such abstractions allow for the use of (adapted) temporal logics as specification languages, tools from formal verification and temporal logic games for analysis and control, and techniques inspired from synchronization in concurrency theory for synthesis of communication strategies. The computational tools developed in this project are implemented as user-friendly software packages and tested in a miniature mobile robotics experimental platform. This research is closely integrated with a comprehensive educational and outreach plan, which includes undergraduate and graduate classes, involvement of undergraduate and high school students in research, and the participation of the PI as a judge and organizer in high school robotics competitions.