On an Invariance Problem for Parameterized Concurrent Systems

TL;DR

This paper investigates the havoc invariance property in parameterized concurrent systems, reducing it to an entailment problem and establishing its 2EXP complexity for a specific logic fragment.

Contribution

It introduces a formal reduction of havoc invariance to entailment, providing complexity bounds and insights into the invariance problem for concurrent systems with a resource logic.

Findings

Havoc invariance reduces to an entailment problem.

Havoc invariance is undecidable in general.

For a logic fragment, havoc invariance is in 2EXP complexity.

Abstract

We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called \emph{havoc invariance}, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem $\phi \models \psi$, asking if any model of $\phi$ is also a model of $\psi$. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.