AI 中文总结
本文针对部分可观测运行时验证问题，提出概率迹表达式（PTEs）的新语法与语义，改进原PTE的概率关联方式，支持间隙推理与信念监测，涵盖隐马尔可夫模型，通过火星车场景验证其应用。
AI 中文摘要
运行时验证（RV）技术通常在系统执行完全可观测的假设下定义。然而在许多现实场景中，监测器必须在部分可观测的情况下运行，此时事件可能丢失、延迟或不可观测。这引发了关于监测期间如何解释规范、判定结果和不确定性的基本问题。本文提出了概率迹表达式（PTEs）的新语法与语义，这是一个将概率推理整合到迹表达式操作语义中的形式框架。迹表达式（TE）是我们15年前开始开发的一种高表达力的运行时验证规范形式。与2022年最初的PTE公式中将概率附加到句法转换的做法不同，现在概率与每个语义状态中启用的事件类型集合相关联，确保了超越有限状态模型的语义一致性和PTE规范的高模块化。PTE框架支持对缺失事件（间隙）的原则性推理，区分观测性和生成性概率解释——这比2022年原始PTE公式的语义更精细——并涵盖了隐马尔可夫模型等经典概率模型。我们讨论了PTE如何支持不确定性下基于信念的监测，在一个代表性的火星车场景中说明其应用，并反思其对部分可观测环境中运行时验证的概念意义。
英文摘要
Runtime Verification (RV) techniques are typically defined under the assumption of complete observability of system executions. In many realistic settings, however, monitors must operate under partial observability, where events may be lost, delayed, or unobservable. This raises fundamental questions about how to interpret specifications, verdicts, and uncertainty during monitoring. In this paper, we propose a new syntax and semantics for Probabilistic Trace Expressions (PTEs), a formal framework that integrates probabilistic reasoning into the operational semantics of Trace Expressions. Trace Expressions (TE) are a highly expressive specification formalism for runtime verification that we started to develop 15 years ago. Rather than attaching probabilities to syntactic transitions, as we did in the original formulation of PTEs dating back 2022, probabilities are now associated with the set of event types enabled in each semantic state, ensuring semantic consistency beyond finite-state models, and high modularity of the PTE specification. The PTE framework supports principled reasoning about missing events (gaps), distinguishes between observational and generative probabilistic interpretations -- which represents a more refined semantics w.r.t. the original PTE formulation of 2022 -- and subsumes classical probabilistic models such as Hidden Markov Models. We discuss how PTEs enable belief-based monitoring under uncertainty, illustrate their use in one representative Mars Rover scenario, and reflect on the conceptual implications for runtime verification in partially observable environments.
