有限时间内的无穷

中文摘要 AI 辅助

线性时间时序性质（如线性时间时序逻辑LTL所描述的性质）通常被建模为无穷迹的集合。然而在运行时验证场景（如系统测试或监控）中，仅能观测到系统行为的有限前缀。对于部分性质，这些有限前缀是确定性的——无需进一步观测即可给出是或否的答案。通过用这些确定性前缀丰富LTL的语义，我们对LTL₃的语义给出了恰当的归纳说明，LTL₃是一种面向运行时验证应用的多值线性时间时序逻辑。前人工作中LTL₃的语义仅通过其与传统LTL的关系给出，我们证明了LTL和LTL₃的语义是同构的。此外，我们将运行时验证场景中常用的公式演进评估技术形式化，并证明其相对于我们的语义在有限迹范围内是可靠且完备的。接着，我们转向更一般的线性时间性质：利用确定性前缀理论，我们重新证明了著名的安全-活性分解定理，并重构了无穷迹的拓扑结构。我们为性质定义了可监控性，为各类可监控性类别提供了简洁的拓扑特征，并将它们组织成一个层次结构。我们所有的定义和证明均在Isabelle/HOL中实现了机械化。

英文摘要

Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context, such as when testing or monitoring a system, only a finite prefix of the system's behaviour can be observed. For some properties, these finite prefixes may be definitive---a yes or no answer can be given without further observation. By enriching the semantics of LTL with these definitive prefixes, we give a proper inductive accounting of the semantics of LTL$_3$, a multi-valued variant of Linear-time Temporal Logic for run-time verification applications. The semantic descriptions of LTL$_3$ in previous work are given only in terms of their relationship to conventional LTL. We show that the semantics of LTL and of LTL$_3$ are isomorphic. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification contexts, and show its soundness and completeness up to finite traces with respect to our semantics. Then, we turn to linear-time properties more generally: using our theory of definitive prefixes, we re-prove the well-known safety-liveness decomposition theorem, and reconstruct the topology of infinite traces. We define monitorability for properties, providing neat topological characterisations for various monitorability classes, and arrange them into a hierarchy. All of our definitions and proofs are mechanised in Isabelle/HOL.

补充信息

备注

This paper contains the material of arXiv:2411.14581