Tags:complexity, decidability, entailment, satisfiability and separation logic

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 degree boundedness (is every component involved in a bounded number of interactions?), an ingredient for decidability of entailments.

Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems