Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems

TL;DR

This paper introduces a logic for modeling reconfigurable distributed systems, analyzing its complexity and robustness properties, which aids in understanding system configurations and their decidability.

Contribution

It develops a formal logic with inductive definitions for distributed system configurations and studies its satisfiability, entailment complexity, and robustness properties.

Findings

Complexity results for satisfiability and entailment problems.

Identification of robustness properties like tightness and degree boundedness.

Decidability conditions based on boundedness properties.

Abstract

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.