Hy-CIRCA: Autonomous Synthesis and Verification of Hybrid Cyber-Physical System Controllers

ABSTRACT: To unlock the power of cooperating teams of autonomous cyber-physical systems (CPSs), humans must be able to effectively, reliably, and safely task them using high-level goals. SIFTs Playbook interface approach provides goal-based tasking for multi-agent autonomous missions. SIFTs Cooperative Intelligent Real-time Control Architecture (CIRCA) automatically synthesizes and verifies real-time, closed loop discrete controllers for multiagent autonomous missions. To fully realize the potential that CIRCA and Playbook offer, we must extend CIRCAs coverage from timed discrete systems to CPSs with complex, nonlinear dynamics. CMUs dReal system uses delta-complete approximate reasoning methods to efficiently verify hybrid system models including nonlinear constraints, ordinary differential equations, and discrete dynamics. SIFT will team with Prof. Ed Clarkes research group at CMU to build Hy-CIRCA, a system that will automatically transform mission specifications into verified closed-loop hybrid controllers. BENEFIT: Hy-CIRCAs ability to synthesize formally-guaranteed CPS controllers will be broadly useful in both military and commercial applications, including teams of fully autonomous vehicles, factory and warehouse automation, etc. By allowing humans to express high-level goals that are then reliably transformed into verified controllers, Hy-CIRCA will support deployment of autonomous systems for applications that require high-reliability operations in hazardous or adversarial environments. Building, certifying, and deploying such autonomous systems will be made faster, less costly, and less error-prone using the Hy-CIRCA technology.