Formal Verification of Robustness and Resilience in Learning-Enabled State Estimation Systems

This paper presents a formal verification approach to assess the robustness and resilience of learning-enabled state estimation systems, which integrate neural networks and Bayes filters. It formalizes the concepts of robustness and resilience, reduces the learning-enabled systems to a novel class of labeled transition systems, and develops automated verification algorithms to check the satisfiability of these properties.