CHASE.AI: Compositional and Hierarchical Verification and Synthesis of Systems Enabled by Artificial Intelligence
Abstract
Research Problem and Objectives. Naval and other cyber-physical systems are increasingly reliant on AI-enabled components for enhanced perception, situational awareness, and adaptiveness to unstructured and uncertain environments. This trend has substantially increased system complexity, and traditional methods for system verification and validation, aiming toprovide strong guarantees of correctness and dependability, have become inadequate. This project aims to develop CHASE.AI, a methodology, supported by tools, for scalable verification and validation of AI-enabled systems by leveraging: (i) compact abstractions of different AI components to efficiently reason about multiple design objectives in complex closed-loop systems;(ii) scalable algorithmic techniques to generate correct implementations of AI-enabled components from high-level specifications; (iii) hierarchical and incremental system verification methods; and (iv) modular monitoring algorithms for runtime design assurance.Technical Approaches. CHASE.AI adopts a modeling approach based on contracts, offering mechanisms for rigorous abstraction, composition, and reuse, which are key to enable scalable verification of complex systems and determine the correctness of designs made of independently developed sub-systems. Based on the calculus of contracts, CHASE.AI will introduce acompositional and hierarchical verification methodology combining data-driven and stochastic abstractions of AI-enabled components, correct-by-construction design of learning-based control policies, and efficient runtime validation techniques. Stochastic abstractions, ranging from kernel machine representations of deep neural network-based components to stochastic temporal logic based formalisms, will allow quantifying and reasoning about the uncertainty associated with AI enabled components and their environments in a tractable way. Rich, temporal logic specification will be used to synthesize provably correct optimal controllers via model-based and model-freelearning-driven algorithms. Synthesized designs will be validated via high-fidelity simulations and scalable monitoring algorithms to detect contract violation and provide design assurance at runtime.Anticipated Outcome of Research. The anticipated outcomes of the proposed research include: (i) new data-driven abstractions of AI-enabled perception and control components; (ii) new compositional stochastic specification formalisms for AI-enabled systems; (iii) learning-based model-based and model-free algorithms for optimal controller synthesis from rich temporal logicspecifications; (iv) a modular verification methodology based on incremental system refinement and scalable computational tools; (v) modular algorithms for design assurance via offline and online monitoring of probabilistic requirements.Impact on DoD Capabilities. The research outcomes can significantly enhance DoD capabilities in the design of autonomous watercraft and ground vehicles for unmanned operation in unstructured and uncertain environments.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Apr 29, 2020
- Source ID
- N000142012258
Entities
People
- Pierluigi Nuzzo
Organizations
- Office of Naval Research
- United States Navy
- University of Southern California