论文标题
逻辑中的决策问题,用于推理有关可重构分布式系统的推理
Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
论文作者
论文摘要
我们考虑一种用于描述分布式系统配置集的逻辑,该系统可以通过重新配置程序在运行时更改其网络拓扑。该逻辑使用归纳定义来描述具有无限数量的组件和交互的网络,该网络使用乘法连词编写,让人联想到堆积的含义和分离逻辑。我们研究了正在考虑的配置逻辑的满意度和累积问题的复杂性。此外,我们考虑了稳健性的特性,例如紧密度(所有相互作用都完全连接到组件?)和程度界限(是否涉及界数相互作用的每个组件?),后者是可确定性的成分。
We consider a logic used to describe sets of configurations of distributed systems, whose network topologies can be changed at runtime, by reconfiguration programs. The logic uses inductive definitions to describe networks with an unbounded number of components and interactions, written using a multiplicative conjunction, reminiscent of Bunched Implications and Separation Logic. We study the complexity of the satisfiability and entailment problems for the configuration logic under consideration. Additionally, we consider robustness properties, such as tightness (are all interactions entirely connected to components?) and degree boundedness (is every component involved in a bounded number of interactions?), the latter being an ingredient for decidability of entailments.