树状监视器的策略变更

中文摘要 AI 辅助

我们研究了在长期运行系统的运行时验证中出现的策略变更问题。此类场景中通常使用的在线监视器一般是树状的，即它们维护着子状态，用于监视目标策略的子公式。我们考虑了在受监视系统运行期间，仅利用监视器状态中存储的信息，何时以及如何能够变更策略。例如，这对于考虑新的系统功能或监管要求的变化是相关的。我们在一个通用设置中正式定义了策略变更问题，该设置独立于任何特定的（树状）监视器实现。然后我们证明，对于过去时间度量时序逻辑（pMTL），策略变更是可判定的，但具有紧的非原始递归下界和上界，而在离散时间语义下，它是EXPSPACE完全的。

英文摘要

We study the policy change problem that arises in the runtime verification of long-running systems. The online monitors typically used in this context are generally treelike, in that they maintain substates that monitor subformulae of the target policy. We consider when and how the policy can be changed while the monitored system is running by only exploiting the information stored in the monitor's state. This is relevant, for example, to account for new system functionality or changes in regulatory requirements. We formally define the policy change problem in a general setting, independent of any specific (treelike) monitor implementation. We then show that policy change for past-time metric temporal logic (pMTL) is decidable but has tight non-primitive recursive lower and upper bounds, while with discrete-time semantics it is EXPSPACE-complete.

发表机构

• Institute of Information Security, Department of Computer Science, ETH Zurich（苏黎世联邦理工学院信息系信息安全研究所）

机构由 AI 辅助整理，请以论文原文为准。