STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification

• URL: http://arxiv.org/abs/2501.04194v1
• Date: Wed, 08 Jan 2025 00:06:43 GMT
• Title: STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification
• Authors: Parv Kapoor, Kazuki Mizuta, Eunsuk Kang, Karen Leung,
• Abstract summary: We present STLCG++, a masking-based approach that parallelizes STL computation across timesteps. We also introduce a smoothing technique for different temporal boundsiability through time interval bounds. We demonstrate STLCG++'s benefits through three robotics use cases and provide open-source Python libraries in JAX and PyTorch.
• Score: 8.017203108408975
• License:
• Abstract: Signal Temporal Logic (STL) offers a concise yet expressive framework for specifying and reasoning about spatio-temporal behaviors of robotic systems. Attractively, STL admits the notion of robustness, the degree to which an input signal satisfies or violates an STL specification, thus providing a nuanced evaluation of system performance. Notably, the differentiability of STL robustness enables direct integration to robotics workflows that rely on gradient-based optimization, such as trajectory optimization and deep learning. However, existing approaches to evaluating and differentiating STL robustness rely on recurrent computations, which become inefficient with longer sequences, limiting their use in time-sensitive applications. In this paper, we present STLCG++, a masking-based approach that parallelizes STL robustness evaluation and backpropagation across timesteps, achieving more than 1000x faster computation time than the recurrent approach. We also introduce a smoothing technique for differentiability through time interval bounds, expanding STL's applicability in gradient-based optimization tasks over spatial and temporal variables. Finally, we demonstrate STLCG++'s benefits through three robotics use cases and provide open-source Python libraries in JAX and PyTorch for seamless integration into modern robotics workflows.

Related papers

• Constrained LTL Specification Learning from Examples [8.544277223210894]
  We propose a new type of learning problem called constrained learning. In addition to positive and negative examples, the user can specify one or more constraints over the properties of the formula. An experimental evaluation demonstrates that ATLAS is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in learning.
  arXiv  Detail & Related papers  (2024-12-03T23:15:27Z)
• Regret-Free Reinforcement Learning for LTL Specifications [6.342676126028222]
  Reinforcement learning is a promising method to learn optimal control policies for systems with unknown dynamics. Current RL-based methods offer only guarantees, which provide no insight into the transient performance during the learning phase. We present the first regret-free online algorithm for learning a controller that addresses the general class of specifications over Markov decision processes.
  arXiv  Detail & Related papers  (2024-11-18T20:01:45Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  Linear temporal logic (LTL) is a powerful language for task specification in reinforcement learning. We show that the synthesized reward signal remains fundamentally sparse, making exploration challenging. We show how better exploration can be achieved by further leveraging the specification and casting its corresponding Limit Deterministic B"uchi Automaton (LDBA) as a Markov reward process.
  arXiv  Detail & Related papers  (2024-08-18T14:25:44Z)
• Sparser is Faster and Less is More: Efficient Sparse Attention for Long-Range Transformers [58.5711048151424]
  We introduce SPARSEK Attention, a novel sparse attention mechanism designed to overcome computational and memory obstacles. Our approach integrates a scoring network and a differentiable top-k mask operator, SPARSEK, to select a constant number of KV pairs for each query. Experimental results reveal that SPARSEK Attention outperforms previous sparse attention methods.
  arXiv  Detail & Related papers  (2024-06-24T15:55:59Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  This paper introduces TLINet, a neural-symbolic framework for learning STL formulas. In contrast to existing approaches, we introduce approximation methods for max operator designed specifically for temporal logic-based gradient techniques. Our framework not only learns the structure but also the parameters of STL formulas, allowing flexible combinations of operators and various logical structures.
  arXiv  Detail & Related papers  (2024-05-03T16:38:14Z)
• Fast, Scalable, Warm-Start Semidefinite Programming with Spectral Bundling and Sketching [53.91395791840179]
  We present Unified Spectral Bundling with Sketching (USBS), a provably correct, fast and scalable algorithm for solving massive SDPs. USBS provides a 500x speed-up over the state-of-the-art scalable SDP solver on an instance with over 2 billion decision variables.
  arXiv  Detail & Related papers  (2023-12-19T02:27:22Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• Semi-supervised Learning of Partial Differential Operators and Dynamical Flows [68.77595310155365]
  We present a novel method that combines a hyper-network solver with a Fourier Neural Operator architecture. We test our method on various time evolution PDEs, including nonlinear fluid flows in one, two, and three spatial dimensions. The results show that the new method improves the learning accuracy at the time point of supervision point, and is able to interpolate and the solutions to any intermediate time.
  arXiv  Detail & Related papers  (2022-07-28T19:59:14Z)
• Fast Distributionally Robust Learning with Variance Reduced Min-Max Optimization [85.84019017587477]
  Distributionally robust supervised learning is emerging as a key paradigm for building reliable machine learning systems for real-world applications. Existing algorithms for solving Wasserstein DRSL involve solving complex subproblems or fail to make use of gradients. We revisit Wasserstein DRSL through the lens of min-max optimization and derive scalable and efficiently implementable extra-gradient algorithms.
  arXiv  Detail & Related papers  (2021-04-27T16:56:09Z)
• Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods [28.72161643908351]
  This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems.
  arXiv  Detail & Related papers  (2020-07-31T22:01:39Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.