English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper presents a formal verification guided approach for a principleddesign and implementation of robust and resilient learning-enabled systems. Wefocus on learning-enabled state estimation systems (LE-SESs), which have beenwidely used in robotics applications to determine the current state (e.g.,location, speed, direction, etc.) of a complex system. The LE-SESs arenetworked systems composed of a set of connected components including Bayesfilters for localisation, and neural networks for processing sensory input. Westudy LE-SESs from the perspective of formal verification, which determines thesatisfiability of a system model against the specified properties. OverLE-SESs, we investigate two key properties - robustness and resilience - andprovide their formal definitions. To enable formal verification, we reduce theLE-SESs to a novel class of labelled transition systems, named {PO}2-LTS in thepaper, and formally express the properties as constrained optimisationobjectives. We prove that the robustness verification is NP-complete. Based on{PO}2-LTS and the optimisation objectives, practical verification algorithmsare developed to check the satisfiability of the properties on the LE-SESs. Asa major case study, we interrogate a real-world dynamic tracking system whichuses a single Kalman Filter (KF) - a special case of Bayes filter - to localiseand track a ground vehicle. Its perception system, based on convolutionalneural networks, processes a high-resolution Wide Area Motion Imagery (WAMI)data stream. Experimental results show that our algorithms can not only verifythe properties of the WAMI tracking system but also provide representativeexamples, the latter of which inspired us to take an enhanced LE-SESs designwhere runtime monitors or joint-KFs are required. Experimental results confirmthe improvement of the robustness of the enhanced design.

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