Monitoring Hyperproperties
超属性，如非干扰性和观察确定性，将多个系统执行相互关联。它们不能用标准的时态逻辑（如LTL、CTL和CTL*）来表示，因此不能用标准的运行时验证技术来监视。HyperLTL扩展了线性时间时态逻辑（LTL），在迹上显式量化，以表达Hyperproperties。我们研究了HyperLTL公式在三种不同输入模型下的运行时验证问题：（1）并行模型，其中并行处理固定数量的系统执行。(2)无限顺序模型，其中系统执行是顺序处理的，每次一个执行。在这个模型中，传入执行的数量可能会永远增长。(3)有界顺序模型，其中跟踪按顺序处理，传入执行的数量是有界的。我们证明了对于输入模型（1）和（3），决定HyperLTL公式的可监控性是PSPACE完全的。对于输入模型（2）中的无替代HyperLTL公式，判定可监控性是PSPACE完全的。对于每个输入模型，我们都提供了实用的监控算法。我们还提出了各种优化技术。通过识别规范的属性，如自反性，对称性和传递性，我们减少了跟踪之间的比较次数。对于顺序模型，我们提出了一种技术，最大限度地减少了需要存储的痕迹的数量。最后，我们提供了一个优化，简洁地表示存储的痕迹共享共同的前缀。我们评估了我们的优化，表明这会导致更可扩展的监控，特别是显着降低内存消耗。
2018-07-02 cs.LO
Monitoring hyperproperties with circuits
本文根据Hyper-LTL的思想，给出了Hennessy-Milner逻辑安全片段的一种扩展，它具有迹集上的递归性。然后，它介绍了一种新的监测设置，采用类似电路的结构，结合定期监测的判决。这项研究的主要贡献是监测和他们的语义本身，以及一个监测合成程序从公式的逻辑，产生“电路样监测”的这种类型的声音和违反完成了一个有限的一组无限的痕迹。
2022-05-10 cs.LO
Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Toronto（多伦多大学）
本文针对有限迹LTL的预期监控，提出基于递进与LTLf可满足性检查的替代方法，实验表明其在算术设置下优于自动机方法，结合两者在命题设置下权衡良好。
2026-09-29 cs.AI cs.LO
Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic
信号时序逻辑监测的数值模拟轨迹已经成为一种有效的方法来近似验证的连续和混合系统。在本报告中，我们探索了STL属性的精确验证程序，该程序基于对Flow* 验证积分器生成的泰勒模型流管形式的验证痕迹进行监控。我们将探讨与Flow* 符号流管表示的紧密集成如何实现更精确、更高效的监控。然后，我们展示了如何通过引入掩码，将流管监测限制在与复杂命题的整体真相相关的时间区域的方法的属性导向的改进来大幅提高监测的性能。最后，我们将这些方法的实现应用于验证一个具有挑战性的连续系统的属性，评估我们的程序的每个方面对监控性能的影响。
2020-08-14 cs.LO
Efficient Offline Monitoring of Linear Temporal Logic with Bit Vectors
位图是一种数据结构，用于压缩表示整数集合;它提供了非常快速的查询和操作这些集合的操作，利用位级并行性。在本文中，我们描述了一种技术，离线验证的任意表达式的线性时序逻辑使用位图操作。首先对事件跟踪进行预处理并将其转换为一组位图。然后通过操作这些位图的递归过程来计算LTL表达式。实验结果表明，复杂的LTL公式包含近20个操作符，事件跟踪可以评估在每秒数百万个事件的吞吐量。
2020-05-24 cs.LO
Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking
Faculty of Informatics West University Timi s oara Romania
本文提出一种基于TLA+轨迹检查的监控工具，可从Kubernetes审计日志推断行为并检测多租户等违规，将形式化推理融入实时Kubernetes环境以提升监控与正确性检查效果。
2026-09-28 cs.DC cs.LO
A Counting Semantics for Monitoring LTL Specifications over Finite Traces
我们考虑的问题，监测的线性时间逻辑（LTL）的规格，定义在无限的路径，在有限的痕迹。例如，我们可能需要对系统是否满足或违反性质“p无穷常成立”做出裁决。“问题是，总是有一个满足该性质的有限迹的延续和一个违反它的不同延续。我们提出了一个两步的方法来解决这个问题。首先，我们引入了一个计数语义，它计算步骤的数量，以证明跟踪中每个位置的公式的满足或违反。第二，我们使用这些信息对不确定的后缀进行预测。特别是，我们认为一个好的后缀是一个短于最长的证人满意，和一个坏的后缀是短于或等于最长的证人违反。基于这一假设，我们提供了一个判决，评估是否在同一系统上执行的继续将可能满足或违反的财产。
2018-04-09 cs.FL cs.LO
Monitoring Second-Order Hyperproperties
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文针对现有超性质监控无法处理二阶性质的局限，提出支持二阶轨迹集合量化的Hyper$^2$LTL$_f$逻辑，分别给出并行模型下的规约方法和串行模型下的高效监控算法，并通过多基准实验验证有效性。
2024-04-15 cs.AI cs.LO cs.MA
Automata-less Monitoring via Trace-Checking (Extended Version)
Department of Mathematics, Computer Science and Physics University of Udine（乌迪内大学数学、计算机与物理系）
针对运行时验证中DFA监控器双指数爆炸问题，提出基于内蕴安全/共安全公式的迹检查监控方法，复杂度为多项式级，并明确了LTL和LTLf中识别这类公式的复杂度。
2025-11-14 cs.FL cs.LO
Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring
University of Udine, Italy（乌迪内大学）
针对监控技术中确定性自动机复杂度高的问题，提出将STL纯过去（共）安全片段监控简化为轨迹检查的方法，构建GPU加速的遗传编程学习框架，实现可解释早期故障检测，关键性能指标提升2-10%。
2025-08-25 cs.AI cs.FL cs.LG
The Cost of Monitoring Alone
我们比较了两个监测系统的简洁性的无限的痕迹，即并行和定期监测的属性。虽然并行监视器可以转换为等价的常规监视器，但这种转换的代价是监视器语法大小的双指数爆炸，而当目标是确定性监视器时，则是三指数爆炸。我们表明，这些界限是紧的，他们也持有相应的片段之间的翻译Hennessy-Milner逻辑递归无限的痕迹。
2019-02-13 cs.FL cs.LO
Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4
University of Washington（华盛顿大学）
研究非奇异方阵的Kannan - Bachem史密斯标准型算法，在Lean 4中形式化，通过递归减小枢轴二进制大小实现稳定终止，生成算术叶跟踪，用自定界编解码器定义输入输出大小，给出跟踪成本和矩阵编码长度的多项式界。
2026-07-27 cs.DS cs.LO cs.SC
Fast Robust Monitoring for Signal Temporal Logic with Value Freezing Operators (STL*)
本文针对STL*监控不可扩展的问题，提出带加速启发式的离线布尔与鲁棒性监控算法，首次支持嵌套冻结变量公式的长轨迹监控。
2024-09-29 cs.LO cs.SY eess.SY
On distributed monitoring of asynchronous systems
分布式系统是出了名的难以理解和分析，以维护其正确w.r.t.给定属性。一旦活动实体（对等体、代理、进程等）以异步方式运行，它们通常会表现出大量不同的行为。这样的系统的模型化已经是一项重要的任务，更不用说它们的形式化验证了。本文的目的是讨论一个简单的模型的有限状态分布式自动机的分布式监控问题的基础上共享的行动，称为异步自动机。监视是一个与运行时验证相关的问题：假设我们必须针对未知或非常复杂的系统$A$检查属性$L$，因此经典的静态分析是不可能的。因此，使用监视器而不是模型检查，它在运行时检查底层系统的属性。我们在这里感兴趣的是监视异步自动机建模的分布式系统。要求监视器与底层系统属于同一类型是很自然的，因此我们在这里考虑分布式监视。分布式监视器不具有系统的全局视图，因此我们提出了局部可监视跟踪语言的概念。我们的主要结果表明，如果分布式字母表的行动是连接的，如果$L$是一个集的无限迹，使$L$和它的补充$L^c$是可数的联合的局部安全语言，那么$L$是局部监测。我们还表明，在无限的痕迹，可识别可数工会的局部安全的语言正是确定性语言的补充。
2012-08-10 cs.FL cs.LO
Towards Runtime Monitoring of Node.js and Its Application to the Internet of Things
在过去的几年里，Node.js已经成为一个特别适合实现轻量级物联网应用程序的框架，这要归功于其底层的异步事件驱动，非阻塞I/O模型。然而，验证程序的正确性与异步嵌套回调是相当困难的，因此，运行时监控可以是一个有价值的支持，以解决这样一个复杂的任务。静态监测是一种有用的软件验证技术，它补充了静态分析和测试，但尚未在物联网（IoT）系统的背景下得到充分的探讨。跟踪表达式已成功地用于广泛的多智能体系统平台的运行时监控。最近，它们的表达能力已经扩展到允许对只能在运行时捕获和监视的数据进行参数化规范。此外，通过事件域和类型的概念，它们可以是语言和系统不可知的。本文研究了使用参数跟踪表达式作为Node.js和Node-RED（一种基于流的物联网编程工具，构建在Node.js之上）中开发的程序运行时监控的第一步。这类系统的可扩展性验证是一项迄今为止在文献中似乎大多被忽视的任务。一个原型实现所提出的系统Node.js，为了动态检查跟踪表达式的API函数的正确使用，提出。该工具利用动态分析框架Jalangi来监控Node.js程序，并允许检测其他技术难以捕获的错误。此外，它还提供了一个简单的REST接口，可用于Node-RED组件的运行时验证，更广泛地说，可用于物联网设备。
2018-02-06 cs.LO cs.PL cs.SE
RuleRunner technical report
基于规则的有限轨迹运行时监控系统，具有FTL判决和二次复杂性。
2013-06-01 cs.LO cs.SE
Efficient Monitoring of Timed Properties
Aalborg University（奥尔堡大学）；Queens University（女王大学）
本文针对实时系统的定时性质，提出基于差分边界矩阵的高效符号在线监测算法，在工具 MoniTAal 中实现后可有效监测长轨迹上的性质。
2026-08-05 cs.FL cs.LO
QTWTL: Quality Aware Time Window Temporal Logic for Performance Monitoring
University of Missouri-Columbia（密苏里大学哥伦比亚分校）
本文提出质量感知时间窗口时序逻辑QTWTL，通过扩展TWTL增加计数与聚合算子，并设计离线运行时监控算法，利用纽约市出租车轨迹数据验证其线性时空复杂度。
2023-08-10 cs.LO cs.PF cs.RO
Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
Free University of Bozen-Bolzano（博尔扎诺自由大学）
动态系统及其操作数据的组合建模和验证在人工智能和多个应用领域中获得了发展势头。我们研究了数据感知动态系统（DDS）的表达而简洁的框架，用线性算法对其进行了扩展，并提供了以下贡献。首先，我们引入了一个新的，语义属性的“有限总结”，这保证了一个忠实的有限状态抽象的存在。我们依靠这一点来证明，检查证人是否存在的线性时间，有限跟踪属性是可判定的DDS有限总结。第二，我们证明了在形式化方法和数据库理论中研究的几个可判定性条件可以被看作是这个属性的具体的、可检查的实例。这也产生了新的可判定性结果。第三，我们展示了如何抽象的，统一的属性有限总结导致模块化的结果：一个系统享有有限总结，如果它可以被适当地划分成更小的系统，拥有的财产。我们的研究结果使我们能够分析在早期方法中无法实现的系统。最后，我们证明了我们的方法在原型实现的可行性。
2022-03-15 cs.AI cs.LO
An Efficient Algorithm for Monitoring Practical TPTL Specifications
Arizona State University（亚利桑那州立大学）
本文提出一种动态规划算法，用于监控TPTL片段的规范，该片段比度量时序逻辑更 expressive，通过独立时间变量提取复杂实时需求，并提供多项式时间算法和实验结果。
2016-12-09 cs.LO cs.SY eess.SY
