发表机构
Free University of Bozen-Bolzano; University of Toronto（博尔扎诺自由大学; 多伦多大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对有限迹LTL的预期监控，提出基于递进与LTLf可满足性检查的替代方法，实验表明其在算术设置下优于自动机方法，结合两者在命题设置下权衡良好。
AI 中文摘要
当安全关键系统根据已知的内部规范进行开发时，其正确性可以通过模型检查来确立。在规范未知或不可访问的常见情况下，运行时验证提供了一种有吸引力的替代方案，例如，用于确认自主系统和智能体系统以及业务流程满足期望的属性并/或符合安全要求。在本文中，我们研究了预期监控，这是一种高级的运行时验证形式，其中监控状态由迄今为止所见到的迹前缀及其所有可能的有限长度未来延续共同决定。我们专注于监控可能涉及算术约束的线性时间属性。基于自动机的方法是该领域的实际标准，以其计算复杂性而著称。我们提出了一种基于递进和LTLf可满足性检查的替代方法，适用于命题和算术两种设置。我们通过实验比较了基于自动机的方法、基于递进的方法以及结合两者的第三种方法。我们的实验表明，基于递进的方法在自动机构造无法终止时通常能够成功产生判定，尤其是在算术设置下。对于命题设置，结合技术提供了良好的权衡。
英文摘要
When safety-critical systems are developed from a known internal specification, their correctness can be established by model checking. In the frequent case where such a specification is unknown or inaccessible, runtime verification presents an attractive alternative, e.g., to ascertain that autonomous and agentic systems as well as business processes satisfy desirable properties and/or comply with safety requirements. In this paper we study anticipatory monitoring, an advanced form of runtime verification, where the monitoring state is determined by both the trace prefix seen so far, and all its possible finite-length, future continuations. We focus on monitoring linear-time properties that may involve arithmetic constraints. Automata-based approaches, the de-facto standard in this setting, are notorious for their computational complexity. We propose an alternative approach based on progression and LTLf satisfiability checking, for both propositional and arithmetic settings. We experimentally compare the automata- and progression-based approaches, and a third method that combines the two. Our experiments suggest that the progression-based approach often succeeds in producing a verdict when the automata constructions do not terminate, especially for the arithmetic setting. For the propositional setting, the combined technique provides a good tradeoff.
