一句话：提出双向运行时强制的操作框架，并证明带递归的Hennessy-Milner逻辑安全片段sHML可由动作禁用监视器强制。
运行时强制是一种动态分析技术：为系统装配监视器，以保证系统满足给定性质。已有工作多针对输出行为或单一方向，本文研究同时刻画系统输入与输出行为的双向强制策略。作者建立一个双向运行时强制的操作框架，并在其中研究带递归的Hennessy-Milner逻辑安全片段（sHML）的可强制性——sHML 恰好适合表达一阶分支时间的安全性质。论文给出一个自动综合函数，可由 sHML 公式生成正确的监视器，并进一步证明该逻辑可由一类特定的双向强制监视器，即动作禁用监视器（action disabling monitors）来强制。结果表明双向强制在表达能力上可覆盖经典的安全性质监测，为输入—输出双向约束下的监视器合成与可强制性分析提供了统一的形式化基础。
Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.
@article{paperbot2235,
title = {Bidirectional Runtime Enforcement of First-Order Branching-Time Properties},
author = {Luca Aceto and Ian Cassar and Adrian Francalanza and Anna Ingolfsdottir},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:14)2023}
}