Retrieval-Augmented Mining of Temporal Logic Specifications from Data

将网络物理系统（CPS）整合到日常生活中，使确保其安全和可靠性变得至关重要。在这方面迈出的重要一步是需求挖掘，即从观察到的行为中推断出形式化指定的系统属性，以便发现有关系统的知识。信号时间逻辑（STL）提供了一种简洁而表达力强的语言，用于指定要求，特别适用于CPS，其中行为通常表示为时间序列数据。本文针对数据驱动的方式从观察到的行为中学习STL要求，重点关注二元分类，即推断系统的属性，这些属性能够区分正常和异常行为，并且既可用作分类器，也可用作CPS符合期望规范的监视器。我们提出了一种新颖的框架，将贝叶斯优化（BO）和信息检索（IR）技术相结合，以同时学习STL公式的结构和参数，而不限制STL语法。具体而言，我们提出了一种框架，利用包含数百万公式的语义保持连续表示的密集向量数据库进行查询，以促进BO循环内的需求挖掘。我们在几个信号分类应用程序中展示了我们方法的有效性，展示了它从系统执行中提取可解释洞察力的能力，并推进了CPS需求挖掘的最新技术。

论文旨在解决将Signal Temporal Logic (STL)应用于Cyber-Physical Systems (CPS)的要求挖掘问题，以确保CPS的安全性和可靠性。

论文提出了一种结合贝叶斯优化和信息检索技术的框架，用于在数据驱动的方式下学习STL要求，同时学习STL公式的结构和参数，从而提高CPS的分类和监测性能。

论文的亮点包括使用密集向量数据库来查询数百万个公式，以便在BO循环中挖掘要求；在几个信号分类应用中展示了该方法的有效性和可解释性；为CPS的要求挖掘提供了一个新的数据驱动框架。

近期的相关研究包括：'Learning-Based Synthesis of Correct-by-Construction Controllers for CPS'，'A Survey of Signal Temporal Logic: Specification, Verification, and Synthesis'，'Mining Temporal Specifications for Cyber-Physical Systems from Execution Traces'等。