通过信号时序逻辑规范的反向传播：将逻辑结构注入基于时序的方法
Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods
摘要：
提出了一种利用计算图计算信号时序逻辑（STL）公式的定量语义的方法，称为STLCG。STLCG提供了一个平台，使逻辑规范纳入机器人问题，受益于基于梯度的解决方案。具体来说，STL是一种功能强大、表达能力强的形式化语言，它可以指定连续系统和混杂系统产生的信号的空间和时间属性。STL的定量语义提供了一个鲁棒性度量，即，信号满足或违反STL规范的程度。在这项工作中，我们设计了一个系统的方法来翻译STL的鲁棒性公式到计算图。通过这种表示，并利用现成的自动微分工具，我们能够有效地通过STL鲁棒性公式进行反向传播，从而实现STL规范与机器人技术中使用的许多基于梯度的方法的自然和易于使用的集成。通过一些来自各种机器人应用的例子，我们证明了STLCG是通用的，计算效率高，并能够将人类领域的知识到问题的制定。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
