Cyber-Physical Systems (CPSs) with learning components are increasingly being deployed in safety-critical applications. However formal verification methodologies only offer limited support for the safety analysis of such systems. The project aims to fill this gap by developing new algorithms and software toolkits for the verification of learning-enabled CPSs (LE-CPSs).
To enable the development of verification methods, the project aims at defining semantic models and formal specification languages for LE-CPSs. Our efforts are focussed on two main objectives:
Our group contributed several techniques to verify neural networks via, e.g., Mixed-integer Linear Programming or Symbolic Interval Propagation. Our approaches present state-of-the-art solutions for the verification of both feed-forward and recurrent neural networks.
We extended the techniques above to account for LE-CPSs operating in an environment. The resulting models are amenable to formal verification and we proposed several techniques to verify them against specifications expressed in rich logics such as LTL, CTL or ATL.
More details on our current research can be found in the Software and Publications sections below.
The following tools have been developed within the project:
P. Henriksen, A. Lomuscio.
Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search.
Proceedings of the 24th European Conference on Artificial Intelligence (ECAI20). Santiago de Compostela, Spain. To Appear.
M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
Formal Verification of Neural Agents in Non-Deterministic Environments.
Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.
E. Botoeva, P. Kouvaros, J. Kronqvist, A. Lomuscio, R. Misener.
Efficient Verification of Neural Networks via Dependency Analysis.
Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). New York City, New York. AAAI Press. To Appear.
M. Akintunde, A. Kevorchian, A. Lomuscio, E. Pirovano
Verification of RNN-Based Neural Agent-Environment Systems
Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019). Honolulu, Hawaii. AAAI Press.
M. Akintunde, A. Lomuscio, L. Maganti, E. Pirovano
Reachability Analysis for Neural Agent-Environment Systems
Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR18). Tempe, Arizona. AAAI Press.
This research is funded by DARPA under the Assured Autonomy program.