Quantitative Monitoring of Signal First-Order Logic
Zeroth Research（零次研究）；Institute of Science and Technology Austria（奥地利科学技术研究所）；CISPA Helmholtz Center for Information Security（CISPA赫尔姆霍兹信息安全中心）；Leiden University（莱顿大学）
本文提出了一种基于鲁棒性的SFO定量语义，实现了对信号一阶逻辑的高效在线监测，并展示了其在实时属性评估中的有效性。
2026-03-03 cs.LO cs.SE cs.SY
Model Predictive Monitoring of Dynamical Systems for Signal Temporal Logic Specifications
针对安全关键信息物理系统的在线监测需求，提出基于已知系统模型的模型预测监测方法，通过预测未来状态提前证伪或验证STL规范，经真实案例验证有效。
2023-11-09 cs.FL cs.SY eess.SY
Robust Control for Signal Temporal Logic Specifications using Average Space Robustness
KTH Royal Institute of Technology（皇家理工学院）
本文提出了一种计算高效且鲁棒的模型预测控制框架，用于满足信号时间逻辑规范，引入了新的量化语义'离散平均空间鲁棒性'并将其纳入模型预测控制器的成本函数，通过凸二次规划实现规范的鲁棒满足，并定义了谓词鲁棒性度量来评估鲁棒性。
2019-01-15 cs.SY eess.SY
Ro-To-Go! Robust Reactive Control with Signal Temporal Logic
本文提出了一种新的信号时间逻辑鲁棒性度量方法Ro-To-Go，用于改进模型预测控制中的机器人控制，通过隔离后缀轨迹的贡献，提高决策能力，并在仿真中验证了其有效性。
2026-05-18 cs.SY eess.SY
Towards formalization and monitoring of microscopic traffic parameters using temporal logic
智慧城市正在通过技术整合彻底改变交通基础设施。然而，确保各种运输系统组件按预期并以安全的方式运行是一个巨大的挑战。在这项工作中，我们提出了使用正式的方法作为一种手段来指定和原因的交通网络的复杂属性。形式化方法提供了一个灵活的工具来定义交通网络的安全运行，通过捕获不符合的行为，探索各种可能的状态的交通场景，并检测其中的任何不一致之处，因此，我们开发了基于规范的监测交通网络的分析使用的形式语言，信号时序逻辑。我们开发的监控器可识别与安全相关的行为，例如遵守速度限制和保持适当的车头时距。该框架进行了测试，使用校准的微观模拟高速公路的情况下，离线规范为基础的监控应用于个别车辆的轨迹，以了解他们是否违反或满足定义的安全规范。输出的统计分析表明，我们的方法可以区分违反符合车辆轨迹的基础上定义的规格。交通管理中心可以利用这项工作来研究交通流特性，识别可能的危险，并为交通监控系统的自动化提供有价值的反馈。
2021-10-12 cs.CY cs.SY eess.SY
Robust Online Monitoring of Signal Temporal Logic
Toyota Technical Center（丰田技术中心）；University of California Berkeley（加州大学伯克利分校）
本文提出一种鲁棒在线监控信号时序逻辑部分轨迹的语义，通过高效算法在汽车领域和MOOC教学中验证，显著降低计算成本。
2015-06-26 cs.SY eess.SY
Specifying User Preferences using Weighted Signal Temporal Logic
我们扩展信号时序逻辑（STL），使规范的重要性和优先级。该扩展名为加权STL（wSTL），具有与STL相同的定性（布尔）语义，但还定义了与布尔和时间运算符相关的权重，以调节其定量语义（鲁棒性）。我们证明了wSTL的鲁棒性可以定义为所有已知兼容鲁棒性泛函的加权推广（即，在公式上递归定义的鲁棒性得分），其可以考虑wSTL公式中的权重。我们利用这种加权的鲁棒性来区分信号相对于一个所需的wSTL公式，具有不同的重要性或优先级和时间偏好的子公式，并证明其有用的冲突任务的问题，其中所有任务的满意度不能实现。我们还采用wSTL鲁棒性的优化框架，合成控制器，最大限度地满足用户指定的偏好的规范。
2020-10-02 cs.SY eess.SY
Robustness Analysis for Value-Freezing Signal Temporal Logic
Faculty of Informatics Masaryk University（马萨里克大学信息学院）
本文基于STL*逻辑，定义了鲁棒性度量，并提出计算算法，通过案例展示其应用。
2013-09-03 cs.CE cs.LO cs.SY
Robust Motion Planning employing Signal Temporal Logic
Royal Institute of Technology (KTH)（皇家理工学院）
本文提出结合信号时序逻辑与模型预测控制的鲁棒运动规划方法，通过引入离散平均空间鲁棒性指标提升对噪声的抗干扰能力。
2017-03-06 cs.SY eess.SY
Lipschitz Continuity of Signal Temporal Logic Robustness Measures: Synthesizing Control Barrier Functions from One Expert Demonstration
本文提出一种从单次专家演示构造控制障碍函数的方法，利用信号时序逻辑鲁棒性度量的Lipschitz连续性合成时变CBF，通过过滤控制输入确保系统轨迹满足规约，并在Robotarium上验证了有效性。
2023-04-07 cs.SY eess.SY
Online Causation Monitoring of Signal Temporal Logic
针对经典STL在线监测因鲁棒性区间单调收缩而无法及时报告新违反或精确描述系统演化的问题，本文提出布尔与定量因果监测器，以更细粒度刻画每个时刻与规约违反或满足的因果关系，并在不显著增加监测成本的前提下提供更详细的系统演化信息。
2023-05-28 cs.FL cs.LO cs.SY
Temporal Robustness of Temporal Logic Specifications: Analysis and Control Design
我们研究了时序逻辑规范的时间鲁棒性，并展示了如何为时间关键控制系统设计时间鲁棒控制律。这个主题在连接系统和交错过程中特别感兴趣，例如多机器人和人机系统，其中个体代理和人类行为的不确定性可能会导致时序不确定性。尽管时间关键系统的重要性，时序逻辑规范的时间鲁棒性还没有研究，特别是从控制设计的角度来看。我们定义同步和异步的时间鲁棒性，并表明这些概念量化的鲁棒性相对于同步和异步的时间转移的时间逻辑规范的谓词。进一步证明了同步时间鲁棒性是异步时间鲁棒性的上界。然后，我们研究的控制设计问题，我们的目标是设计一个控制律，最大限度地提高了动力系统的时间鲁棒性。我们的解决方案包括一个混合线性规划（MILP）编码，可用于获得一系列的最优控制输入。虽然异步时间鲁棒性可以说是比同步时间鲁棒性更细致入微，我们表明，控制设计使用同步时间鲁棒性是计算更有效。设计人员可以根据手头的特定应用程序来利用这种权衡。我们总结了各种案例研究的文件。
2022-03-29 cs.FL cs.SY eess.SY
Monitoring electrical systems data-network equipment by means of Fuzzy and Paraconsistent Annotated Logic
Centro Universitário FEI（FEI大学中心）；Flinders University（弗林德斯大学）；Universidade Santa Cecília（圣塞西利亚大学）
从IT数据networkelements获得的信息的数量和复杂性不断增加，为了对其进行正确的监控和管理，这是一个现实。同样的情况也发生在电力系统中的数据网络上，这些网络为变电站和水力发电厂提供有效的监督和控制。造成这一事实的原因是越来越多的设施和新的环境受到这种数据网的监测，以及所涉及的技术不断发展。这种情况可能导致数据不完整和/或矛盾，必须解决这些问题，以保持良好的监测水平，从而管理这些系统。在本文中，一个专家系统的原型开发，以监测电力系统中的数据网络的设备的状态，它处理不一致，而不淡化的推理。这是在水电站和变电站的远程控制的情况下完成的区域操作中心（ROC）。专家系统是用模糊逻辑和二值次协调注释逻辑（PAL 2 v）相结合的算法开发的，以分析不确定信号并产生设备的运行状态（故障、正常、不稳定或不一致/不确定），这些状态被识别为水电厂和变电站远程控制的重要状态。该专家系统的原型安装在虚拟服务器上，带有CLP 500软件（来自EFACEC制造商），用于调查由区域（巴西）运营中心组成的场景，具有通用变电站和通用水电厂，代表远程控制环境。
2021-05-24 cs.AI cs.SY eess.SY
On Expressing and Monitoring Oscillatory Dynamics
Faculty of Informatics Masaryk University（马萨里克大学信息学院）
本文提出扩展的信号时序逻辑STL*，通过引入信号值冻结算子来增强表达能力，以区分生物学中重要的振荡特性，并实现了监控算法。
2012-08-19 cs.CE cs.LO cs.NA
An Efficient Algorithm for Monitoring Practical TPTL Specifications
Arizona State University（亚利桑那州立大学）
本文提出一种动态规划算法，用于监控TPTL片段的规范，该片段比度量时序逻辑更 expressive，通过独立时间变量提取复杂实时需求，并提供多项式时间算法和实验结果。
2016-12-09 cs.LO cs.SY eess.SY
Smooth Robustness Measures for Symbolic Control Via Signal Temporal Logic
本文针对符号控制中STL鲁棒性度量非平滑非凸问题，推广并提出四种平滑鲁棒性度量，引入误差与梯度语义以优化选择并提高计算效率，经仿真验证。
2023-05-16 cs.SY eess.SY
A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control
University of Notre Dame（圣母大学）
近年来，越来越多地使用信号时序逻辑（STL）作为符号控制的形式化规范语言，由于其表达能力和接近自然语言。此外，STL规范可以使用STL的鲁棒语义编码为代价函数，将合成问题转换为优化问题。不幸的是，这些代价函数是非光滑和非凸的，并且使用混合整数规划的精确解不能很好地缩放。最近的工作集中在使用平滑近似的鲁棒性，这使得更快的基于梯度的方法找到局部最大值，以牺牲稳健性和/或完整性。我们提出了一种新的鲁棒性近似，是光滑的，声音，渐近完成。我们的方法结合了现有近似的优点，同时使保守性和完整性之间的明确权衡。
2020-06-09 cs.RO cs.SY eess.SY
Stochastic Robustness Interval for Motion Planning with Signal Temporal Logic
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出一种针对STL规范的连续时间随机轨迹鲁棒性度量及其监控器，并基于此开发了不确定性下机器人的采样运动规划算法，证明了概率完备性与渐近最优性。
2023-05-28 cs.FL cs.RO cs.SY
Logical Signal Processing: a Fourier Analysis of Temporal Logic
时态逻辑公式的频率内容是什么？也就是说，当我们根据公式监测信号时，信号的哪些频段与逻辑相关，应该保留，哪些可以安全地丢弃？这个问题与信号在被监测之前被滤波或压缩时有关，这几乎总是模拟信号的情况。为了回答这个问题，我们专注于测量信号相对于信号时序逻辑规范的鲁棒性的监视器。我们证明了鲁棒性监视器可以使用Volterra系列建模。然后研究了这些Volterra表示的傅里叶变换，并给出了一种推导整个公式的傅里叶变换的方法.我们还明确了时间逻辑的测量过程，并重新定义它的基础上的分布，使其与测量兼容的信号处理。实验证明了这些结果。除了压缩之外，这项工作还可以将时序逻辑监控集成到常见的信号处理工具链中，作为另一种信号处理操作，并实现一种常见的形式主义来研究频域中的逻辑和非逻辑操作，我们将其称为逻辑信号处理。
2020-09-17 cs.SY eess.SY
Synthesis of Temporally-Robust Policies for Signal Temporal Logic Tasks using Reinforcement Learning
针对未知随机环境下STL控制策略设计问题，提出兼顾时序鲁棒性的两个控制目标，通过近似处理适配标准Q-learning算法并推导理论边界，经案例验证方法可行。
2024-03-23 cs.SY eess.SY
Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics
Boston University（波士顿大学）；TU Wien（维也纳工业大学）
本文提出了一种从复杂时间约束生成非线性动态系统控制策略的框架，引入了平滑且可微的累积鲁棒性语义，并通过梯度上升算法求解一系列平滑优化问题来高效生成控制策略，同时展示了如何将这些技术整合到模型预测控制框架中以实现长时间 horizon 的控制策略合成。
2019-04-25 cs.SY eess.SY
Robust Multi-Agent Coordination from CaTL+ Specifications
本文将CaTL扩展为更具表达力的CaTL+逻辑，提出传统鲁棒性和指数鲁棒性两种度量，并通过两步优化方法实现多智能体控制综合，仿真验证了方法的有效性。
2023-04-12 cs.SY eess.SY
Multi-Agent Control Synthesis from Global Temporal Logic Tasks with Synchronous Satisfaction Requirements
本文研究异构智能体在全局时序逻辑任务下的控制问题，提出基于全局STL公式和同步鲁棒性度量的MILP编码方法，实现高同步性与最小代价的运动规划，且计算复杂度仅为线性。
2024-11-14 cs.SY eess.SY
Robust Satisfaction of Temporal Logic Specifications via Reinforcement Learning
Georgia Institute of Technology（佐治亚理工学院）；Boston University（波士顿大学）；Stanford University（斯坦福大学）
本文提出通过强化学习最大化满足信号时序逻辑规范的概率和鲁棒性，通过机器人导航仿真验证其在概率和鲁棒性上的优越性。
2015-10-22 cs.RO cs.SY eess.SY
pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems
Oklahoma State University（俄克拉荷马州立大学）
提出pdSTL框架，将概率语义与可微鲁棒性结合，通过区间值概率语义和LSTM式展开实现线性时间可微监控，在障碍物规避、换道和真实四旋翼飞行实验中优于确定性可微STL。
2026-06-19 cs.RO cs.SY eess.SY
RRT* Based Optimal Trajectory Generation with Linear Temporal Logic Specifications under Kinodynamic Constraints
Centre for Cyber-Physical Systems, IISc（印度科学学院网络物理系统中心）
提出一种基于RRT*的轨迹生成方法，结合LTL鲁棒性度量与运动约束，通过递归成本函数平衡可行性与逻辑正确性，经仿真和实验验证，适用于复杂真实场景。
2024-11-09 cs.RO cs.SY eess.SY
Interval Signal Temporal Logic from Natural Inclusion Functions
本文提出区间信号时序逻辑 ISTL，利用自然包含函数递归构造区间鲁棒性语义，以处理不确定信号与谓词，并通过离线监测和在线控制综合示例验证其易用性。
2023-12-11 cs.SY eess.SY
Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods
Stanford University（斯坦福大学）；Toyota Research Institute（丰田研究院）
提出了一种利用计算图计算信号时序逻辑（STL）公式的定量语义的方法，称为STLCG。STLCG提供了一个平台，使逻辑规范纳入机器人问题，受益于基于梯度的解决方案。具体来说，STL是一种功能强大、表达能力强的形式化语言，它可以指定连续系统和混杂系统产生的信号的空间和时间属性。STL的定量语义提供了一个鲁棒性度量，即，信号满足或违反STL规范的程度。在这项工作中，我们设计了一个系统的方法来翻译STL的鲁棒性公式到计算图。通过这种表示，并利用现成的自动微分工具，我们能够有效地通过STL鲁棒性公式进行反向传播，从而实现STL规范与机器人技术中使用的许多基于梯度的方法的自然和易于使用的集成。通过一些来自各种机器人应用的例子，我们证明了STLCG是通用的，计算效率高，并能够将人类领域的知识到问题的制定。
2021-12-27 cs.CL cs.LO cs.SY
Risk of Stochastic Systems for Temporal Logic Specifications
数据的广泛可用性，加上人工智能和机器学习的计算进步，有望实现许多未来技术，如自动驾驶。虽然这些技术已经有了各种成功的示范，但多次报告了关键的系统故障。即使这种系统故障很少见，但如果没有严格的风险评估，这种系统故障也会对采用构成严重障碍。本文提出了一个系统和严格的系统风险验证的框架。我们认为制定信号时序逻辑（STL）的系统规范和模型的系统作为一个随机过程，允许离散时间和连续时间的随机过程。然后，我们将STL鲁棒性风险定义为缺乏鲁棒性的风险。这个定义的动机是因为系统故障往往是由于缺乏鲁棒性的建模误差，系统干扰，并在底层数据生成过程中的分布变化。在定义中，我们允许一般类别的风险度量，并专注于尾部风险度量，如风险价值和条件风险价值。虽然STL鲁棒性风险一般难以计算，但我们提出了近似的STL鲁棒性风险作为一个更易于处理的概念，该概念将STL鲁棒性风险上限化。我们展示了如何从系统轨迹数据中准确估计近似STL鲁棒性风险。对于离散时间随机过程，我们证明了在何种条件下近似STL鲁棒性风险甚至可以精确计算。我们说明了我们的验证算法在自动驾驶模拟器CARLA和显示如何风险最小的控制器可以选择四个神经网络车道保持控制器的五个有意义的系统规范。
2022-10-08 cs.FL cs.LO cs.SY
Monitoring Bounded LTL Properties Using Interval Analysis
Tokyo Institute of Technology（东京工业大学）；CNRS, IRCCyN（法国国家科学研究中心，IRCCyN）
本文提出一种区间方法用于验证由有界线性时序逻辑描述的属性，通过前向模拟混合自动机并传播时间区间来验证属性，证明了问题的可判定性。
2015-07-14 cs.LO cs.NA cs.SY
Technical Report: Distribution Temporal Logic: Combining Correctness with Quality of Estimation
Boston University（波士顿大学）
本文提出分布时间逻辑（DTL），用于描述部分可观测系统中涉及不确定性和可能性的属性，提供了一种安全的公式化方法及监控算法，并通过救援机器人应用案例验证。
2013-09-09 cs.AI cs.LO cs.SY
Feasibility-aware Learning of Robust Temporal Logic Controllers using BarrierNet
Amazon Robotics（亚马逊机器人）；Department of Mechanical Engineering（机械工程系）；Worcester Polytechnic Institute（沃斯堡技术学院）；Department of Electrical and Computer Engineering and the Department of Computer Science（电气与计算机工程系和计算机科学系）
本文提出一种基于BarrierNet的鲁棒时序逻辑控制器学习方法，通过可训练的高阶控制屏障函数约束和统一鲁棒性度量，实现对STL规范的严格满足，无需手动调参。
2026-01-28 cs.LG cs.SY eess.SY
Robust Linear Temporal Logic
University of California at Los Angeles（加州大学洛杉矶分校）
本文提出鲁棒LTL，通过多值语义定义鲁棒性，证明验证和合成问题可解，验证问题在子公式数量上指数时间，合成问题双指数时间。
2015-10-30 cs.LO cs.SY eess.SY
Local Descent For Temporal Logic Falsification of Cyber-Physical Systems (Extended Technical Report)
School of Computing, Informatics, and Decision Systems Engineering Arizona State University（亚利桑那州立大学计算、信息学与决策系统工程学院）
本文提出利用局部下降方法结合模拟退火，以解决时序逻辑下物理系统的失效问题，通过优化鲁棒性度量来寻找不安全行为。
2018-02-13 cs.FL cs.SY eess.SY
Signal Temporal Logic Meets Convex-Concave Programming: A Structure-Exploiting SQP Algorithm for STL Specifications
Université Paris-Saclay（巴黎-萨克雷大学）；Osaka University（大阪大学）；Kyoto University（京都大学）
针对带STL规范的控制问题中现有SQP方法易陷局部极小值的缺陷，提出基于CCP的结构利用型SQP算法，通过鲁棒性分解构造DC规划并仅近似析取部分求解，在鲁棒性和计算时间上均优于现有方法。
2023-05-16 cs.FL cs.RO cs.SY
Barrier Function-based Collaborative Control of Multiple Robots under Signal Temporal Logic Tasks
KTH Royal Institute of Technology（KTH皇家理工学院）
最近的兴趣在网络物理和自主机器人系统的动机下，我们研究了一组信号时序逻辑任务下的动态耦合多智能体系统的问题。特别是，这些信号时序逻辑任务中的每一个的满意度取决于一组不同的代理的行为。而不是抽象的代理动力学和时序逻辑任务到一个离散的域，并解决其中的问题，或使用基于优化的方法，我们得到的合作反馈控制律。这些控制法是基于一个分散的控制障碍函数的条件下，在不连续的控制法的结果，而不是一个集中的条件类似的单代理的情况下。我们的方法的好处是固有的鲁棒性通常存在于反馈控制以及连续时间多智能体系统的满意度保证。更具体地，使用时变控制障碍函数，其考虑了手头的信号时间逻辑任务的语义。对于信号时序逻辑任务的某个片段，我们进一步提出了一种系统的方法来构造这样的控制障碍函数。最后，我们在一个实验中，包括一组三个全向机器人，我们的框架的有效性和鲁棒性。
2021-02-04 cs.FL cs.RO cs.SY
