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.
翻译:我们考虑对没有中央观察点和权威的分散系统实施线性时空逻辑公式的运行时间,每个系统组成部分都配有所谓的执行者,并观察其本地跟踪。如果全球跟踪违反规格,执行者协调纠正其本地跟踪。我们将分散运行时间执行问题正式化,并界定执行者的预期特性,即稳妥性、透明度和最佳性。我们提出两种执行算法。在第一个系统中,执行者探索所有可能的本地修改,以找到最佳的全球更正。虽然这保证了最佳更正,但迫使系统同步化,而且费用更高,计算和沟通明智。在第二个系统中,每个执行者在沟通前都进行本地更正。本版本成本的降低是以执行者最佳性校正为代价的。