一阶分支时间属性的双向运行时强制执行
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
AI总结：
本文提出双向运行时强制执行框架，研究sHML安全属性的可执行性，并给出自动综合函数生成动作禁用监视器以保障系统正确性。
摘要：
运行时强制执行是一种动态分析技术，它通过将监视器与系统结合，以确保系统满足由某个属性所指定的正确性。本文探讨了针对描述系统输入和输出行为的属性的双向强制执行策略。我们开发了一个用于双向强制执行的操作框架，并利用该框架研究带递归的Hennessy-Milner逻辑的安全片段（sHML）的可执行性。我们提供了一种自动综合函数，该函数能够从sHML公式生成正确的监视器，并证明该逻辑可通过一种特定类型的双向强制执行监视器（称为动作禁用监视器）来执行。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
