Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software
摘要
Verification of robotic systems that use neural networks is a challenge. In this paper, we present a formal technique supported by tools to model and verify control software involving neural networks. Our technique enables reasoning about the reactive, communication-based, properties of a system through a process-algebraic lens. We support our framework with a link to state-of-the-art ANN verification tools, using them to prove contextual properties of a neural network. Our approach is flexible, platform-independent, and focuses on the logic of neural network models, instead of on a training method or specific use case.