Formal Specifications of Autonomous Systems

A specification for a system describes its admissible behaviors and formalizes its properties. Many existing design and verification efforts, particularly those based on formal methods, assume the availability of such specifications. However, this assumption has been proved to be a major problem of its own, as witnessed in many CPS applications that integrate autonomy. The lack of precise specifications is a significant impediment towards formal methods realizing their full potential in this domain.

The goal of this project is to provide theory, methods, and tools to derive, analyze, and refine specifications for systems subject to regulatory requirements. Our approach integrates formal methods, learning-based approaches, and game-theoretic frameworks, and utilize complementary sources of information, namely the textual information from the regulatory requirements and the demonstrations, taking into account their imperfection such as ambiguity, incompleteness, labeling errors, and uncertainties.