Decentralized LTL Enforcement
Decentralized LTL Enforcement
复制标题
分散零担执法
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Yliès Falcone
中科院分区：
文献类型：
--
作者：
F. Gallay;Yliès Falcone
我们考虑在没有中心观察点或权威的去中心化系统上线性时间时态逻辑公式的运行时执行。每个系统组件都附加了一个所谓的执行器，并观察其本地跟踪。如果全局跟踪违反规范，执行者将协调纠正其本地跟踪。我们形式化了去中心化的运行时执行问题，并定义了执行者的预期属性，即稳健性、透明度和最优性。我们提出了两种执行算法。在第一个中，执行者探索所有可能的局部修改，以找到最佳的全局修正。虽然这保证了最佳校正，但它迫使系统同步，并且在计算和通信方面成本更高。在第二个中，每个执行者在通信之前进行本地更正。该版本成本的降低是以执行者修正的最优性为代价的。
We consider the runtime enforcement of Linear-time Temporal Logic formulas on decentralized systems with no central observation point nor authority. A so-called enforcer is attached to each system component and observes its local trace. Should the global trace violate the specification, the enforcers coordinate to correct their local traces. We formalize the decentralized runtime enforcement problem and define the expected properties of enforcers, namely soundness, transparency and optimality. We present two enforcement algorithms. In the first one, the enforcers explore all possible local modifications to find the best global correction. Although this guarantees an optimal correction, it forces the system to synchronize and is more costly, computation and communication wise. In the second one, each enforcer makes a local correction before communicating. The reduced cost of this version comes at the price of the optimality of the enforcer corrections.