AI 中文总结
针对传统运行时验证未考虑预测延续的问题，提出结合观测执行监控与预测延续分析的SplitLTL形式框架，定义其语法语义并设计在线监控架构，以实现自主系统的运行时保证。
AI 中文摘要
自主系统的运行时保证日益需要不仅推理已观测到的执行过程，还要推理预期的未来行为。然而，传统运行时验证主要评估到目前为止观测到的执行，并未直接考虑预测的延续。我们提出一种运行时保证的形式框架，将对观测执行的监控与对多个预测延续的分析相结合。为支持这种集成，我们引入分离线性时态逻辑（SplitLTL），这是一种线性时间时态逻辑，在单个规范中为过去和未来的时态规范分配互补角色。过去组件利用观测到的历史确定执行当前点适用的保证要求，而未来组件则根据这些要求评估预测的延续。因此，该框架根据观测历史产生的要求过滤预测的延续，识别可支持后续决策的可允许延续。我们正式定义SplitLTL的语法和语义，并提出一种在线监控架构，用于评估观测到的执行与预测的延续。
英文摘要
Runtime assurance for autonomous systems increasingly requires reasoning not only about observed executions but also about anticipated future behaviors. Traditional runtime verification, however, primarily evaluates the execution observed so far and does not directly account for predicted continuations. We propose a formal framework for runtime assurance that combines monitoring of the observed execution with analysis of multiple predicted continuations. To support this integration, we introduce Split Linear Temporal Logic (SplitLTL), a linear-time temporal logic that assigns complementary roles to past and future temporal specifications within a single specification. The past component uses the observed history to determine the assurance requirements applicable at the current point of execution, while the future component evaluates predicted continuations against those requirements. The framework therefore filters predicted continuations according to the requirements induced by the observed history, identifying admissible continuations that can support subsequent decision making. We formally define the syntax and semantics of SplitLTL and present an online monitoring architecture for evaluating observed executions together with predicted continuations.
