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

Several methods have been proposed recently to learn neural network (NN)controllers for autonomous agents, with unknown and stochastic dynamics, taskedwith complex missions captured by Linear Temporal Logic (LTL). Due to thesample-inefficiency of the majority of these works, compositional learningmethods have been proposed decomposing the LTL specification into smallersub-tasks. Then, separate controllers are learned and composed to satisfy theoriginal task. A key challenge within these approaches is that they often lacksafety guarantees or the provided guarantees are impractical. This paper aimsto address this challenge. Particularly, we consider autonomous systems withunknown and stochastic dynamics and LTL-encoded tasks. We assume that thesystem is equipped with a finite set of base skills modeled by trained NNfeedback controllers. Our goal is to check if there exists a temporalcomposition of the trained NN controllers - and if so, to compute it - thatwill yield a composite system behavior that satisfies the assigned LTL taskwith probability one. We propose a new approach that relies on a novelintegration of automata theory and data-driven reachability analysis tools forNN-controlled stochastic systems. The resulting neuro-symbolic controllerallows the agent to generate safe behaviors for unseen complex temporal logictasks in a zero-shot fashion by leveraging its base skills. We show correctnessof the proposed method and we provide conditions under which it is complete. Tothe best of our knowledge, this is the first work that designs verifiedtemporal compositions of NN controllers for unknown and stochastic systems.Finally, we provide extensive numerical simulations and hardware experiments onrobot navigation tasks to demonstrate the proposed method.

Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks