Back-propagation through signal temporal logic specifications: infusing logical structure into gradient-based methods

DOI10.1007/978-3-030-66723-8_26MaRDI QIDQ3381991zbMATH OpenOpenAlexFDO

Authors

Publication date 20 September 2021

Published in Algorithmic Foundations of Robotics XIV (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2008.00097

zbMATH Keywords

back-propagationcomputation graphlogical structurerobustnesssignal temporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence for robotics (68T40)

Abstract: This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STLCG provides a platform which enables the incorporation of logical specifications into robotics problems that benefit from gradient-based solutions. Specifically, STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems. The quantitative semantics of STL provide a robustness metric, i.e., how much a signal satisfies or violates an STL specification. In this work, we devise a systematic methodology for translating STL robustness formulas into computation graphs. With this representation, and by leveraging off-the-shelf automatic differentiation tools, we are able to efficiently backpropagate through STL robustness formulas and hence enable a natural and easy-to-use integration of STL specifications with many gradient-based approaches used in robotics. Through a number of examples stemming from various robotics applications, we demonstrate that STLCG is versatile, computationally efficient, and capable of incorporating human-domain knowledge into the problem formulation.

Recommendations

• Robust control for signal temporal logic specifications using discrete average space robustness
• Temporal logic guided safe model-based reinforcement learning: a hybrid systems approach
• TeLEx: learning signal temporal logic from positive examples using tightness metric
• Reactive synthesis from signal temporal logic specifications
• Temporal logic model predictive control

Cites work

• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Logical clustering and learning for time-series data

Cited in

(2)

• Survey on mining signal temporal logic specifications
• Poster Abstract: Safety Guaranteed Preference Learning Approach for Autonomous Vehicles

Describes a project that uses

Uses Software

• PyTorch

This page was built for publication: Back-propagation through signal temporal logic specifications: infusing logical structure into gradient-based methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3381991)