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 new approach to design verified compositions of NeuralNetwork (NN) controllers for autonomous systems with tasks captured by LinearTemporal Logic (LTL) formulas. Particularly, the LTL formula requires thesystem to reach and avoid certain regions in a temporal/logical order. Weassume that the system is equipped with a finite set of trained NN controllers.Each controller has been trained so that it can drive the system towards aspecific region of interest while avoiding others. Our goal is to check ifthere exists a temporal composition of the trained NN controllers - and if so,to compute it - that will yield composite system behaviors that satisfy auser-specified LTL task for any initial system state belonging to a given set.To address this problem, we propose a new approach that relies on a novelintegration of automata theory and recently proposed reachability analysistools for NN-controlled systems. We note that the proposed method can beapplied to other controllers, not necessarily modeled by NNs, by appropriateselection of the reachability analysis tool. We focus on NN controllers due totheir lack of robustness. The proposed method is demonstrated on navigationtasks for aerial vehicles.

Verified Compositions of Neural Network Controllers for Temporal Logic Control Objectives