Marius Bozga

Lucas Bueri

Radu Iosif

Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems

. 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.

x.out, z 1 .in chain h-1,t (z 1 , y)

Introduction

Distributed systems are increasingly used as critical parts of the infrastructure of our digital society, as in e.g., datacenters, e-banking and social networking. In order to address maintenance (e.g., replacement of faulty and obsolete network nodes by new ones) and data traffic issues (e.g., managing the traffic inside a datacenter [START_REF] Noormohammadpour | Datacenter traffic control: Understanding techniques and tradeoffs[END_REF]), the distributed systems community has recently put massive effort in designing algorithms for reconfigurable systems, whose network topologies change at runtime [START_REF] Foerster | Survey of reconfigurable data center networks: Enablers, algorithms, complexity[END_REF]. However, dynamic reconfiguration is an important souce of bugs that may result in e.g., denial of services or even data corruption 1 .

This paper contributes to a logical framework that addresses the timely problems of formal modeling and verification of reconfigurable distributed systems. The basic building blocks of this framework are (i) a Hoare-style program proof calculus [START_REF] Ahrens | Local reasoning about parameterized reconfigurable distributed systems[END_REF] used to write formal proofs of correctness of reconfiguration programs, and (ii) an invariant synthesis method [START_REF] Bozga | Verification of component-based systems with recursive architectures[END_REF] that proves the safety (i.e., absence of reachable error configurations) of the configurations defined by the assertions that annotate a reconfiguration program. These methods are combined to prove that an initially correct distributed system cannot reach an error state, following the execution of a given reconfiguration sequence.

The assertions of the proof calculus are written in a logic that defines infinite sets of configurations, consisting of components (i.e., processes running on different nodes of the network) connected by interactions (i.e., multi-party channels alongside which messages between components are transfered). Systems that share the same architectural style (e.g., pipeline, ring, star, tree, etc.) and differ by the number of components and interactions are described using inductively defined predicates. Such configurations can be modified either by (a) adding or removing components and interactions (reconfiguration), or (b) changing the local states of components, by firing interactions.

The assertion logic views components and interactions as resources, that can be created or deleted, in the spirit of resource logics à la Bunched Implications [START_REF] O'hearn | The logic of bunched implications[END_REF], or Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. The main advantage of using resource logics is their support for local reasoning [START_REF] Calcagno | Local action and abstract separation logic[END_REF]: reconfiguration actions are specified by pre-and postconditions mentioning only the resources involved, while framing out the rest of the configuration.

The price to pay for this expressive power is the difficulty of automating the reasoning in these logics. This paper makes several contributions in the direction of proof automation, by studying the complexity of the satisfiability and entailment problems, for the configuration logic under consideration. Additionally, we study the complexity of two robustness properties [START_REF] Jansen | Unified reasoning about robustness properties of symbolic-heap separation logic[END_REF], namely tightness (are all interactions entirely connected to components?) and degree boundedness (is every component involved in a bounded number of interactions?). In particular, the latter problem is used as a prerequisite for defining a fragment with a decidable entailment problem.

Motivating Example

The logic studied in this paper is motivated by the need for an assertion language that supports reasoning about dynamic reconfigurations in a distributed system. For instance, consider a distributed system consisting of a finite (but unknown) number of components (processes) placed in a ring, executing the same finite-state program and communicating via interactions that connect the out port of a component to the in port of its right neighbour, in a round-robin fashion, as in Fig. 1 (a). The behavior of a component is a machine with two states, T and H, denoting whether the component has a token (T) or not (H). A component c i without a token may receive one, by executing a transition H in -→ T, simultaneously with its left neighbour c j , that executes the transition transition T out -→ H. Then, we say that the interaction (c j , out, c i , in) has fired, moving a token one position to the right in the ring. Note that there can be more than one token, moving independently in the system, as long as no token overtakes another token.

The token ring system is formally specified by the following inductive rules:

ring h,t (x) ← ∃y∃z . [x]@q * x.out, z.in * chain h ,t (z, y) * y.out, x.in chain h,t (x, y) ← ∃z.

[x]@q * x.out, z.in * chain h ,t (z, y)

chain 0,1 (x, x) ← [x]@T chain 1,0 (x, x) ← [x]@H chain 0,0 (x, x) ← [x]
where

h def = max(h -1, 0) , if q = H h , if q = T and t def = max(t -1, 0) , if q = T t , if q = H
The predicate ring h,t (x) describes a ring with at least two components, such that at least h (resp. t) components are in state H (resp. T). The ring consists of a component x in state q, described by the formula [x]@q, an interaction from the out port of x to the in port of another component z, described as x.out, z.in , a separate chain of components stretching from z to y (chain h ,t (z, y)), and an interaction connecting the out port of component y to the in port of component x ( y.out, x.in ). Inductively, a chain consists of Fig. 1: Inductive Specification and Reconfiguration of a Token Ring a component [x]@q, an interaction x.out, z.in and a separate chain h ,t (z, y). Fig. 1 (b) depicts the unfolding of the inductive definition of the token ring, with the existentially quantified variables z from the above rules α-renamed to z 1 , z 2 , . . . to avoid confusion.

A reconfiguration program takes as input a mapping of program variables to components and executes a sequence of basic operations i.e., component/interaction creation/deletion, involving the components and interactions denoted by these variables. For instance, the reconfiguration program in Fig. 1 (c) takes as input three adjacent components, mapped to the variables x, y and z, respectively, removes the component y together with its left and right interactions and reconnects x directly with z. Programming reconfigurations is error-prone, because the interleaving between reconfiguration actions and interactions in a distributed system may lead to bugs that are hard to trace. For instance, if a reconfiguration program removes the last component in state T (resp. H) from the system, no token transfer interaction may fire and the system deadlocks.

We prove absence of such errors using a Hoare-style proof system [START_REF] Ahrens | Local reasoning about parameterized reconfigurable distributed systems[END_REF], based on the above logic as assertion language. For instance, the proof from Fig. 1 (c) shows that the reconfiguration sequence applied to a component y in state H (i.e., [y]@H) in a ring with at least h ≥ 2 components in state H and at least t ≥ 1 components in state T leads to a ring with at least h -1 components in state H and at least t in state T; note that the states of the components may change during the execution of the reconfiguration program, as tokens are moved by interactions.

For reasons of proof scalability, a basic operation is specified only with regard to the components and interactions required to avoid faulting. For instance {[x]@q} delete(x) {emp} (resp. { x.out, y.in } disconnect(x.out, y.in) {emp}) means that delete (resp. disconnect) requires a component (resp. interaction) and returns an empty configuration, whereas {emp} connect(x.out, y.in) { x.out, y.in } means that connect requires nothing and creates an interaction between the given ports of the given components. These local specifications are plugged into a context described by a frame formula F, using the frame rule {φ} P {ψ} ⇒ {φ * £ ¢ ¡ F } P {ψ * F}; for readability, the frame formulae (from the preconditions of the conclusion of the frame rule applications) are enclosed in boxes.

The proof also uses the consequence rule {φ} P {ψ} ⇒ {φ } P {ψ } that applies if φ is stronger than φ and ψ is weaker than ψ. The side conditions of the consequence rule require checking the validity of the entailments ring h,t (y) |= ∃x∃z . x.out, y.in * [y]@H * y.out, z.in * chain h-1,t (z, x) and chain h-1,t (z, x) * x.out, z.in |= ring h-1,t (z), for all h ≥ 2 and t ≥ 1. These side conditions can be automatically discharged using the results on the decidability of entailments given in this paper. Additionally, checking the satisfiability of a precondition is used to detect trivially valid Hoare triples.

Related Work

Formal modeling coordinating architectures of component-based systems has received lots of attention, with the development of architecture description languages (ADL), such as BIP [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] or REO [START_REF] Arbab | Reo: A channel-based coordination model for component composition[END_REF]. Many such ADLs have extensions that describe programmed reconfiguration, e.g., [START_REF] El-Ballouli | Programming dynamic reconfigurable systems[END_REF][START_REF] Krause | Modeling dynamic reconfigurations in reo using high-level replacement systems[END_REF], classified according to the underlying formalism used to define their operational semantics: process algebras [START_REF] Cavalcante | Supporting dynamic software architectures: From architectural description to implementation[END_REF][START_REF] Magee | Dynamic structure in software architectures[END_REF], graph rewriting [START_REF] Taentzer | Dynamic change management by distributed graph transformation: Towards configurable distributed systems[END_REF][START_REF] Wermelinger | A graph transformation approach to software architecture reconfiguration[END_REF][START_REF] Metayer | Describing software architecture styles using graph grammars[END_REF], chemical reactions [START_REF] Wermelinger | Towards a chemical model for software architecture reconfiguration[END_REF] (see the surveys [START_REF] Bradbury | A survey of self-management in dynamic software architecture specifications[END_REF][START_REF] Butting | A classification of dynamic reconfiguration in component and connector architecture description[END_REF]). Unfortunately, only few ADLs support formal verification, mainly in the flavour of runtime verification [START_REF] Bucchiarone | Dynamic software architectures verification using dynalloy[END_REF][START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF][START_REF] Lanoix | Combining proof and model-checking to validate reconfigurable architectures[END_REF][START_REF] El-Hokayem | A temporal configuration logic for dynamic reconfigurable systems[END_REF] or finite-state model checking [START_REF] Clarke | A basic logic for reasoning about connector reconfiguration[END_REF].

Parameterized verification of unbounded networks of distributed processes uses mostly hard-coded coordinating architectures (see [START_REF] Bloem | Decidability of Parameterized Verification[END_REF] for a survey). A first attempt at specifying architectures by logic is the interaction logic of Konnov et al. [START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF], a combination of Presburger arithmetic with monadic uninterpreted function symbols, that can describe cliques, stars and rings. More structured architectures (pipelines and trees) can be described using a second-order extension [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]. However, these interaction logics are undecidable and lack support for automated reasoning.

Specifying parameterized component-based systems by inductive definitions is not new. Network grammars [START_REF] Shtadler | Network grammars, communication behaviors and automatic verification[END_REF][START_REF] Metayer | Describing software architecture styles using graph grammars[END_REF][START_REF] Hirsch | Graph grammars and constraint solving for software architecture styles[END_REF] use context-free grammar rules to describe systems with linear (pipeline, token-ring) architectures obtained by composition of an unbounded number of processes. In contrast, we use predicates of unrestricted arities to describe architectural styles that are, in general, more complex than trees. Moreover, we write inductive definitions using a resource logic, suitable also for writing Hoare logic proofs of reconfiguration programs, based on local reasoning [START_REF] Calcagno | Local action and abstract separation logic[END_REF].

Local reasoning about concurrent programs has been traditionally the focus of Concurrent Separation Logic (CSL), based on a parallel composition rule [START_REF] O'hearn | Resources, concurrency, and local reasoning[END_REF], initially with a non-interfering (race-free) semantics [START_REF] Brookes | Concurrent separation logic[END_REF] and later combining ideas of assumeand rely-guarantee [START_REF] Owicki | An Axiomatic Proof Technique for Parallel Programs[END_REF][START_REF] Jones | Developing methods for computer programs including a notion of interference[END_REF] with local reasoning [START_REF] Feng | On the relationship between concurrent separation logic and assume-guarantee reasoning[END_REF][START_REF] Vafeiadis | A marriage of rely/guarantee and separation logic[END_REF] and abstract notions of framing [START_REF] Dinsdale-Young | Concurrent abstract predicates[END_REF][START_REF] Dinsdale-Young | Views: Compositional reasoning for concurrent programs[END_REF][START_REF] Farka | On algebraic abstractions for concurrent separation logics[END_REF]. However, the body of work on CSL deals almost entirely with sharedmemory multithreading programs, instead of distributed systems, which is the aim of our work. In contrast, we develop a resource logic in which the processes do not just share and own resources, but become mutable resources themselves.

The techniques developed in this paper are inspired by existing techniques for similar problems in the context of Separation Logic (SL) [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. For instance, we use an abstract domain similar to the one defined by Brotherston et al. [START_REF] Brotherston | A decision procedure for satisfiability in separation logic with inductive predicates[END_REF] for checking satisfiability of symbolic heaps in SL and reduce a fragment of the entailment problem in our logic to SL entailment [START_REF] Echenim | Unifying decidable entailments in separation logic with inductive definitions[END_REF]. In particular, the use of existing automated reasoning techniques for SL has pointed out several differences between the expressiveness of our logic and that of SL. First, the configuration logic describes hypergraph structures, in which edges are -tuples for ≥ 2, instead of directed graphs as in SL, where is a parameter of the problem: considering to be a constant strictly decreases the complexity of the problem. Second, the degree (number of hyperedges containing a given vertex) is unbounded, unlike in SL, where the degree of heaps is constant. Therefore, we dedicate an entire section ( §5) to the problem of deciding the existence of a bound (and computing a cut-off) on the degree of the models of a formula, used as a prerequisite for the encoding of the entailment problems from the configuration logic as SL entailments.

Definitions

We denote by N the set of positive integers. For a set A, we define A 1 def = A, A i+1 def = A i ×A, for all i ≥ 0, and A + = i≥1 A i , where × denotes the Cartesian product. We denote by pow(A) the powerset of A and by mpow(A) the power-multiset (set of multisets) of A. The cardinality of a finite set A is denoted as ||A||. By writing A ⊆ fin B we mean that A is a finite subset of B. Given integers i and j, we write [i, j] for the set {i, i + 1, . . . , j}, assumed to be empty if i > j. For a tuple t = t 1 , . . . ,t n , we define

|t| def = n, t i def = t i and t [i, j] def = t i , .
. . ,t j . By writing x = poly(y), for given x, y ∈ N, we mean that there exists a polynomial function f : N → N, such that x ≤ f (y).

Configurations

We model distributed systems as hypergraphs, whose vertices are components (i.e., the nodes of the network) and hyperedges are interactions (i.e., describing the way the components communicate with each other). The components are taken from a countably infinite set C, called the universe. We consider that each component executes its own copy of the same behavior, represented as a finite-state machine B = (P , Q , -→), where P is a finite set of ports, Q is a finite set of states and -→⊆ Q × P × Q is a transition relation. Intuitively, each transition q p -→ q of the behavior is triggerred by a visible event, represented by the port p. For instance, the behavior of the components of the token ring system from Fig. 1 We introduce a logic for describing infinite sets of configurations of distributed systems with unboundedly many components and interactions. A configuration is a snapshot of the system, describing the topology of the network (i.e., the set of present components and interactions) together with the local state of each component:

Definition 1. A configuration is a tuple γ = (C , I , ρ)
, where:

-C ⊆ fin C is a finite set of components, that are present in the configuration, -I ⊆ fin (C × P ) + is a finite set of interactions, where each interaction is a sequence (c 1 , p 1 , . . . , c n , p n ) ∈ (C × P ) n that binds together the ports p 1 , . . . , p n of the pairwise distinct components c 1 , . . . , c n , respectively.

ρ : C → Q is a state map associating each (possibly absent) component, a state of the behavior B, such that the set {c ∈ C | ρ(c) = q} is infinite, for each q ∈ Q .

The last condition requires that there is an infinite pool of components in each state q ∈ Q ; since C is infinite and Q is finite, this condition is feasible. For example, the configurations of the token ring from Fig. 1 (a) are ({c 1 , . . . ,

c n }, {(c i , out, c (i mod n)+1 , in) | i ∈ [1, n]}, ρ)
, where ρ : C → {H, T} is a state map. The ring topology is described by the set of components {c 1 , . . . , c n } and interactions {(c i , out, c

(i mod n)+1 , in) | i ∈ [1, n]}.
Intuitively, an interaction (c 1 , p 1 , . . . , c n , p n ) synchronizes transitions labeled by the ports p 1 , . . . , p n from the behaviors (i.e., replicas of the state machine B) of c 1 , . . . , c n , respectively. The interactions are classified according to their sequence of ports, called the interaction type and let Inter def = P + be the set of interaction types; an interaction type models, for instance, the passing of a certain kind of message (e.g., request, acknowledgement, etc.). From an operational point of view, two interactions that differ by a permutation of indices e.g., (c 1 , p 1 , . . . , c n , p n ) and

(c i 1 , p i 1 , . . . , c i n , p i n ) such that {i 1 , . . . , i n } = [1, n],
are equivalent, since the set of transitions is the same; nevertheless, we chose to distinguish them in the following, exclusively for reasons of simplicity.

Note that Def. 1 allows configurations with interactions that involve absent components (i.e., not from the set C of present components in the given configuration). The following definition distinguishes such configurations:

Definition 2. Let γ = (C , I , ρ) be a configuration. An interaction (c 1 , p 1 , . . . , c n , p n ) is loose in γ if and only if c i ∈ C , for some i ∈ [1, n]. If I contains at least one interaction
that is loose in γ, we say that γ is loose. An interaction (resp. configuration) that is not loose is said to be tight.

For instance, every configuration of the system from Fig. 1

γ i = (C i , I i , ρ), for i = 1, 2, such that C 1 ∩ C 2 = / 0 and I 1 ∩ I 2 = / 0, is defined as γ 1 • γ 2 def = (C 1 ∪ C 2 , I 1 ∪ I 2 , ρ). The com- position γ 1 • γ 2 is undefined if C 1 ∩ C 2 = / 0 or I 1 ∩ I 2 = /
0. Note that a tight configuration may be the result of composing two loose configurations, whereas the composition of tight configurations is always tight. The example below shows that, in most cases, a non-trivial decomposition of a tight configuration necessarily involves loose configurations:

Example 1. Let γ i = (C i , I i , ρ) be loose configurations, where C i = {c i }, I i = {(c i , out, c 3-i , in)}, for all i = 1, 2. Then γ def = γ 1 •γ 2 is the tight configuration γ = ({c 1 , c 2 }, {(c 1 , out, c 2 , in), (c 2 , out, c 1 , in)}, ρ).
The only way of decomposing γ into two tight subconfigurations γ 1 and γ 2 is taking

γ 1 def = γ and γ 2 def = ( / 0, / 0
, ρ), or viceversa. In analogy with graphs, the degree of a configuration is the maximum number of interactions from the configuration that involve a (possibly absent) component:

Definition 4. The degree of a configuration γ = (C , I , ρ) is defined as δ(γ) def = max c∈C δ c (γ), where δ c (γ) def = ||{(c 1 , p 1 , . . . , c n , p n ) ∈ I | c = c i , i ∈ [1, n]}||.
For instance, the configuration of the system from Fig. 1 (a) has degree two.

Configuration Logic

Let V and A be countably infinite sets of variables and predicates, respectively. For each predicate A ∈ A, we denote its arity by #A. The formulae of the Configuration Logic (CL) are described inductively by the following syntax:

φ := emp | [x] | x 1 .p 1 , . . . , x n .p n | x@q | x = y | x = y | A(x 1 , . . . , x #A ) | φ * φ | ∃x . φ
where x, y, x 1 , . . . ∈ V, q ∈ Q and A ∈ A. A formula [x], x 1 .p 1 , . . . , x n .p n , x@q and A(x 1 , . . . , x #A ) is called a component, interaction, state and predicate atom, respectively. Sometimes, we use the shorthand [x]@q def = [x] * x@q. Intuitively, the formula [x]@q * [y]@q * x.out, y.in * x.in, y.out describes a configuration consisting of two distinct components, denoted by the values of x and y, in states q and q , respectively, and two interactions binding the out port of one to the in port of the other component. For instance, γ = γ 1 • γ 2 from Example 1 is such a configuration.

A formula is said to be pure if and only if it consists of state atoms, equalities and disequalities. A formula with no occurrences of predicate atoms (resp. existential quantifiers) is called predicate-free (resp. quantifier-free). A variable is free if it does not occur within the scope of an existential quantifier and let fv(φ) be the set of free variables of φ. A sentence is a formula with no free variables. A substitution φ[x 1 /y 1 . . . x n /y n ] replaces simultaneously every free occurrence of x i by y i in φ, for all i ∈ [1, n]. Before defining the semantics of CL formulae, we introduce the set of inductive definitions that assigns meaning to predicates: Definition 5. A set of inductive definitions (SID) ∆ consists of rules A(x 1 , . . . , x #A ) ← φ, where x 1 , . . . , x #A are pairwise distinct variables, called parameters, such that fv(φ) ⊆ {x 1 , . . . , x #A }. The rule A(x 1 , . . . , x #A ) ← φ defines A and we denote by def ∆ (A) the set of rules from ∆ that define A.

Note that having distinct parameters in a rule is without loss of generality, as e.g., a rule A(x 1 , x 1 ) ← φ can be equivalently written as A(x 1 , x 2 ) ← x 1 = x 2 * φ. As a convention, we shall always use the names x 1 , . . . , x #A for the parameters of a rule that defines A.

The semantics of CL formulae is defined by a satisfaction relation γ |= ν ∆ φ between configurations and formulae. This relation is parameterized by a store ν : V → C mapping the free variables of a formula into components from the universe (possibly absent from γ) and an SID ∆. We write ν[x ← c] for the store that maps x into c and agrees with ν on all variables other than x. The definition of the satisfaction relation is by induction on the structure of formulae, where γ = (C , I , ρ) is a configuration (Def. 1):

γ |= ν ∆ emp ⇐⇒ C = / 0 and I = / 0 γ |= ν ∆ [x] ⇐⇒ C = {ν(x)} and I = / 0 γ |= ν ∆ x 1 .p 1 , . . . , x n .p n ⇐⇒ C = / 0 and I = {(ν(x 1 ), p 1 , . . . , ν(x n ), p n )} γ |= ν ∆ x@q ⇐⇒ γ |= ν ∆ emp and ρ(ν(x)) = q γ |= ν ∆ x ∼ y ⇐⇒ γ |= ν ∆ emp and ν(x) ∼ ν(y), for all ∼∈ {=, =} γ |= ν ∆ A(y 1 , . . . , y #A ) ⇐⇒ γ |= ν ∆ φ[x 1 /y 1 , . . . , x #A /y #A ], for some rule A(x 1 , . . . , x #A ) ← φ from ∆ γ |= ν ∆ φ 1 * φ 2 ⇐⇒ exist γ 1 , γ 2 , such that γ = γ 1 • γ 2 and γ i |= ν ∆ φ i , for i = 1, 2 γ |= ν ∆ ∃x . φ ⇐⇒ γ |= ν[x←c] ∆ φ, for some c ∈ C
If φ is a sentence, the satisfaction relation γ |= ν ∆ φ does not depend on the store, written γ |= ∆ φ, in which case we say that γ is a model of φ. If φ is a predicate-free formula, the satisfaction relation does not depend on the SID, written γ |= ν φ. A formula φ is satisfiable if and only if the sentence ∃x 1 . . . ∃x n . φ has a model, where fv(φ) = {x 1 , . . . , x n }. A formula φ entails a formula ψ, written φ |= ∆ ψ if and only if, for any configuration γ and store ν, we have γ |= ν ∆ φ only if γ |= ν ∆ ψ.

Separation Logic

Separation Logic (SL) [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] will be used in the following to prove several technical results concerning the decidability and complexity of certain decision problems for CL.

For self-containment reasons, we define SL below. The syntax of SL formulae is described by the following grammar:

φ := emp | x 0 → (x 1 , . . . , x K ) | x = y | x = y | A(x 1 , . . . , x #A ) | φ * φ | ∃x . φ
where x, y, x 0 , x 1 , . . . ∈ V, A ∈ A and K ≥ 1 is an integer constant. Formulae of SL are interpreted over finite partial functions h : C fin C K , called heaps2 , by a satisfaction relation h ν φ, defined inductively as follows:

h ν ∆ emp ⇐⇒ h = / 0 h ν ∆ x 0 → (x 1 , . . . , x K ) ⇐⇒ dom(h) = {ν(x 0 )} and h(ν(x 0 )) = ν(x 1 ), . . . , ν(x K ) h ν φ 1 * φ 2 ⇐⇒ there exist h 1 , h 2 such that dom(h 1 ) ∩ dom(h 2 ) = / 0, h = h 1 ∪ h 2 and h i ν ∆ φ i , for both i = 1, 2
where dom(h) def = {c ∈ C | h(c) is defined} is the domain of the heap and (dis-)equalities, predicate atoms and existential quantifiers are defined same as for CL.

Decision Problems

We define the decision problems that are the focus of the upcoming sections. As usual, a decision problem is a class of yes/no queries that differ only in their input. In our case, the input consists of an SID and one or two predicates, written between square brackets. Definition 6. We consider the following problems, for a SID ∆ and predicates A, B ∈ A:

1. Sat[∆, A]: is the sentence ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ) satisfiable for ∆? 2. Tight[∆, A]: is every model γ of the sentence ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ) a tight configuration? 3. Bnd[∆, A]: is the set {δ(γ) | γ |= ∆ ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A )} finite? 4. Entl[∆, A, B]: does A(x 1 , . . . , x #A ) |= ∆ ∃x #B+1 . . . ∃x #A . B(x 1 , . . . , x #B ) hold?
We define the size of a formula φ as the total number of occurrences of symbols needed to write it down, denoted by size(φ). The size of a SID ∆ is size(∆) def = ∑ A(x 1 ,...,x #A )←φ∈∆ size(φ)+ #A + 1. Other parameters of a SID ∆ are its:

maximal arity, denoted as arity(∆)

def = max{#A | A(x 1 , . . . , x #A ) ← φ ∈ ∆}, -width, denoted as width(∆) def = max{size(φ) | A(x 1 , . . . , x #A ) ← φ ∈ ∆}, -maximal interaction size, denoted as intersize(∆) def = max{n | x 1 .p 1 , . . . , x n .p n occurs in φ, A(x 1 , . . . , x #A ) ← φ ∈ ∆}.
For each decision problem P[∆, A, B], we consider its (k, )-bounded versions P (k, ) [∆, A, B], obtained by restricting the predicates and interaction atoms occurring ∆ to arity(∆) ≤ k and intersize(∆) ≤ , respectively, where k and are either positive integers or infinity. We consider, for each P[∆, A, B], the subproblems P (k, ) [∆, A, B] corresponding to the three cases (1) k < ∞ and = ∞, (2) k = ∞ and < ∞, and (3) k = ∞ and = ∞. As we explain next, this is because, for the decision problems considered (Def. 6), the complexity for the case k < ∞, < ∞ matches the one for the case k < ∞, = ∞.

Moreover, for each problem P[∆, A] (resp. P[∆, A, B]), we consider its general version P[∆, φ] (resp. P[∆, φ, ψ]), where φ and ψ are CL formulae, whose predicates are interpreted by the rules in ∆. The generalized problems P[∆, φ] involving one predicate atom (points 1 and 3 of Def. 6) can be reduced to their restricted versions P[∆, A], by introducing a fresh predicate A φ (not occurring in ∆), of arity n ≥ 0 and a rule A φ (x 1 , . . . , x n ) ← φ, where fv(φ) = {x 1 , . . . , x n }. This reduction is linear in the size of the input and changes none of the following complexity results. Concerning the generalized entailment problem Entl[∆, φ, ψ], the reduction to the problem Entl[∆, A, B] (Def. 6 4) might affect its decidability status, which is subject to syntactic restrictions on the rules in ∆ (details will be given in §6).

Satisfiability [START_REF] Ahrens | Local reasoning about parameterized reconfigurable distributed systems[END_REF] and entailment (4) arise naturally during verification of reconfiguration programs. For instance, Sat[∆, φ] asks whether a specification φ of a set configurations (e.g., a pre-, post-condition, or a loop invariant) is empty or not (e.g., an empty precondition typically denotes a vacuous verification condition), whereas Entl[∆, φ, ψ] is used as a side condition for the Hoare rule of consequence, as in e.g., the proof from Fig. 1 (c). Moreover, entailments must be proved when checking inductiveness of a user-provided loop invariant.

In contrast, the applications of the tightness (2) and boundedness (3) problems are less obvious and require a few explanations. The Tight[∆, φ] problem is relevant in the context of compositional verification of distributed systems. Suppose we have a distributed system consisting of two interacting subsystems, whose sets of initial configurations are described by φ 1 and φ 2 , respectively i.e., the initial configurations of the system are described by φ 1 * φ 2 . The compositional verification of a reconfiguration program P reduces checking the validity of a Hoare triple {φ 1 * φ 2 } P {ψ 1 * ψ 2 } to checking the validity of the simpler {φ i } P {ψ i }, for i = 1, 2. Unfortunately, this appealing method faces the problem of interference between the subsystems described by φ 1 and φ 2 , namely the loose interactions of φ i might connect to present components of φ 3-i and change their states during the execution. In this case, it is sufficient to infer the sets of cross-boundary interactions F i,3-i , describing those interactions from φ i that connect to components from φ 3-i , and check the validity of the triples {φ i * F 3-i,i } P {ψ i * F 3-i,i }, under a relaxed semantics which considers that the interactions in F 3-i,i can fire anytime, or according to the order described by some regular language. However, if Tight[∆, φ 1 ] (resp. Tight[∆, φ 2 ]) has a negative answer, the set of cross-boundary interactions may be unbounded, hence not representable by a finite sep-arating conjunction of interaction atoms F 1,2 (resp. F 2,1 ). Thus, the tightness problem is important in establishing necessary conditions under which a compositional proof rule can be applied to checking correctness of reconfigurations in a distributed system.

The Bnd[∆, φ] problem is used to check a necessary condition for the decidability of entailments i.e., Entl[∆, φ, ψ]. If Bnd[∆, φ] has a positive answer, we can reduce the problem Entl[∆, φ, ψ] to an entailment problem for SL, which is always interpreted over heaps of bounded degree [START_REF] Echenim | Unifying decidable entailments in separation logic with inductive definitions[END_REF]. Otherwise, the decidability status of the entailment problem is open, for configurations of unbounded degree, such as the one described by the example below.

Example 2. The following SID describes star topologies with a central controller connected to an unbounded number of workers stations:

Star(x) ← [x] * Worker(x), Worker(x) ← emp | ∃y . x.out, y.in * [y] * Worker(x)

Satisfiability

We show that the satisfiability problem (Def. 6, point 1) is decidable, using a method similar to the one pioneered by Brotherston et al. [START_REF] Brotherston | A decision procedure for satisfiability in separation logic with inductive predicates[END_REF], for checking satisfiability of inductively defined symbolic heaps in SL. We recall that a formula π is pure if and only if it is a separating conjunction of equalities, disequalities and state atoms. Definition 7. The closure cl(π) of a pure formula π is the limit of the sequence π 0 , π 1 , π 2 , . . . such that π 0 = π and, for each i ≥ 0, π i+1 is obtained by joining (with * ) all of the following formulae to π i :

x = z, where x and z are the same variable, or x = y and y = z both occur in π i , x = z, where x = y and y = z both occur in π i , or y@q, where x@q and x = y both occur in π i .

Because only finitely many such formulae can be added, the sequence of pure formulae from Def. 7 is bound to stabilize after polynomially many steps. A pure formula is satisfiable if and only if its closure does not contain contradictory literals i.e., x = y and x = y, or x@q and x@q , for q = q ∈ Q . We write x ≈ π y (resp. x ≈ π y) if and only if

x = y (resp. x = y) occurs in cl(π) and not(x ≈ π y) (resp. not(x ≈ π y)) whenever x ≈ π y (resp. x ≈ π y) does not hold. Note that e.g., not(x ≈ π y) is not the same as x ≈ π y.

Lemma 1. A pure formula π is satisfiable if and only if the following hold:

1. for all x, y ∈ fv(π), x = y and x = y do not occur both in cl(π),

2. for all x ∈ fv(π) and q = r ∈ Q , x@q and x@r do not occur both in cl(π).

Proof. A pure formula π is satisfiable if and only if there exists a store ν and a configuration ( / 0, / 0, ρ), such that ( / 0, / 0, ρ) |= ν π. "⇐" It is easy to see that ≈ π is an equivalence relation, for each pure formula π. Given any state map ρ, we define ν by assigning each equivalence class of ≈ π a distinct component c, such that ρ(c) = q if y@q occurs in π, for a variable y in the class. By the conditions of the Lemma, ρ and ν are well defined and we have ( / 0, / 0, ρ) |= ν π, by definition. "⇒" If ( / 0, / 0, ρ) |= ν π then ( / 0, / 0, ρ) |= ν cl(π), because each additional formula in cl(π) is a logical consequence of π. Since cl(π) is satisfiable, the two conditions of the Lemma must hold.

Base tuples constitute the abstract domain used by the algorithms for checking satisfiability (point 1 of Def. 6) and boundedness (point 3 of Def. 6), defined as follows: Definition 8. A base tuple is a triple t = (C , I , π), where:

-C ∈ mpow(V) is a multiset of variables denoting present components, -I : Inter → mpow(V + ) maps each interaction type τ ∈ Inter into a multiset of tuples of variables of length |τ| each, and π is a pure formula. A base tuple is called satisfiable if and only if π is satisfiable and the following hold:

1. for all x, y ∈ C , not(x ≈ π y), 2. for all τ ∈ Inter, x 1 , . . . , x |τ| , y 1 , . . . , y |τ| ∈ I (τ), there exists i ∈ [1, |τ|] such that not(x i ≈ π y i ), 3. for all τ ∈ Inter, x 1 , . . . , x #τ ∈ I (τ) and 1 ≤ i < j ≤ |τ|, we have not(x i ≈ π x j ).
We denote by SatBase the set of satisfiable base tuples.

Note that a base tuple (C , I , π) is unsatisfiable if C (I ) contains the same variable (tuple of variables) twice (for the same interaction type), hence the use of multisets in the definition of base tuples. It is easy to see that checking the satisfiability of a given base tuple (C , I , π) can be done in time poly(||C || + ∑ τ∈Inter ||I (τ)|| + size(π)).

We define a partial composition operation on satisfiable base tuples, as follows:

(C 1 , I 1 , π 1 ) ⊗ (C 2 , I 2 , π 2 ) def = (C 1 ∪ C 2 , I 1 ∪ I 2 , π 1 * π 2 )
where the union of multisets is lifted to functions Inter → mpow(V + ) in the usual way.

The composition operation

⊗ is undefined if (C 1 , I 1 , π 1 ) ⊗ (C 2 , I 2 , π 2 ) is not satisfiable e.g., if C 1 ∩ C 2 = / 0, I 1 (τ) ∩ I 2 (τ) = /
0, for some τ ∈ Inter, or π 1 * π 2 is not satisfiable. Given a pure formula π and a set of variables X, the projection π↓ X removes from π all atomic propositions α, such that fv(α) ⊆ X. The projection of a base tuple (C , I , π) on a variable set X is formally defined below:

(C , I , π)↓ X def = C ∩ X, λτ . { x 1 , . . . , x |τ| ∈ I (τ) | x 1 , . . . , x |τ| ∈ X}, cl(dist(I ) * π)↓ X where dist(I ) def = * τ∈Inter * x 1 ,...,x |τ| ∈I (τ) * 1≤i< j≤|τ| x i = x j
The substitution operation (C , I , π)[x 1 /y 1 , . . . , x n /y n ] replaces simultaneously each x i with y i in C , I and π, respectively. For a store ν, we denote by ν[x 1 /y 1 , . . . , x n /y n ] the store such that ν[x 1 /y 1 , . . . , x n /y n ](x i ) = ν(y i ) and agrees with ν over V\{x 1 , . . . , x n }.We lift the composition, projection and substitution operations to sets of satisfiable base tuples, as usual.

Lemma 2. Given a formula φ and a substitution σ = [x 1 /y 1 , . . . , x n /y n ], for any configuration (C , I , ρ) and store ν,

(C , I , ρ) |= ν ∆ φσ only if (C , I , ρ) |= νσ φ.
Proof. By induction on the definition of |= ν ∆ . Next, we define the base tuple corresponding to a quantifier-and predicate-free formula φ = ψ * π, where ψ consists of component and interaction atoms and π is pure. Since, moreover, we are interested in those components and interactions that are visible

input: a SID ∆ output: µ - → X .∆ 1: initially µ - → X .∆ := λA . / 0 2: for A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ ∈ ∆, with φ quantifier-and predicate-free do 3: µ - → X .∆ (A) := µ - → X .∆ (A) ∪ Base(φ, {x 1 , . . . , x #A })↓ x 1 ,...,x #A 4: while µ - → X .∆ still change do 5: for r : A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * * h =1 B (z 1 , . . . , z #B ) ∈ ∆ do 6: if there exist t 1 ∈ µ - → X .∆ (B 1 ), . . . , t h ∈ µ - → X .∆ (B h ) then 7: µ - → X .∆ (A) := µ - → X .∆ (A) ∪ Base(φ, {x 1 , . . . , x #A }) ⊗ h =1 t [x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A
Fig. 2: Algorithm for the Computation of the Least Solution through a given indexed set of parameters X = {x 1 , . . . , x n }, for a variable y, we denote by {{y}} X π the parameter x i with the least index, such that y ≈ π x i , or y itself, if no such parameter exists. We define the following sets of formulae:

Base(φ, X) def = {(C , I , π)} , if (C , I , π) is satisfiable / 0 , otherwise where C def = {{{x}} X π | [x] occurs in ψ} I def = λ p 1 , . . . , p s . {{y 1 }} X π , . . . , {{y s }} X π | y 1 .p 1 , . . . , y s .p s occurs in ψ
We consider a tuple of variables -→ X , having a variable X (A) ranging over pow(SatBase), for each predicate A that occurs in ∆. With these definitions, each rule of ∆:

A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * B 1 (z 1 1 , . . . , z 1 #B 1 ) * . . . * B h (z h 1 , . . . , z h #B h )
where φ is a quantifier-and predicate-free formula, induces the constraint:

X (A) ⊇ Base(φ, {x 1 , . . . , x #A }) ⊗ h =1 X (B )[x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A (1)
Let ∆ be the set of such constraints, corresponding to the rules in ∆ and let µ -→ X .∆ be the tuple of least solutions of the constraint system generated from ∆, indexed by the tuple of predicates that occur in ∆, such that µ -→ X .∆ (A) denotes the entry of µ -→

X .∆

correponding to A. Since the composition and projection are monotonic operations, such a least solution exists and is unique. Moreover, since SatBase is finite, the least solution can be attained in a finite number of steps, using a standard Kleene iteration(see Fig. 2).

Given a base tuple (C , I , π) and a store ν, we define the following sets of components and interactions, respectively:

ν(C ) def = {ν(x) | x ∈ C } ν(I ) def = p 1 ,...,p n ∈Inter {(ν(x 1 ), p 1 , . . . , ν(x n ), p n ) | (x 1 , . . . , x n ) ∈ I ( p 1 , . . . , p n )}
We state below the main result leading to an elementary recursive algorithm for the satisfiability problem (Thm. 1).

Lemma 3. Given a base tuple (C , I , π) ∈ µ - → X .∆ (A)[x 1 /y 1 , . . . , x #A /y #A ], a state map
ρ and a store ν such that ( / 0, / 0, ρ) |= ν π, a set of components D disjoint from ν(C ) and a set of interactions J disjoint from ν(I ), there exists a configuration (C ,

I , ρ), such that (C , I , ρ) |= ν ∆ A(y 1 , . . . , y #A ), C ∩ D = / 0 and I ∩ J = / 0. Proof. Let σ def = [x 1 /y 1 , . . . , x #A /y #A ] be a substitution and (C 0 , I 0 , π 0 ) ∈ µ - → X .∆ (A) be a base pair, such that (C , I , π) = (C 0 , I 0 , π 0 )σ. Since ( / 0, / 0, ρ) |= ν π, we obtain ( / 0, / 0, ρ) |= ν 0 π 0 , by Lemma 2, where we define ν 0 def = νσ. Let K def = D ∪ {c i | (c 1 , p 1 , . . . , c n , p n ) ∈ J , i ∈ [1, n]}
The proof is by fixpoint induction on the definition of (C 0 , I 0 , π 0 ). Assume that:

(C 0 , I 0 , π 0 ) ∈ Base(ψ * π , {x 1 , . . . , x #A }) ⊗ h =2 µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A for a rule A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . ψ * π * * h =2 B (z 1 , . . . , z #B ) of ∆, such that ψ * π is quantifier-free,
ψ consists of component and interaction atoms and π is the largest pure subformula of ψ * π . Then there exist base tuples (C 1 , I 1 , π 1 ), . . . , (C h , I h , π h ), such that:

-(C 1 , I 1 , π 1 ) ∈ Base(ψ * π , {x 1 , . . . , x #A }), -(C , I , π ) ∈ µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ], for all ∈ [2, h], -(C 0 , I 0 , π 0 ) = (C 1 , I 1 , π 1 ) ⊗ . . . ⊗ (C h , I h , π h ) ↓ x 1 ,...,x #A .
From the first and last points, we deduce

π 0 = cl(π * * h =2 (dist(I ) * π ))↓ x 1 ,...,x #A . Let π def = π * * h =2 (dist(I ) * π
) and define a store ν 0 , by assigning each ≈ π -equivalence class the following component:

-ν 0 (x i ), if x i belongs to the class, for some i ∈ [1, #A],
else, if the class is disjoint from {x 1 , . . . , x #A } and y@q occurs in π , for a variable y in the class, we assign c ∈ C \ K , such that ρ(c) = q; since π is satisfiable, there are no two state atoms y@q and z@r, such that y ≈ π z and q = r in π and, moreover, chosing c is always possible, by the last point of Def. 1, otherwise, the class is assigned an arbitrary component c ∈ C \ K .

Such a store exists, because π is satisfiable and, moreover, ( / 0, / 0, ρ)

|= ν 0 π , hence also ( / 0, / 0, ρ) |= ν 0 π , for all ∈ [2, h].
We define two sequences of sets of components C 1 , . . . , C h and interactions I 1 , . . . , I h , as follows:

-C 1 def = {ν 0 (y) | [y] occurs in ψ}, -I 1 def = {(ν 0 (z 1 ), p 1 , . . . , ν 0 (z t ), p t ) | z 1 .p 1 , . . . , z t .p t occurs in ψ},
for all ∈ [2, h], assume that C 1 , . . . , C -1 and I 1 , . . . , I -1 have been defined and let us define:

D def = D ∪ -1 j=1 C j ∪ h j= +1 ν 0 (C j ) J def = J ∪ -1 j=1 I j ∪ h j= +1 ν 0 (I j )
First, we prove that D ∩ ν 0 (C ) = / 0 and J ∩ ν 0 (I ) = / 0 (we prove the first point, the second using a similar argument). Suppose, for a contradiction, that c ∈ D ∩ ν 0 (C ). We distinguish the following cases:

• if c ∈ D ∩ ν 0 (C ), then c ∈ D ∩ ν 0 (C 0 ), because C ⊆ C 0 , contradiction with D ∩ ν 0 (C 0 ) = D ∩ ν(C ) = / 0. • else, if c ∈ C j ∩ ν 0 (C ), for some j ∈ [1, -1], then c ∈ C j ∩ D j , because ν 0 (C ) ⊆ D j , contradiction with the inductive hypothesis C j ∩ D j = / 0.
• otherwise, c ∈ ν 0 (C j ) ∩ ν 0 (C ), hence there exist variables y j ∈ C j and y ∈ C , such that y j ≈ π y , contradiction with the fact that (C j , I j , π j ) ⊗ (C , I , π ) is satisfiable.

Second, we apply the inductive hypothesis to obtain configurations

(C , I , ρ), such that (C , I , ρ) |= ν 0 ∆ B (t 1 , . . . ,t #B ), C ∩ D = / 0 and I ∩ J = / 0, for all ∈ [2, h].
By the definitions of D and J , the sets C and I are pairwise disjoint, respectively, hence the composition (C , I , ρ)

def = • h =1 (C , I , ρ) is defined. Moreover, (C , I , ρ) |= ν 0 ∆ ψ * π * * h =2 B (t 1 , . . . ,t #B ), hence (C , I , ρ) |= ν 0 ∆ A(x 1 , . . . , x #A ), leading to (C , I , ρ) |= ν A(y 1 , . . . , y #A ).
Finally, we are left with proving that C ∩ D = / 0 and I ∩ J = / 0 (we prove the first point only, the second uses a similar reasoning). Since C = h =1 C , this is equivalent to proving the following:

• C 1 ∩ D = / 0: suppose,
I , π) ∈ µ - → X .∆ (A)[x 1 /y 1 , . . . , x #A /y #A ], such that ν(C ) ⊆ C , ν(I ) ⊆ I and ( / 0, / 0, ρ) |= ν π.
Proof. By fixpoint induction on the definition of the satisfaction relation

|= ν ∆ . Since (C , I , ρ) |= ν ∆ A(y 1 , . . . , y #A ), by Lemma 2, we have (C , I , ρ) |= ν 0 ∆ A(x 1 , . . . , x #A ), where ν 0 def = ν[x 1 /y 1 , . . . , x #A /y #A ]. Hence, ∆ has a rule A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . ψ * π * * h =2 B (z 1 , . . . , z #B )
, such that ψ * π is quantifier-free, ψ consists of component and interaction atoms and π is pure and there exists a store ν 0 , that agrees with ν 0 over x 1 , . . . , x #A and configurations (C 1 , I 1 , ρ), . . . , (C , I , ρ), such that:

-(C 1 , I 1 , ρ) |= ν 0 ψ * π , -(C , I , ρ) |= ν 0 ∆ B (z 1 , . . . , z #B ), for all ∈ [2, h],
and

-(C , I , ρ) = (C 1 , I 1 , ρ) • . . . • (C h , I h , ρ).
We consider the following base tuples:

-(C 1 , I 1 , π 1 ) def = Base(ψ * π , {x 1 , . . . , x #A }), -(C , I , π ) ∈ µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ], such that ν 0 (C ) ⊆ C , ν 0 (I ) ⊆ I
and ( / 0, / 0, ρ) |= ν 0 π , whose existence is guaranteed by the inductive hypothesis, for all ∈ [2, h].

By the definition of Base(ψ * π , {x 1 , . . . , x #A }) and the fact that (C 1 , I 1 , ρ) |= ν 0 ψ * π , we obtain ν 0 (C 1 ) = C 1 and ν 0 (I 1 ) = I 1 . Since the composition • h =1 (C , I , ρ) is defined, the sets C 1 , . . . , C h and I 1 , . . . , I h are pairwise disjoint, respectively. Since ν 0 (C ) ⊆ C and ν 0 (I ) ⊆ I , for all ∈ [1, h], we deduce that h =1 (C , I , π ) is satisfiable, because: for all 1 ≤ i < j ≤ h, for any two variables y ∈ C i and z ∈ C j we have not(y

≈ π z), because ν 0 (C i ) ∩ ν 0 (C j ) = / 0,
for all 1 ≤ i < j ≤ h, all τ ∈ Inter, for any two tuples y 1 , . . . , y |τ| ∈ I i (τ) and z 1 , . . . , z |τ| ∈ I j (τ), we have not(

y k ≈ π z k ), for at least some k ∈ [1, |τ|], because ν 0 (I i ) ∩ ν 0 (I j ) = / 0,
for each tuple y 1 , . . . , y |τ| ∈ I ( p 1 , . . . , p n ), for ∈ [1, h], we have not(y i ≈ π y j ), for all 1 ≤ i < j ≤ n, because (ν 0 (y 1 ), p 1 , . . . , ν 0 (y n ), p n ) ∈ I , hence ν 0 (y 1 ), . . . , ν 0 (y n )

are pairwise distinct, -( / 0, / 0, ρ) |= ν 0 π * * h =2 π , hence ( / 0, / 0, ρ) |= ν 0 π * * h =2 dist(I ) * π , by the previ- ous point. Then we define (C 0 , I 0 , π 0 ) def = h =1 (C , I , π ) ↓ x 1 ,...,x #A and (C , I , π) def = (C 0 , I 0 , π 0 )[x 1 /y 1 , . . . , x #A /y #A ].
By the definition of ∆ , we have:

µ - → X .∆ (A) ⊇ Base(ψ * π , {x 1 , . . . , x #A }) ⊗ h =2 µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A
and, since, by the construction of (C 0 , I 0 , π 0 ),

(C 0 , I 0 , π 0 ) ∈ Base(ψ * π , {x 1 , . . . , x #A }) ⊗ h =2 µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A we obtain (C 0 , I 0 , π 0 ) ∈ µ - → X .∆ (A), leading to (C , I , π) ∈ µ - → X .∆ (A)[x 1 /y 1 , . . . , x #A /y #A ]. Next, we check that ν(C ) ⊆ h =1 ν 0 (C ) ⊆ h =1 C = C and ν(I ) ⊆ h =1 ν 0 (I ) ⊆ h =1 I = I .
Finally, the requirement ( / 0, / 0, ρ) |= ν π follows from the following:

-π = π 0 [x 1 /y 1 , . . . , x #A /y #A ]
, by the definition of (C , I , π), Proof. "⇐" follows from Lemma 3 and "⇒" follows from Lemma 4.

-( / 0, / 0, ρ) |= ν 0 π and ( / 0, / 0, ρ) |= ν 0 π , for all ∈ [2, h], -π 0 = cl(π * * h =2 dist(I ) * π )↓ x 1 ,...,x #A ,
If the maximal arity of the predicates occurring in ∆ is bound by a constant k, no satisfiable base tuple (C , I , π) can have a tuple y 1 , . . . , y |τ| ∈ I (τ), for some τ ∈ Inter, such that |τ| > k, since all variables y 1 , . . . , y |τ| are parameters denoting distinct components (point 3 of Def. 8). Hence, the upper bound on the size of a satisfiable base tuple is constant, in both the k < ∞, < ∞ and k < ∞, = ∞ cases, which are, moreover indistinguishable complexity-wise (i.e., both are NP-complete). In contrast, in the cases k = ∞, < ∞ and k = ∞, = ∞, the upper bound on the size of satisfiable base tuples is polynomial and simply exponential in size(∆), incurring a complexity gap of one and two exponentials, respectively. The theorem below states the main result of this section:

Theorem 1. Sat (k,∞) [∆, A] is NP-complete for k ≥ 4, Sat (∞, ) [∆, A] is EXP-complete and Sat[∆, A] is in 2EXP.
Proof. Membership (upper bounds). p j • S α, j ) + (2α 2 + α), that is, size of the set of components C plus the size of the set of interactions I plus the length of the longest pure formula π. In general, for any non-negative integer j there exists at most p j interaction types of arity j with ports from P ; moreover, for any such interaction type there exists at most S α, j interactions relating distinct components from an α-element set. Moreover, no such interaction exists neither if j > α nor j > β.

For any u ≤ α it holds that ∑ u j=1 p j • S α, j ≤ p u α u (an easy check by induction on u). We use the inequality above with u = min(α, β) and obtain that B ≤ 2α + 2α 2 + p min(α,β) α min(α,β) def = B * . We distinguish the three cases: Let N def = 2 B * , that is, (an over-approximation of) the total number of base tuples. Clearly, N is constant in case (1) and respectively 2 poly(size(∆)) and 2 2 poly(size(∆)) in cases (2), (3). Let L be the number of predicates occuring in ∆ and H be the maximum number of predicates used in a term in ∆. Let observe that both L and H are in general O(size(∆)).

Then the least solution µ -→

X .∆ has at most N base tuples for each predicate, hence at most L • N base tuples. Furthermore, for each rule of ∆ the time to check and/or produce the base tuple (C 0 , I 0 , π 0 ) with respect to the rule constraint (1) and given arguments (C j , I j , π j ) j=1,h is polynomial poly(B * , size(∆))). That is, both composition and projection take at most (H + 1)B * + size(∆) 3 time as they need to process (union or scan) at most H + 1 base tuples of length B * each plus the closure of pure formula with at most size(∆) variables. 1. k < ∞, = ∞: We define a non-determinstic algorithm as follows. Let (∆, A) be the input instance. We guess a witness W 1 , . . . ,W K for a least solution, where 1 ≤ K ≤ L • N and each W i entry is of the form (T i , r i , e i,1 , . . . , e i,h i ), where T i is a base tuple, r i an index of a rule of ∆ and e i,1 , .

I , π) ∈ µ - → X .∆ (A).
For this, we need to check: (a) every entry is well-formed, that is, the rule indexed by r i instantiates precisely h i predicates; moreover, for every 1 ≤ j ≤ h i the index e i, j designates an entry W e i, j whose rule defines the j-th predicate instantiated by the rule r i ; (b) the base tuple of every entry is satisfiable and correctly computed, that is, T i is the result of applying the constraint (1) for rule r i with actual arguments T e i,1 , . . . , T e i,h i from the referred entries; (c) the rule r 1 of the first entry W 1 defines the predicate A. Again, as B * and N are constant in this case, all these checks are done in polynomial time. Since both the generation and the checking of the witness are polynomial time, this ensures membership in NP. 2. k = ∞, < ∞: Consider the computation of the least solution µ -→ X .∆ using standard Kleene iteration. At every step, a rule of ∆ and a tuple of at most H base tuples arguments are selected to produce a new base tuple. Thus, in the worst case, at most size(∆) rules in combination with at most N H base tuples need to be selected and evaluated. If no new base tuple is generated the fixpoint is reached and the algorithms stops. Since there are at most L • N base tuples in the least solution, the total time will be therefore

L • N • size(∆) • N H • t(B * , size(∆)) where t(B * , size(∆))
is the (polynomial) time to process one selection. It is an easy check that the above is 2 poly(size(∆)) since N = 2 poly(size(∆)) in this case. 3. k = ∞, = ∞: Following the same reasoning as in the previous case the complexity is 2 2 poly(size(∆)) as N = 2 2 poly(size(∆)) in this case.

Hardness (lower bounds). The restricted fragment of CL to * , =, = is equisatisfiable to the restricted fragment of SL restricted to * , =, =. The satisfiability of the above SL fragment has been proven respectively NP-hard, if the arities of predicates are bounded by a constant k ≥ 3 [9, Theorem 4.9] and EXP-hard, in general [START_REF] Brotherston | A decision procedure for satisfiability in separation logic with inductive predicates[END_REF]Theorem 4.15]. Yet, the reductions considered in these proofs rely on the use of a predefined nil constant symbol in the SL logic; this constant can be nevertheless replaced by a variable consistently propagated along the SID, that is, at the price of increasing the arities of all predicates by one. Therefore, it follows immediately that Sat (k,∞) [∆, φ] is NP-hard for k ≥ 4 and Sat (∞, ) [∆, φ], Sat[∆, φ] are both EXP-hard.

Example 3. The doubly-exponential upper bound for the algorithm computing the least solution of a system of constraints of the form (1) is necessary, in general, as illustrated by the following worst-case example. Let n be a fixed parameter and consider the n-arity predicates A 1 , . . . , A n defined by the following SID:

A i (x 1 , . . . , x n ) → * n-i j=0 A i+1 (x 1 , . . . , x i-1 , [x i , . . . , x n ] j ) , for all i ∈ [1, n -1] A n (x 1 , . . . , x n ) → x 1 .p, . . . , x n .p A n (x 1 , . . . , x n ) → emp
where, for a list of variables x i , . . . , x n and an integer j ≥ 0, we write [x i , . . . , x n ] j for the list rotated to the left j times (e.g., [x 1 , x 2 , x 3 , x 4 , x 5 ] 2 = x 3 , x 4 , x 5 , x 1 , x 2 ). In this example, when starting with A 1 (x 1 , . . . , x n ) one eventually obtains predicate atoms A n (x i 1 , . . . , x i n ), for any permutation x i 1 , . . . , x i n of x 1 , . . . , x n . Since A n may choose to create or not an interaction with that permutation of variables, the total number of base tuples generated for A 1 is 2 n! . That is, the fixpoint iteration generates 2 2 O(nlogn) base tuples, whereas the size of the input of Sat[∆, A] is poly(n).

Tightness

The tightness problem (Def. 6, point 2) is the complement of a problem slightly stronger than satisfiability (1): given a SID ∆ and a formula φ, such that fv(φ) = {x 1 , . . . , x n }, the looseness problem Loose[∆, A] asks for the existence of a loose configuration γ (Def. 2), such that γ |= ∆ ∃x 1 . . . ∃x n . φ. We establish upper and lower bounds for the complexity of the looseness problem by a reduction to and from the satisfiability problem. The bounds for the tightness problem follow by standard complementation of the complexity classes for the looseness problem.

From Looseness to Satisfiability. Let ∆ be a given SID and A be a predicate. For each predicate B that occurs in ∆, we consider a fresh predicate B , not occurring in ∆, such that #B = #B + 1. The SID ∆ consists of ∆ and, for each rule of ∆ of the form:

B 0 (x 1 , . . . , x #B 0 ) ← ∃y 1 . . . ∃y m . φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h )
where φ is a quantifier-and predicate-free formula, ∆ has the following rules: if (c 1 , p 1 , . . . , c n , p n ) ∈ I because of an interaction atom z 1 .p 1 , . . . , z n .p n from φ, such that ν

B 0 (x 1 , . . . , x #B 0 +1 ) ← ∃y 1 . . . ∃y m . φ * x #B 0 +1 = z * B 1 (t
(z i ) = c i , for all i ∈ [1, n], then (C , I , ρ) |= ν [y←c i ] ∆ φ * y = z i * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ), hence (C , I , ρ) |= ν[y←c i ] ∆ A (x 1 , . . . , x #A , y)
, by the definition of ∆.

else (c

and γ |= ν φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B i-1 (t i-1 1 , . . . ,t i-1 #B i-1 ) * B i+1 (t i+1 1 , . . . ,t i+1 #B i+1 ) * . . . * B h (t h 1 , . . . ,t h #B h ) follows from γ = γ • γ . "⇐" Let γ def = (C , I , ρ) be a configuration and ν be a store, such that γ |= ν ∆ A(x 1 , . . . , x #A ).
Since the only rule of ∆ that defines A is:

A(x 1 , . . . , x #A ) ← ∃y . A (x 1 , . . . , x #A , y) * [y] there exists a component c ∈ C , such that (C \ {c}, I , ρ) |= ν[y←c] ∆ A (x 1 , . . . , x #A , y).
We prove the following:

there exists an interaction (c 1 , p 1 , . . . , c n , p n ) ∈ I , such that c i = c, and

-(C \ {c}, I , ρ) |= ν ∆ A(x 1 , . . . , x #A ),
-(C \ {c}, I , ρ) |= ν [y←c] ∆ φ * y = z * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h )
, where z occurs in an interaction atom from φ. In this case, there exists an interaction (c 1 , p 1 , . . . , c n , p n ) ∈ I , such that c = c i , for some i ∈ [1, n]. Moreover, (C \{c}, I , ρ) |= ν ∆ A(x 1 , . . . , x #A ), because ∆ has a rule:

A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ) such that (C \ {c}, I , ρ) |= ν ∆ φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ). -(C \{c}, I , ρ) |= ν [y←c] ∆ φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B i (t i 1 , . . . ,t i #B i , y) * . . . * B h (t h 1 , . . . ,t h #B h ).
In this case, there exists configurations γ and γ , such that

(C \ {c}, I , ρ) = γ • γ , γ |= ν [y←c] ∆ B i (t i 1 , . . . ,t i #B i , y) and γ |= ν ∆ φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h )
. By the inductive hypothesis, there exists an interaction (c 1 , p 1 , . . . ,

c n , p n ) in γ , such that c = c i , for some i ∈ [1, n] and γ |= ν ∆ B i (t i 1 , . . . ,t i #B i ). Then (c 1 , p 1 , . . . , c n , p n ) ∈ I and (C \ {c}, I , ρ) |= ν ∆ A(x 1 , . . . , x #A ), since ∆ has a rule: A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ) such that γ • γ |= ν ∆ φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ). -(C \ {c}, I , ρ) |= ν [y←c] ∆ φ * [y] this
= ( / 0, {(c 1 , p 1 , c 2 , p 2 )}, ρ),
for some components c 1 , c 2 ∈ C . Then the composition γ • γ is defined and we have

γ • γ |= ν[y 1 ←c 1 ,y 2 ←c 2 ] ∆ A(x 1 , . . . , x #A ) * y 1 .p 1 , y 2 .p 2 , leading to γ • γ |= ν ∆ A(x 1 , . . . , x #A ). Moreover, γ • γ is loose, because c 1 , c 2 ∈ C . "⇐" If γ |= ν ∆ A(x 1 , . . . , x #A ), we necessarily have γ |= ν[y 1 ←c 1 ,y 2 ←c 2 ] ∆ A(x 1 , . . . , x #A ) * y 1 .p 1 , y 2 .p 2 ,
for some components c 1 , c 2 ∈ C, hence there exists a configuration γ , such that γ |= ν ∆ A(x 1 , . . . , x #A ). The polynomial reductions from Lemmas 6 and 7 establish the following complexity bounds for the tightness problem:

Theorem 2. Tight (k,∞) [∆, A] is co-NP-complete, Tight (∞, ) [∆, A] is EXP-complete and Tight[∆, A] is 2EXP. Proof. Since Loose (k,∞) [∆, A] is polynomially-reducible to Sat (k+1,∞) [∆, A], by The- orem 1, we obtain that Loose (k,∞) [∆, A] is in NP. Moreover, since Sat (k,∞) [∆, A] is polynomially-reducible to Loose (k,∞) [∆, A], by Theorem 1, we obtain that Loose (k,∞) [∆, A] is NP-complete. Because Tight (k,∞) [∆, A] is the complement of Loose (k,∞) [∆, A], we ob- tain that Tight (k,∞) [∆, A] is co-NP-complete.
The rest of the bounds are obtained by the same polynomial reductions and the fact that Tight (k,∞) [∆, A] is the complement of Loose (k,∞) [∆, A], for any k and , either integer constants, or infinity.

Degree Boundedness

The boundedness problem (Def. 6, point 3) asks for the existence of a bound on the degree (Def. 4) of the models of a sentence ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ). For instance, it is possible to define inductively star topologies, with a central controller connected to an unbounded number of workers stations. Roughly speaking, the Bnd[∆, A] problem has a negative answer if and only if there are increasingly large unfoldings (expansions of a formula by replacement of a predicate atom with one of its definitions) of A(x 1 , . . . , x #A ) repeating a rule that contains an interaction atom involving a parameter of the rule, which is always bound to the same component. For instance, the rule Worker(x) ← ∃y . x.out, y.in * [y] * Worker(x) (Example 2) declares an unbounded number of interactions x.out, y.in involving the component to which x is bound. Definition 9. Given a predicate A and a sequence (r 1 , i 1 ), . . . , (r n , i n ) ∈ (∆ × N) + , where r 1 is the rule A(x 1 , . . . , x #A ) ← φ ∈ ∆, the unfolding A(x 1 , . . . , x #A ) (r 1 ,i 1 )...(r n ,i n ) = ======= ⇒ ∆ ψ is inductively defined as (1) ψ = φ if n = 1, and (2) ψ is obtained from φ by replacing its i 1 -th predicate atom B(y 1 , . . . , y #B ) with

ψ 1 [x 1 /y 1 , . . . , x #B /y #B ], where B(x 1 , . . . , x #B ) (r 2 ,i 2 )...(r n ,i n ) = ======= ⇒ ∆ ψ 1 is an unfolding, if n > 1.
We show that the Bnd[∆, A] problem can be reduced to the existence of increasingly large unfoldings or, equivalently, a cycle in a finite directed graph, built by a variant of the least fixpoint iteration algorithm used to solve the satisfiability problem (Fig. 3). Definition 10. Given satisfiable base pairs t, u ∈ SatBase and a rule from ∆:

r : A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * B 1 (z 1 1 , . . . , z 1 #B 1 ) * . . . * B h (z h 1 , . . . , z h #B h )
where φ is a quantifier-and predicate-free formula, we write (A, t)

(r, i)

∼∼∼∼ (B, u) if and only if B = B i and there exist satisfiable base tuples t 1 , . . . , u = t i , . . . , t h ∈ SatBase, such that t ∈ Base(φ, {x 1 , . . . ,

x #A }) ⊗ h =1 t [x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A .
We define the directed graph with edges labeled by pairs (r, i) ∈ ∆ × N:

G(∆) def = {def(∆) × SatBase}, { (A, t), (r, i), (B, u) | (A, t) (r, i) ∼∼∼∼ (B, u)} input: a SID ∆ output: G(∆) = (V, E)
1: initially V := / 0, E := / 0 2: for A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ ∈ ∆, with φ quantifier-and predicate-free do 3:

V := V ∪ {A} × Base(φ, {x 1 , . . . , x #A })↓ x 1 ,...,x #A
4: while V or E still change do 5:

for r : A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * * h =1 B (z 1 , . . . , z #B ) ∈ ∆ do 6:
if there exist (B 1 , t 1 ), . . . , (B h , t h ) ∈ V then 7:

X := Base(φ, {x 1 , . . . , x #A }) ⊗ h =1 t [x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A 8: V := V ∪ ({A} × X )
9: The graph G(∆) is built by the algorithm in Fig. 3, a slight variation of the classical Kleene iteration algorithm for the computation of the least solution of the constraints of the form (1)(see Fig. 2). A path

E := E ∪ { (A, t), (r, ), (B , t ) | t ∈ X , ∈ [1, h]}
(A 1 , t 1 ) (r 1 , i 1 ) ∼∼∼∼ (A 2 , t 2 ) (r 2 , i 2 ) ∼∼∼∼ . . . (rn , in) ∼∼∼∼ (A n , t n ) in G(∆) induces a unique unfolding A 1 (x 1 , . . . , x #A 1 ) (r 1 ,i 1 )...(r n ,i n )
= ======= ⇒ ∆ φ (Def. 9). Since the vertices of G(∆) are pairs (A, t), where t is a satisfiable base tuple and the edges of G(∆) reflect the construction of the base tuples from the least solution of the constraints (1), the outcome φ of this unfolding is always a satisfiable formula. Proof. Let r 1 be the following rule:

Lemma 8. Given a path (A 0 , t 0 ) (r 1 , i 1 ) ∼∼∼∼ . . . (rn , in ) ∼∼∼∼ (A n , t n ) in G(∆),
A 0 (x 1 , . . . , x #A 0 ) ← φ, where φ = ∃y 1 . . . ∃y m . ψ * π * * h =2 B (z 1 , . . . , z #B )
and ψ * π is a quantifier-and predicate-free formula and π is, moreover, pure. The proof goes by induction on the length n ≥ 1 of the path. For the base case n = 1, by Def. 10, the edge (A 0 , t 0 ) (r 1 , i 1 )

∼∼∼∼ (A 1 , t 1 ) implies the existence of base tuples u ∈ µ -→ X .∆ (B ),

for all ∈ [2, h], such that B i 1 = A 1 , u i 1 -1 = t 1 and: t 0 ∈ Base(ψ * π, {x 1 , . . . , x #A }) ⊗ h =2 u [x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A Let u def = (C , I , π ), for all ∈ [2, h] and π def = π * * h =2 π
. Since t 0 is satisfiable, there exists a store ν , that agrees with ν over x 1 , . . . , x #A 0 , such that, moreover:

ν (x) = ν (y) only if x ≈ π y, for all x, y ∈ fv(ψ * π ) ∪ ( †) h =2 C ∪ {z i | z 1 , . . . , z n ∈ I (τ), τ ∈ Inter}
We define the configurations (C 1 , I 1 , ρ), . . . , (C h , I h , ρ) inductively, as follows:

-C 1 def = {ν (y) | [y] occurs in ψ}, -I 1 def = {(ν (z 1 ), p 1 , . . . , ν (z s ), p s ) | z 1 .p 1 , . . . , z t .p t occurs in ψ},
for all ∈ [2, h], assuming C 1 , . . . , C -1 and I 1 , . . . , I -1 are defined, let:

D def = -1 i=1 C i ∪ h i= +1 ν (C i ) J def = -1 i=1 I i ∪ h i= +1 ν (I i )
We prove first that D ∩ ν (C ) = / 0 and J ∩ ν (I ) = / 0 (we prove only the first point, the second uses a similar reasoning), by induction on ∈ [2, h]. For the base case D 2 ∩ ν (C 2 ) = / 0, we prove the points below:

-C 1 ∩ ν (C 2 ) = / 0: suppose, for a contradiction, that there exists c ∈ C 1 ∩ ν (C 2 ), then c = ν (y), for a component atom [y] from ψ and c = ν (x), for some x ∈ C 2 . By ( †), we obtain x ≈ π y, contradicting the existence of t 0 .

ν (C i )∩ν (C 2 ) = / 0, for some i ∈ [3, h]: suppose, for a contradiction, that there exists

c ∈ ν (C i ) ∩ ν (C 2 ), then c = ν (x) = ν (y)
, for some x ∈ C i and y ∈ C 2 . By ( †), we obtain x π y, contradicting the existence of t 0 .

We assume that D j ∩ ν (C j ) = / 0, for all j ∈ [2, -1]. By Lemma 3, there exist configu-

rations (C j , I j , ρ), such that C j ∩ D j = / 0 ( ‡) and (C j , I j , ρ) |= ν B j (x 1 , . . . , x #B j ), for all j ∈ [2, -1]. We prove D ∩ ν (C ) = /
0, by showing the following points:

-C j ∩ ν (C ) = /
0, for all j ∈ [1, -1]: suppose, for a contradiction, that there exists We obtain that C i ∩ C j = / 0 and I i ∩ I j = / 0, for all 1 ≤ i < j ≤ h, meaning that the config-

c ∈ C j ∩ ν (C ), for some j ∈ [1, -1], then c ∈ C j ∩ D j , because D j ⊆ ν (C ), in contradiction with C j ∩ D j = / 0 ( ‡). -ν (C j ) ∩ ν (C ) = / 0, for all j ∈ [2, - 1
uration (C , I , ρ) def = (C 1 , I 1 , ρ) • . . . • (C h , I h , ρ) is defined, which leads to (C , I , ρ) |= ν φ.
For the inductive step n > 1, by Def. 10, there exists base tuples u ∈ µ -→

X .∆ (B ), for all ∈ [2, h], such that A 1 = B i 1 , u i 1 -1 = t 1 and: t 0 ∈ Base(ψ * π, {x 1 , . . . , x #A }) ⊗ h =1 u [x 1 /z 1 , . . . , x #B /z #B ] ↓ x 1 ,...,x #A
Then there exists a store ν that agrees with ν over x 1 , . . . , x #A 0 and satisfies ( †). Let

ν def = ν [x 1 /z i 1 1 , . . . , x #A 1 /z i 1 #A 1 ]. By the inductive hypothesis, since (A 1 , t 1 ) (r 2 , i 2 ) ∼∼∼∼ . . . (rn , in ) ∼∼∼∼ (A n , t n ) is a path in G(∆), there exists a configuration (C , I , ρ), such that (C , I , ρ) |= ν A 1 (z i 1 1 , . . . , z i 1 #A 1 ), because (C , I , ρ) |= ν φ 1 , for the unfolding A 1 (x 1 , . . . , x #A 1 ) (r 2 ,i 2 )...(r n ,i n ) = ======= ⇒ ∆ φ 1 .
The required configuration is defined as (C , I , ρ)

def = (C 1 , I 1 , ρ)•. . .•(C i 1 -1 , I i 1 -1 , ρ)• (C , I , ρ) • (C i 1 +1 , I i 1 +1 , ρ) • . . . • (C h , I h , ρ), where (C 1 , I 1 , ρ), . . ., (C i 1 -1 , I i 1 -1 , ρ) and (C i 1 +1 , I i 1 +1
, ρ), . . ., (C h , I h , ρ) are defined as in the base case, by taking ν instead of ν and defining, for all ∈ [2, h] \ {i 1 }:

D def = C ∪ -1 i=1 C i ∪ h i= +1 ν (C i ) J def = I ∪ -1 i=1 I i ∪ h i= +1 ν (I i )
The proof of the fact that C 1 , . . ., C i 1 -1 , C , C i 1 +1 , . . ., C h and I 1 , . . ., I i 1 -1 , I , I i 1 +1 , . . ., I h are pairwise disjoint, respectively, follows by the same argument as in the base case.

Lemma 9. Given an unfolding A 0 (x 1 , . . . ,

x #A 0 ) (r 1 ,i 1 )...(r n ,i n ) = ======= ⇒ ∆ φ, a configuration (C , I , ρ)
and a store ν, such that (C , I , ρ)

|= ν ∆ φ, then G(∆) has a path (A 0 , (C 0 , I 0 , π 0 )) (r 1 , i 1 ) ∼∼∼∼ . . . (rn, in ) ∼∼∼∼ (A n , (C n , I n , π n )), for some (C 0 , I 0 , π 0 ), . . . , (C n , I n , π n ) ∈ SatBase, such that ν(C 0 ) ⊆ C 0 , ν(I 0 ) ⊆ I 0 and ( / 0, / 0, ρ) |= ν π 0 .
Proof. Let r 1 be the following rule:

A 0 (x 1 , . . . , x #A 0 ) ← ∃y 1 . . . ∃y m . ψ * π * * h =2 B (z 1 , . . . , z #B )
and ψ * π is a quantifier-and predicate-free formula and π is, moreover, pure. The proof goes by induction on the length n ≥ 1 of the path. For the base case n = 1, we have φ = ∃y 1 . . . ∃y m . ψ * π * * h =2 B (z 1 , . . . , z #B ), hence there exists a store ν , that agrees with ν over x 1 , . . . , x #A 0 , and configurations (C 1 , I 1 , ρ), . . . , (C h , I h , ρ), such that:

-(C 1 , I 1 , ρ) |= ν ψ * π, -(C , I , ρ) |= ν ∆ B (z 1 , . . . , z #B ), for all ∈ [2, h],
and

-γ = (C 1 , I 1 , ρ) • . . . • (C h , I h , ρ).
We consider the following base tuples:

-(C 1 , I 1 , π 1 ) def = Base(ψ * π, {x 1 , . . . , x #A 0 }), -for all ∈ [2, h], there exist (C , I , π ) ∈ µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ],
such that C ⊆ ν (C ), I ⊆ ν (I ) and ( / 0, / 0, ρ) |= ν π , by Lemma 4. By similar argument to the one from the proof of Lemma 4 (base case), we show that the composition h

=1 (C , I , π ) is defined and let (C 0 , I 0 , π 0 ) def = h =1 (C , I , π ) ↓ x 1 ,...,x #A .
Moreover, we obtain ν(C 0 ) ⊆ C 0 , ν(I 0 ) ⊆ I 0 and ( / 0, / 0, ρ) |= ν π 0 , as in the proof of Lemma 4. Then, by Def. 10, G(∆) has an edge

(A 0 , (C 0 , I 0 , π 0 )) (r 1 , i 1 ) ∼∼∼∼ (B i 1 -1 , (C i 1 -1 , I i 1 -1 , π i 1 -1 )).
For the inductive step n > 1, let

B i 1 -1 (x 1 , . . . , x #B i 1 -1 ) (r 2 ,i 2 )...(r n ,i n ) = ======= ⇒ ∆ φ 1 be an unfold- ing, such that φ is obtained from ∃y 1 . . . ∃y m . ψ * π * * h =2 B (z 1 , . . . , z #B ), by replac- ing B i 1 -1 (z i 1 -1 1 , . . . , z i 1 -1 #B i 1 -1 ) with φ 1 [x 1 /z i 1 -1 1 , . . . , x #B i 1 -1 /z i 1 -1 #B i 1 -1 ]. Since (C , I , ρ) |= ν ∆ φ,
there exists a store ν , that agrees with ν over x 1 , . . . , x #A 0 , and configurations

(C 1 , I 1 , ρ), . . . , (C h , I h , ρ), where γ = (C 1 , I 1 , ρ) • . . . • (C h , I h , ρ
) and the following hold:

-(C 1 , I 1 , ρ) |= ν ψ * π, -(C , I , ρ) |= ν ∆ B (z 1 , . . . , z #B ), for all ∈ [2, h] \ {i 1 + 1}, -(C i 1 -1 , I i 1 -1 , ρ) |= ν ∆ φ 1 [x 1 /z i 1 -1 1 , . . . , x #B i 1 -1 /z i 1 -1 #B i 1 -1 ], hence (C i 1 -1 , I i 1 -1 , ρ) |= ν ∆ B i 1 -1 (z i 1 -1 1 , . . . , z i 1 -1 #B i 1 -1
). We consider the following base tuples:

-(C 1 , I 1 , π 1 ) def = Base(ψ * π, {x 1 , . . . , x #A 0 }), -for all ∈ [2, h]\{i 1 + 1}, there exist (C , I , π ) ∈ µ - → X .∆ (B )[x 1 /z 1 , . . . , x #B /z #B ],
such that C ⊆ ν (C ), I ⊆ ν (I ) and ( / 0, / 0, ρ) |= ν π , by Lemma 4.

-G(∆) has a path

(B i 1 -1 , (C 1 , I 1 , π 1 )) (r 2 , i 2 ) ∼∼∼∼ . . . (rn , in ) ∼∼∼∼ (A n , (C n , I n , π n )), such that C i 1 -1 ⊆ ν (C 1 ), I i 1 -1 ⊆ ν (I 1
) and ( / 0, / 0, ρ) |= ν π 1 , by the inductive hypothesis.

By an argument similar to the one from Lemma 4, the composition (C , I , π)

def = i 1 -2 =1 (C , I , π )⊗ (C 1 , I 1 , π 1 )⊗ h =i 1 (C , I , π ) is defined and let (C 0 , I 0 , π 0 ) def = (C , I , π)↓ {x 1 ,...,x #A 0 } . Fi-
nally, the conditions ν(C 0 ) ⊆ C 0 , ν(I 0 ) ⊆ I 0 and ( / 0, / 0, ρ) |= ν π 0 follow from a similar argument to the one used in Lemma 4.

An elementary cycle of G(∆) is a path from some vertex (B, u) back to itself, such that (B, u) does not occur on the path, except at its endpoints. The cycle is, moreover, reachable from (A, t) if and only if there exists a path (A, t)

(r 1 , i 1 ) ∼∼∼∼ . . . (rn , in ) ∼∼∼∼ (B, u) in G(∆).
We reduce the complement of the Bnd[∆, A] problem, namely the existence of an infinite set of models of ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ) of unbounded degree, to the existence of a reachable elementary cycle in G(∆ ), where ∆ is obtained from ∆, as described in the following.

First, we consider, for each predicate B ∈ def(∆), a predicate B , of arity #B + 1, not in def(∆) i.e., the set of predicates for which there exists a rule in ∆. Second, for each rule B 0 (x 1 , . . . , x #B 0 ) ← ∃y 1 . . . ∃y m . φ * * h =2 B (z 1 , . . . , z #B ) ∈ ∆, where φ is a quantifier-and predicate-free formula and iv(φ) ⊆ fv(φ) denotes the subset of variables occurring in interaction atoms in φ, the SID ∆ has the following rules:

B 0 (x 1 , . . . , x #B 0 , x #B 0 +1 ) ← ∃y 1 . . . ∃y m . φ * * ξ∈iv(φ) x #B 0 +1 = ξ * * h =2 B (z 1 , . . . , z #B , x #B 0 +1 ) (2)
B 0 (x 1 , . . . , x #B 0 , x #B 0 +1 ) ← ∃y 1 . . . ∃y m . φ * x #B 0 +1 = ξ * * h =2 B (z 1 , . . . , z #B , x #B 0 +1 ) (3)
for each variable ξ ∈ iv(φ), that occurs in an interaction atom in φ.

Intuitively, there exists a family of models (with respect to ∆) of ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ) of unbounded degree if and only if these are models of ∃x 1 . . . ∃x #A+1 . A (x 1 , . . . , x #A+1 ) (with respect to ∆ ) and the last parameter of each predicate B ∈ def(∆ ) can be mapped, in each of the these models, to a component that occurs in unboundedly many interactions. The latter condition is equivalent to the existence of an elementary cycle, containing a rule of the form (3), that it, moreover, reachable from some vertex (A , t) of G(∆ ), for some t ∈ SatBase. This reduction is formalized below:

Lemma 10. Let A be a predicate and γ be a model of ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ). Then there exists an unfolding A(x 1 , . . . ,

x #A ) w = ⇒ ∆ ψ of length |w| ≥ log(δ(γ))-log β 1 log β 2
where β 1

is the maximal number of components and interaction atoms and β 2 is the maximal number of predicate atoms, occurring in a rule of ∆.

Proof. Let γ be a configuration, ν be a store and A be a predicate, such that γ |= ν ∆ A(x 1 , . . . , x #A ). We consider the derivation tree T induced by the definition of the |= ν ∆ relation. The nodes of T are labelled by a triple γ |= ν ∆ B(x 1 , . . . , x #B ). We start from the root labelled by γ |= ν ∆ A(x 1 , . . . , x #A ) and define the children of a node inductively. For each node γ |= ν ∆ B(x 1 , . . . , x #B ), there exists a rule:

r : B(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * B 1 (z 1 1 , . . . , z 1 #B 1 ) * . . . * B h (z h 1 , . . . , z h #B h ) and configurations γ 0 , . . . , γ h , such that γ = γ 0 •. . .•γ h , γ 0 |= ν ∆ φ and γ i |= ν ∆ B i (z i 1 , . . . , z i #B i ) for every i ∈ [1, h],
where φ is a predicate-free formula and ν is a store that agrees with

ν over x 1 , . . . , x #B . We define ν def = ν [x 1 /z , . . . , x #B /z #B ], for all ∈ [1, h]. Then the node γ |= ν ∆ B(x 1 , . . . , x #B ) has h children in T , where the -th child is labelled by γ |= ν ∆ B (x 1 , . . . , x #B ), for all ∈ [1, h]. The construction is finite since γ |= ν ∆ A(x 1 , . . . , x #A ) has a finite inductive definition.
We now consider the degree of the configurations which occur in T . By Def. 3, we obtain δ(γ) ≤ δ(γ 0 ) + ∑ h i=1 δ(γ i ). With each γ i associated to a child of this node (except γ 0 ), we obtain that δ(γ init ) does not exceed β 1 times the number of nodes in T . Since h ≤ β 2 , the height n of T is bound to the degree δ(γ) by the inequality δ(γ) ≤

β 1 × ∑ n k=0 β 2 k = β 1 × β 2 n+1 -1, leading to: n + 1 ≥ log δ(γ) -log β 1 log β 2
Finally, with T of height n, there exists a branch in T (starting from the root) of length exactly n + 1. Yet each branch of T corresponds to an unfolding A(x 1 , . . . ,

x #A ) w = ⇒ ∆ ψ,
with w obtained by concatenating for every node (γ, ν, A) of the branch (from root to leaf) the couple (r, i) consisting of:

the rule r ∈ ∆ used to unfold A(x 1 , . . . , x #A ), and the position i of this node among its brothers in T (take i = 1 for the root). This unfolding has the length required, which concludes the lemma. Lemma 11. There exists an infinite sequence of configurations γ 1 , γ 2 , . . . such that γ i |= ∆ ∃x 1 . . . ∃x #A . A(x 1 , . . . , x #A ) and δ(γ i ) < δ(γ i+1 ), for all i ≥ 1 if and only if G(∆ ) has an elementary cycle containing a rule (3), reachable from a node (A , t), for t ∈ SatBase.

Proof. "⇒" Let ν 1 , ν 2 , . . . be stores such that γ i |= ν i ∆ A(x 1 , . . . , x #A ), for all i ≥ 1. By Lemma 10, where exists unfoldings A(x 1 , . . . , x #A )

w i = ⇒ ∆ φ i of lengths |w 1 | < |w 2 | < . . ., such that γ i |= ν i ∆ φ i , for all i ≥ 1. For each configuration γ i , let d i ∈ C be a component, such that δ(γ i ) = ||{(c 1 , p 1 , . . . , c n , p n ) | d i = c j , j ∈ [1, n]}||. By induction on |w i | ≥ 1,
we build unfoldings A (x 1 , . . . , x #A , x #A+1 ) w i = ⇒ ∆ φ i that bind x #A+1 to all variables bound to d i , using rules of type [START_REF] Bar-Hillel | On formal properties of simple phrase structure grammars[END_REF]. By Lemma 9, w 1 , w 2 , . . . are labels of paths from G(∆ ), that start in (A, t 1 ), (A, t 2 ), . . ., respectively. Since G(∆ ) is finite, we can chose an infinite subsequence of paths that start in the same node of G(∆ ) and repeat the same vertex, with a rule of type (3) in between.

"⇐" Let (A , t)

(r 1 , i 1 ) ∼∼∼∼ . . . (r n , in) ∼∼∼∼ (B n , t n ) (r n+1 , i n+1 ) ∼∼∼∼∼∼∼∼ . . . (r n+p , i n+p )
∼∼∼∼∼∼∼∼ (B n , t n ) be a path in G(∆ ), such that one of the rules r n+1 , . . . , r n+p is of the form (3) and let w i def = (r 1 , i 1 ) . . . (r n , i n )[(r n+1 , i n+1 ) . . . (r n+p , i n+p )] i , for all i ≥ 1. By Lemma 8, there exist unfoldings A (x 1 , . . . , x #A+1 )

w i = ⇒ ∆ φ i , stores ν i and configurations γ i , such that γ i |= ν i φ i .
We define:

δ i def = ||{(c 1 , p 1 , . . . , c n , p n ) ∈ I i | ν(x #A+1 ) = c j , j ∈ [1, n]}||, for all i ≥ 1
where γ i def = (C i , I i , ρ i ). Since γ i |= ν i φ i and one of the rules r n+1 , . . . , r n+p is of type (3), the sequence δ 1 , δ 2 , . . . is strictly increasing. Moreover, we have δ i ≤ δ(γ i ), for all i ≥ 1, hence there exists a sequence of integers 1 ≤ i 1 < i 2 < . . . such that δ(γ i j ) < δ(γ i j+1 ), for all j ≥ 1.

The complexity result below uses a similar argument on the maximal size of (hence the number of) base tuples as in Theorem 1, leading to similar complexity gaps:

Theorem 3. Bnd (k,∞) [∆, A] is in co-NP, Bnd (∞, ) [∆, A] is in EXP and Bnd[∆, A] is in 2EXP.
Proof. Lemma 11 shows the reduction of the complement of Bnd[∆, A] to the existence of a reachable cycle in the graph G(∆ ), where ∆ is constructed from ∆ in polynomial time. Moreover, we have arity(∆ ) = arity(∆) + 1 and intersize(∆ ) = intersize(∆). We distinguish the three cases below:

k < ∞, = ∞: in this case, we can define a non-deterministic algorithm as follows.

We guess the solution ( W 1 , . . . ,W K ,W K+1 , i 1 , i 2 , . . . , i n , where:

• W 1 , . . . ,W K defines an acyclic witness for a satisfiable least solution of A in ∆ constructed as in the proof of Thm. 1; • W K+1 = (T K+1 , r K+1 ,t K+1,1 , ..., e K+1,h K+1 ) is similar to a regular entry W i , that is, contains a base tuple T K+1 , an index r K+1 of a rule of ∆ and indices e K+1,1 , . . ., e K+1,h K+1 ∈ {1, . . . , K} such that T K+1 is computed correctly by applying the rule r K+1 from base tuples T e K+1,1 , . . . , T e K+1,h K+1 as explained in the proof of Thm. 1; • i 1 , i 2 , . . . , i n defines an acyclic path starting at the initial node in the directed acyclic graph defined by W , that is, 1 = i 1 < i 2 < . . . < i n ≤ K and moreover i j+1 ∈ {e i j ,1 , . . . , e i j ,h i j } for all j ∈ {1, 2, . . . , n -1}; • the path i 1 , i 2 , . . . , i n can be closed into a witness reachable cycle from i 1 by using W K+1 that is, whenever (i) rules r i n and r K define the same predicate, and moreover T i n = T K+1 , (ii) the intersection X = {e K+1,1 , . . . , e K+1,h K+1 } ∩ {i 1 , i 2 , . . . , i n } = / 0, (iii) if i j = min X, that is, the cycle starts at i j then at least one of the rules used along the cycle r i j , r i j+1 , . . . , r i n-1 , r K+1 is of the form (3).

The solution is of linear size O(size(∆ )) by the same arguments as in the proof of Thm. 1. Therefore, it can be guessed in polynomial time, and moreover checked in polynomial time following the conditions above. This implies the membership of the complement problem in NP, henceforth Bnd (k,∞) [∆, A] is in co-NP.

k = ∞, < ∞: in this case, using the algorithm from Fig. 3, the graph G(∆ ) is constructed in time 2 poly(size(∆ )) as previously explained in the proof of Theorem 1. Finding a reachable cycle with the additional properties required by Lemma 11 can be done in two additional steps, respectively, first building the SCCs decomposition of G(∆ ) and then checking reachability of SCCs containing edges derived from rules of form (3) from SCCs containing vertices (A , t). Both steps can be done in in linear time in the size of G(∆ ) i.e., using Tarjan algorithm for SCC decomposition and standard graph traversals. Therefore, the overall time complexity remains 2 poly(size(∆ )) , and as such Bnd (∞, ) [∆, A] is in EXP.

k = ∞, = ∞: following the same argument as in the previous point and noticing that the graph G(∆ ) is constructed in time 2 2 poly(size(∆ )) we conclude that Bnd[∆, A] is in 2EXP.

Moreover, the construction of G(∆ ) allows to prove the following cut-off result: Proposition 1. Let γ be a configuration and ν be a store, such that γ

|= ν ∆ A(x 1 , . . . , x #A ). If Bnd (k, ) [∆, A] then (1) δ(γ) = poly(size(∆)) if k < ∞, = ∞, (2) δ(γ) = 2 poly(size(∆)) if k = ∞, < ∞ and (3) δ(γ) = 2 2 poly(size(∆)) if k = ∞, = ∞.
Proof. First, we show that in all cases, the degree is bounded by 2 B * • L • I where B * is the maximal length of a satisfiable base tuple in ∆ , L is the number of predicates in ∆ and I is the maximal number of interactions defined in a rule in ∆ . The maximal length B * of a satisfiable base tuples has been considered in the proof of Thm. 1 to derive an upper bound on the the number of distinct satisfiable base tuples for a SID.

Then, 2 B * • L represents a bound on the number of nodes in the graph G(∆ ) as for every predicate there will be at most 2 B * satisfiable base tuples associated to it. Meantime, this value also represents a bound on the longest acyclic path in G(∆ ). We are interested on acyclic paths because cycles in G(∆ ) are guaranteed to never connect (use in interactions) the extra variable introduced in ∆ (otherwise the system would not be of bounded degree). But then, along the acyclic paths, at most I interactions are defined at each step, henceforth, the bound of 2 B * • L • I on the number on total interactions that could involve the extra variable.

Second, let observe that both L and I are the same in ∆ and in ∆ and equal to O(size(∆)). Moreover, it was shown in the proof of Thm. 1 that B * = 2α + 2α 2 + p min(α,β) α min(α,β) for α = arity(∆ ) = arity(∆) + 1 and β = intersize(∆ ) = intersize(∆), p = ||P || the number of ports. Henceforth, we distinguished the three cases, respec- This section is concerned with the entailment problem Entl[∆, A, B], that asks whether γ |= ν ∆ ∃x #A+1 . . . ∃x #B . B(x 1 , . . . , x #B ), for every configuration γ and store ν, such that γ |= ν ∆ A(x 1 , . . . , x #A ). For instance, the proof from Fig. 1 (c) relies on the following entailments, that occur as the side conditions of the Hoare logic rule of consequence:

tively (i) B * = O(1) if k < ∞, = ∞, (ii) B * = poly(size(∆)) if k = ∞, < ∞ and (iii) B * = 2 poly(size(∆)) if k = ∞, = ∞.
ring h,t (y) |= ∆ ∃x∃z.[y]@H * y.out, z.in * chain h-1,t (z, x) * x.out, y.in [z]@H * z.out, x.in * chain h-1,t (x, y) * y.out, z.in |= ∆ ring h,t (z)
By introducing two fresh predicates A 1 and A 2 , defined by the rules:

A 1 (x 1 ) ← ∃y∃z.[x 1 ]@H * x 1 .out, z.in * chain h-1,t (z, y) * y.out, x 1 .in (4) A 2 (x 1 , x 2 ) ← ∃z.[x 1 ]@H * x 1 .out, z.in * chain h-1,t (z, x 2 ) * x 2 .out, x 1 .in (5)
the above entailments are equivalent to Entl[∆, ring h,t , A 1 ] and Entl[∆, A 2 , ring h,t ], respectively, where ∆ consists of the rules ( 4) and ( 5), together with the rules that define the ring h,t and chain h,t predicates ( §1.1). We show that the entailment problem is undecidable, in general (Thm. 4), and recover a decidable fragment, by means of three syntactic conditions, typically met in our examples. These conditions use the following notion of profile: Definition 11. The profile of a SID ∆ is the pointwise greatest function λ ∆ : A → pow(N), mapping each predicate A into a subset of [1, #A], such that, for each rule A(x 1 , . . . , x #A ) ← φ from ∆, each atom B(y 1 , . . . , y #B ) from φ and each i ∈ λ ∆ (B), there exists j ∈ λ ∆ (A), such that x j and y i are the same variable.

The profile identifies the parameters of a predicate that are always replaced by a variable x 1 , . . . , x #A in each unfolding of A(x 1 , . . . , x #A ), according to the rules in ∆; it is computed by a greatest fixpoint iteration, in time poly(size(∆)). Definition 12. A rule A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * * h =1 B (z 1 , . . . , z #B ), where φ is a quantifier-and predicate-free formula, is said to be:

| i ∈ λ ∆ (A)} = / 0.
A SID ∆ is progressing, connected and e-restricted if and only if each rule in ∆ is progressing, connected and e-restricted, respectively.

For example, the SID consisting of the rules from §1.1, together with rules (4) and ( 5) is progressing, connected and e-restricted. For a configuration γ = (C , I , ρ), let:

nodes(γ) def = C ∪ {c i | (c 1 , p 1 , . . . , c n , p n ) ∈ I , i ∈ [1, n]}
be the set of (possibly absent) components that occur in γ.

Lemma 12. Given a progressing SID ∆ and a predicate A ∈ def(∆), for any configuration γ = (C , I , ρ) and store ν, such that γ |= ν ∆ A(x 1 , . . . , x #A ), we have {ν(x 1 ), . . . , ν(x #A )} ⊆ nodes(γ) = C .

Proof. We proceed by fixpoint induction on the definition of γ |= ν ∆ A(x 1 , . . . , x #A ). By definition, there exists a progressing rule

r : A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . [x 1 ] * ψ * * h =1 B (z 1 , . . . , z #B )
a store ν and configurations γ 0 , . . . , γ h such that:

-

γ = γ 0 • . . . • γ h , -ν(x i ) = ν (x i ) for all i ∈ [1, #A], -γ 0 |= ν ∆ [x 1 ] * ψ, and -γ |= ν ∆ B (z 1 , . . . , z #B ) for all ∈ [1, h]. For 1 ≤ ≤ h, let ν (x i ) = ν (z i ) for 1 ≤ i ≤ #B
. Now apply the induction hypothesis on the derivation of γ |= ν ∆ B (x 1 , . . . , x #B ) to obtain that {ν (x 1 ), . . . , ν (x #B )} ⊆ nodes(γ ). Since r is progressing, we have:

{ν(x 1 ), . . . , ν(x #A )} ⊆ {ν (x 1 ), . . . , ν (x #A )} ∪ {ν (y 1 ), . . . , ν (y m )} = {ν (x 1 )} ∪ h =1 {ν (z 1 ), . . . , ν (z #B )} = {ν (x 1 )} ∪ h =1 {ν (x 1 ), . . . , ν (x #B )} ⊆ nodes(γ 0 ) ∪ h =1 nodes(γ ) = nodes(γ)
We recall that def ∆ (A) is the set of rules from ∆ that define A and denote by def * ∆ (A) the least superset of def ∆ (A) containing the rules that define a predicate from a rule in def * ∆ (A). The following result shows that the entailment problem becomes undecidable as soon as the connectivity condition is even slightly lifted: Theorem 4. Entl[∆, A, B] is undecidable, even when ∆ is progressing and e-restricted, and only the rules in def * ∆ (A) are connected (the rules in def * ∆ (B) may be disconnected). Proof. By a reduction from the known undecidable problem of universality of contextfree languages [START_REF] Bar-Hillel | On formal properties of simple phrase structure grammars[END_REF]. A context-free grammar G = N, T, S, ∆ consists of a finite set N of nonterminals, a finite set T of terminals, a start symbol S ∈ N and a finite set ∆ of productions of the form A → w, where A ∈ N and w ∈ (N ∪ T ) * . Given finite strings u, v ∈ (N ∪ T ) * , the step relation u ⇒ v replaces a nonterminal A of u by the right-hand side w of a production A → w and ⇒ * denotes the reflexive and transitive closure of ⇒. The language of G is the set L(G) of finite strings w ∈ T * , such that s ⇒ * w. The problem T * ⊆ L(G) is known as the universality problem, known to be undecidable. Moreover, we assume w.l.o.g. that:

-T = {0, 1}, because every terminal can be encoded as a binary string, -L(G) does not contain the empty string ε, because computing a grammar G such that L(G ) = L(G) ∩ T + is possible and, moreover, we can reduce from the modified universality problem problem Let ∆ be the SID containing the above rules. It is easy to check that the SID is progressing and e-restricted and that, moreover, the rules from def * ∆ (A) are connected. Finally,

T + ⊆ L(G ) instead of the original T * ⊆ L(G), -G
A(x 1 , x 2 ) |= ∆ B(x 1 , x 2 ) if and only if T + ⊆ L(G).
On the positive side, we prove that Entl[∆, A, B] is decidable, if ∆ is progressing, connected and e-restricted, assuming further that Bnd[∆, A] has a positive answer. In this case, the bound on the degree of the models of A(x 1 , . . . , x #A ) is effectively computable, using the algorithm from Fig. 3 (see Prop. 1 for a cut-off result) and denote by B this bound, throughout this section.

The proof uses a reduction of Entl[∆, A, B] to a similar problem for SL, showed to be decidable [START_REF] Echenim | Unifying decidable entailments in separation logic with inductive definitions[END_REF]. We recall the definition of SL, interpreted over heaps h : C fin C K , introduced in §2.3. SL rules are denoted as A(x 1 , . . . , x #(A) ) ← φ, where φ is a SL formula, such that fv(φ) ⊆ {x 1 , . . . , x #(A) } and SL SIDs are denoted as ∆. The profile λ ∆ is defined for SL same as for CL (Def. 11). Definition 13. A SL rule A(x 1 , . . . , x #(A) ) ← φ from a SID ∆ is said to be: Note that the definitions of progressing and connected rules are different for SL, compared to CL (Def. 12); in the rest of this section, we rely on the context to distinguish progressing (connected) SL rules from progressing (connected) CL rules. Moreover, e-restricted rules are defined in the same way for CL and SL (point 3 of Def. 12). A tight upper bound on the complexity of the entailment problem between SL formulae, interpreted by progressing, connected and e-restricted SIDs, is given below:

Theorem 5 ( [START_REF] Echenim | Unifying decidable entailments in separation logic with inductive definitions[END_REF]). The SL entailment problem is in 2 2 poly(width(∆)•log size(∆)) , for progressing, connected and e-restricted SIDs.

The reduction of Entl[∆, A, B] to SL entailments is based on the idea of viewing a configuration as a logical structure (hypergraph), represented by an indirected Gaifman graph, in which every tuple from a relation (hyperedge) becomes a clique [START_REF] Gaifman | On local and non-local properties[END_REF]. In a similar vein, we encode a configuration, of degree at most B, by a heap of degree K (Def. 14), such that K is defined using the following integer function: [pos(i -1, j, 0), pos(i, j, 0)] are the entries of the i-th interaction of type τ j in h(c 0 ), 3. for all k ∈ [1, N], we have h(c 0 ) state(k) = c 0 if and only if ρ(c 0 ) = q k , where the entry state(k) def = pos(0, M + 1, k -1) in h(c 0 ) corresponds to the state q k ∈ Q . We denote by G(γ) the set of Gaifman heaps for γ.

pos(i, j, k) def = 1 + B • j-1 ∑ =1 |τ | + i • |τ j | + k T x H y H z out in out in (a) 1 2 1 2 [x] out, in H T 1 2 1 2 [y] out, in H T 1 2 1 2 [z] out, in H T x y z (
Intuitively, if h is a Gaifman heap for γ and c 0 ∈ dom(h), then the first entry of h(c 0 ) indicates whether c 0 is present (condition 1 of Def. 14), the next B • ∑ M j=1 |τ j | entries are used to encode the interactions of each type τ j (condition 2 of Def. 14), whereas the last N entries are used to represent the state of the component (condition 3 of Definition 14). Note that the encoding of configurations by Gaifman heaps is not unique: two Gaifman heaps for the same configuration may differ in the order of the tuples from the encoding of an interaction type and the choice of the unconstrained entries from h(c 0 ), for each c 0 ∈ dom(h). On the other hand, if two configurations have the same Gaifman heap encoding, they must be the same configuration. We say that a configuration γ is a subconfiguration of γ, denoted γ γ if and only if γ = γ • γ , for some configuration γ . The following lemma builds Gaifman heaps for subconfigurations: Lemma 13. Given configurations γ and γ , such that γ γ, if h ∈ G(γ), then h ∈ G(γ ), where dom(h ) = dom(h) ∩ nodes(γ ) and h (c) = h(c), for all c ∈ dom(h ).

Proof. We have dom(h ) = dom(h) ∩ nodes(γ ) = nodes(γ) ∩ nodes(γ ) = nodes(γ ), because dom(h) = nodes(γ) ⊇ nodes(γ ). The points (1-3) of Def. 14 are by easy inspection.

We build a SL SID ∆ that generates the Gaifman heaps of the models of the predicate atoms occurring in a progressing CL SID ∆. The construction associates to each variable x, that occurs free or bound in a rule from ∆, a unique K-tuple of variables η(x) ∈ V K , that represents the image of the store value ν(x) in a Gaifman heap h i.e., h(ν(x)) = ν(η(x)). Moreover, we consider, for each predicate symbol A ∈ def(∆), an annotated predicate symbol A ι of arity #A ι = (K + 1) • #A, where ι : [1, #A] × [1, M] → 2 [0,B-1] is a map associating each parameter i ∈ [1, #A] and each interaction type τ j , for j ∈ [1, M], a set of integers ι(i, j) denoting the positions of the encodings of the interactions of type τ j , involving the value of x i , in the models of A ι (x 1 , . . . , x #A , η(x 1 ), . . . , η(x #A )) (point 2 of Def. 14). Then ∆ contains rules of the form:

A ι (x 1 , . . . , x #(A) , η(x 1 ), . . . , η(x #(A) )) ← (6) ∃y 1 . . . ∃y m ∃η(y 1 ) . . . ∃η(y m ) . ψ * π * * h =1 B ι (z 1 , . . . , z #(B ) , η(z 1 ), . . . , η(z #(B ) ))

for which ∆ has a stem rule A(x 1 , . . . , x #(A) ) ← ∃y 1 . . . ∃y m . ψ * π * * h =1 B (z 1 , . . . , z #B ), where ψ * π is a quantifier-and predicate-free formula and π is the conjunction of equalities and disequalities from ψ * π. However, not all rules (6) are considered in ∆, but only the ones meeting the following condition: Definition 15. A rule of the form ( 6) is well-formed if and only if, for each i ∈ [1, #A] and each j ∈ [1, M], there exists a set of integers Y i, j ⊆ [0, B -1], such that:

-||Y i, j || = ||I j ψ,π (x i )||, where I j ψ,π (x) is the set of interaction atoms z 1 .p 1 , . . . , z n .p n from ψ of type τ j = p 1 , . . . , p n , such that z s ≈ π x, for some s ∈ [1, n],

-Y i, j ⊆ ι(i, j) and ι(i, j) \Y i, j = Z j (x i ), where Z j (x) We denote by ∆ the set of well-formed rules [START_REF] Bozga | Verification of component-based systems with recursive architectures[END_REF], such that, moreover: Here for two tuples of variables x = x 1 , . . . , x k and y = y 1 , . . . , y k , we denote by x = y the formula * k i=1 x i = y i . Intuitively, the SL formula CompStates ψ (x) realizes the encoding of the component and state atoms from ψ, in the sense of points (1) and (3) from Def. 14, whereas the formula InterAtoms ψ (x i ) realizes the encodings of the interactions involving a parameter x i in the stem rule (point 2 of Def. 14). In particular, the definition of InterAtoms ψ (x i ) uses the fact that the rule is well-formed. Lemma 14. Let ∆ be a progressing SID and A ∈ def(∆) be a predicate, such that γ |= ν A(x 1 , . . . , x #A ), for some configuration γ = (C , I , ρ) and store ν. Then, for each heap h ∈ G(γ), there exists a map ι : [1, #A] × [1, M] → 2 [0,B-1] and a store ν, such that the following hold: 1. ν(x i ) = ν(x i ) ∈ dom(h) and ν(η(x i )) = h(ν(x i )), ∀i ∈ [1, #A], 2. Tuples ) is a rule from ∆, such that ψ * π is quantifier-and predicate-free and π is the conjunction of equalities and disequalities from ψ * π. Then there exists a store ν , that agrees with ν over x 1 , . . . , x #A , and configurations γ 0 = (C 0 , I 0 , ρ), . . . , γ h = (C h , I h , ρ), such that:

ψ def = x 1 → η(
-γ 0 |= ν ∆ ψ * π, -γ |= ν ∆ B (z 1 , . . . , z #B
), for all ∈ [1, h], and γ = γ 0 • . . . • γ h . We define the heaps h 0 , . . . , h h , as follows:

for each ∈ [1, h], let dom(h ) = nodes(γ ), h (c) = h(c), for all c ∈ dom(h ), -h 0 def = h \ ( h =1 h ). By Lemma 13, we obtain that h ∈ G(γ ), for all ∈ [1, h]. We define h def = h 0 ∪ . . . ∪ h h and prove that this is indeed a heap, by showing dom(h i ) ∩ dom(h j ) = / 0, for all 0 ≤ i < j ≤ h. If i = 0, we have dom(h i ) ∩ dom(h j ) = / 0, by the definition of h i . Else, suppose, for a contradiction, that c ∈ dom(h i ) ∩ dom(h j ), for some 1 ≤ i < j ≤ h. Then c ∈ nodes(γ i ) ∩ nodes(γ j ). Since γ |= ∃x 1 . . . ∃x #B . B(x 1 , . . . , x #B ), by Lemma 12, we obtain c ∈ C i ∩ C j , which contradicts the fact that γ i • γ j is defined. Next, we apply the inductive hypothesis to find stores ν and maps ι such that, for ∈ [1, h], we have:

ν(z i ) = ν (z i ) ∈ dom(h ) and h (ν (z i )) = ν(η(z i )), ∀i ∈ [1, #B ], -Tuples -Tuples j I 0 (ν(x i )) = {c 1 , . . . , c s i, j }, and -0 ≤ k i, j 1 < . . . < k i, j s i, j < B are integers, such that h(ν(x i )) inter( j,k i, j ) = c , ∀ ∈ [1, s i, j ]; the existence of these integers is stated by point (2) of Def. 14, relative to ν(x i ). Second, we define the store ν as follows:

ν(x 1 ) = ν(x 1 ) and ν(η(x 1 ))

def = h(ν(x 1 )), -ν(z i ) def = ν (z i ), ∀ ∈ [1, h] ∀i ∈ [1, #B ], -ν(η(z i )) def = h(ν (z i )), ∀ ∈ [1, h] ∀i ∈ [1, #B ],
ν is arbitrary everywhere else. The points (1) and (2) of the statement follow from the definitions of ν and ι, respectively. To prove point (3), suppose, for a contradiction, that k ∈ {k i, j 1 , . . . , k i, j s i, j }∩ι (t, j) =

  (a) is B = ({in, out}, {H, T}, {H in -→ T, T out -→ H}). The universe C and the behavior B = (P , Q , -→) are considered fixed in the rest of this paper.

Definition 3 .

 3 (a) is tight and becomes loose if a component is deleted. Moreover, the reconfiguration program from Fig. 1 (c) manipulates tight configurations only. In particular, loose configurations are useful for the definition of a composition operation, as the union of disjoint sets of components and interactions: The composition of two configurations

  for a contradiction, that ν 0 (y) ∈ D, for a variable y, such that [y] occurs in ψ. By the definition of ν 0 , we have either ν 0 (y) ∈ ν 0 (C 0 ) orν 0 (y) ∈ K . Since ν 0 (C 0 ) ∩ D = K ∩ D = /0, both cases lead to a contradiction. • C ∩ D = / 0, for all ∈ [2, h]: because C ∩ D = / 0 and D ⊆ D , by definition of D , for all ∈ [2, h]. Lemma 4. Given a predicate atom A(y 1 , . . . , y #A ), a store ν and a configuration (C , I , ρ), such that (C , I , ρ) |= ν ∆ A(y 1 , . . . , y #A ), there exists a base tuple (C ,

Lemma 5 .

 5 where ( / 0, / 0, ρ) |= ν 0 dist(I ) follows from the satisfiability of (C , I , π ), for all ∈ [2, h]. Sat[∆, A] has a positive answer if and only if µ -→ X .∆ (A) = / 0.

  For non-negative integers m ≤ n denote by S n,m def = n! (n-m)! the number of ordered m-element subsets of a n-element set. Let α = arity(∆), β = intersize(∆) and p = ||P ||. The maximum length of a satisfiable base tuple is B def = α + (∑ min(α,β) j=1

1 .

 1 k < ∞, = ∞: since α ≤ k then α is constant and B * = O(1), 2. k = ∞, < ∞: since β ≤ and α = O(size(∆)) then B * = poly(size(∆)), 3. k = ∞, = ∞: since α = O(size(∆)) then B * = 2 poly(size(∆)) .

  by fixpoint induction on the definition of (C \{c}, I , ρ) |= ν[y←c] ∆ A (x 1 , . . . , x #A , y). Based on the definition of ∆, we distinguish the following cases, where φ is quantifier-and predicate-free, c 1 , . . . , c m ∈ C are components and ν def = ν[y 1 ← c 1 , . . . , y m ← c m ]:

Fig. 3 :

 3 Fig. 3: Algorithm for the Construction of G(∆)

  where t 0 = (C , I , π), a state map ρ and a store ν, such that ( / 0, / 0, ρ) |= ν π, there exists a configuration (C , I , ρ), such that (C , I , ρ) |= ν ∆ φ, where A 0 (x 1 , . . . , x #A 0 ) (r 1 ,i 1 )...(r n ,i n ) = ======= ⇒ ∆ φ is the unique unfolding corresponding to the path.

  ]: suppose, for a contradiction, that there exists c ∈ ν (C j ) ∩ ν (C ), then c = ν (x) = ν (y), for some x ∈ C j and y ∈ C . By ( †), we obtain x ≈ π y, contradicting the existence of t 0 . Consequently, D ∩ ν (C ) = / 0, for all ∈ [2, h]. By Lemma 3, there exists a configuration (C , I , ρ), such that C ∩D = / 0 and (C , I , ρ) |= ν B (x 1 , . . . , x #B ), for all ∈ [2, h].

  By using the above in the expression 2 B * • L • I we obtain the values of the bound as stated in the Proposition.

b)Fig. 4 :

 4 Fig. 4: Gaifman Heap for a Chain Configuration

Example 4 .

 4 Fig.4(b) shows a Gaifman heap for the configuration in Fig.4 (a), where each component belongs to at most 2 interactions of type out, in .

  {ι (k, j) | x ≈ π z k } is the set of positions used to encode the interactions of type τ j involving the store value of the parameter x, in the sub-configuration corresponding to an atom B (z 1 , . . . , z #(B ) ), for some ∈ [1, h].

x 1 )= x j p and {k j 1 ,

 11 * * x∈fv(ψ) CompStates ψ (x) * * #A i=1 InterAtoms ψ (x i ), where: CompStates ψ (x) def = * [x] occurs in ψ η(x) 1 = x * * x@q k occurs in ψ η(x) state(k) = x InterAtoms ψ (x i ) def = * M j=1 * r j p=1 η(x i ) inter( j,k j p ) i, j) \ Z j (x i )

jI

  (ν(x i )) = ν(η(x i )) inter( j,k) | k ∈ ι(i, j) , ∀i ∈ [1, #A] ∀ j ∈ [1, M], 3. h ν ∆ A ι (x 1 , . . . , x #A , η(x 1 ), . . . , η(x #(A) )). Proof. By induction on the definition of γ |= ν A(x 1 , . . . , x #A ), assume that γ |= ν ∃y 1 . . . ∃y m . ψ * π * * h =1 B (z 1 , . . . , z #(B ) ),where A(x 1 , . . . , x #(A) ) ← ∃y 1 . . . ∃y m . ψ * π * * h =1 B (z 1 , . . . , z #(B )

jI

  (ν(z i )) = ν (η(z i )) inter( j,k) | k ∈ ι (i, j) , ∀i ∈ [1, #(B )] ∀ j ∈ [1, M], and h ν ∆ B ι (z 1 , . . . , z #B , η(z 1 ), . . . , η(z #(B ) )). First, for each i ∈ [1, #A] and each j ∈ [1, M], we define ι(i, j) def = {k 1 , . . . , k s i }∪ h =1 #B k=1 ι (k, j) | x i ≈ π z k ,where:

  . . , e i,h are index values from {i + 1, . . . , K} for 0 ≤ h i ≤ H. The length of every witness entry is therefore at most B * + log 2 (size(∆)) + H log 2 (L • N) . As N is constant when k < ∞, and L and H are O(size(∆)) it follows that the number of guesses is polynomial for building W 1 , . . . ,W K . We now check that W 1 , . . . ,W K represents indeed a valid computation of a base tuples from the least solution i.e., (C ,

  Intuitively, the last parameter of a B predicate binds to an arbitrary variable of an interaction atom. A configuration γ is loose if and only if the value (component) of some variable occurring in an interaction atom is absent, in which case the component can be added to γ (without clashing with a present component of γ) by the last rule. The reduction is polynomial, since the number of rules in ∆ is linear in the number of rules in ∆ and the size of each newly added rule is increased by a constant. The following lemma states the correctness of the reduction: Lemma 6. Given a SID ∆ and a predicate A, the problem Loose[∆, A] has a positive answer if and only if the problem Sat[ ∆, A] has a positive answer. Since γ is loose, there exists an interaction (c 1 , p 1 , . . . , c n ,p n ) ∈ I , such that c i ∈ C , for some i ∈ [1, n]. We prove that γ |= ν[y←c i ] ∆ A (x 1 , . . . , x #A , y),by fixpoint induction on the definition of γ |= ν ∆ A(x 1 , . . . , x #A ). This is sufficient, because then we obtain (C ∪ {c i }, I , ρ) |= ν ∆ A(x 1 , . . . , x #A ), thus Sat[ ∆, A] has a positive answer. Consider the rule of ∆: A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B

	Proof. "⇒" Let γ

1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ) if z occurs in an interaction atom from φ, and: B 0 (x 1 , . . . , x #B 0 +1 ) ← ∃y 1 . . . ∃y m . φ * B 1 (t 1 1 , . . . ,t 1 #B 1 ) * . . . * B i (t i 1 , . . . ,t i #B i , x #B 0 +1 ) * . . . * B h (t h 1 , . . . ,t h #B h )

for some i ∈ [1, h], if h ≥ 1.

Moreover, for each rule of ∆ of the form above, with no predicate atoms (i.e., h = 0), ∆ contains the rule:

B (x 1 , . . . , x #B+1 ) ← ∃y 1 . . . ∃y m . φ * [x #B 0 +1 ]

if and only if φ contains no predicate atoms. Finally, there is a fresh predicate A, of arity #A, with a rule:

A(x 1 , . . . , x #A ) ← ∃y . A (x 1 , . . . , x #A , y) * [y] def = (C , I , ρ) be a loose configuration, such that γ |= ν ∆ A(x 1 , . . . , x #A ),

for some store ν. h )

where φ is quantifier-and predicate-free and c 1 , . . . , c m ∈ C are components, such that

(C , I , ρ) |= ν ∆ φ * B 1 (t

1 1 , . . . ,t 1 #B 1 ) * . . . * B h (t h 1 , . . . ,t h #B h ), where ν def = ν[y 1 ← c 1 , . . . , y m ← c m ]. We distinguish the following cases:

  case contradicts the semantics of CL.

From Satisfiability to Looseness. Given a SID ∆ and a predicate A, we build a SID ∆ that defines a predicate A, of equal arity, not occurring in ∆, such that Sat[∆, A] has a positive answer if and only if there exists a loose configuration γ and a store ν, such that γ |= ν ∆ A(x 1 , . . . , x #A ). The rules of ∆ are the rules of ∆, to which the following rule is added, for some ports p 1 , p 2 ∈ P :

A(x 1 , . . . , x #A ) ← ∃y 1 ∃y 2 . A(x 1 , . . . , x #A ) * y 1 .p 1 , y 2 .p 2

This reduction is polynomial, because we add one rule, of size linear on #A. The following lemma states the correctness of the reduction: Lemma 7. Given a SID ∆ and a predicate A, the problem Sat[∆, A] has a positive answer if and only if the problem Loose[ ∆, A] has a positive answer. Proof. "⇒" If Sat[∆, A] has a positive answer, there exists a configuration γ def = (C , I , ρ) and a store ν, such that γ |= ν ∆ A(x 1 , . . . , x #A ). Consider the configuration γ def

  1. progressing if and only if φ = [x 1 ] * ψ, where ψ consists of interaction atoms involving x 1 and (dis-)equalities, such that h =1 {z 1 , . . . , z #B } = {x 2 , . . . , x #A }∪{y 1 , . . . , y m }, 2. connected if and only if, for each ∈ [1, h] there exists an interaction atom in ψ that contains both z 1 and a variable from {x 1 } ∪ {x i | i ∈ λ ∆ (A)}, 3. equationally-restricted (e-restricted) if and only if, for every disequation x = y from φ, we have {x, y} ∩ {x i

  is in Greibach normal form, i.e. it contains only production rules of the form B 0 → bB 1 . . . B n , where B 0 , . . . B n ∈ N, for some n ≥ 0 and b ∈ T .Let P = {p 0 , p 1 } be a set of ports. For each nonterminal B 0 ∈ N, we have a predicate B 0 or arity two and a rule B 0 (x 1 , x 2 ) ← ∃y 1 . . . ∃y n . [x 1 ] * x 1 .p a , y 1 .p a * B 1 (y 1 , y 2 ) * . . . * B n (y n , x 2 ), for each rule B 0 → bB 1 . . . B n of G. Moreover, we consider the rules A(x 1 , x 2 ) ← ∃z . x 1 .p a , z.p a * A(z, x 2 ) and A(x 1 , x 2 ) ← x 1 .p a , x 2 .p a , for all a ∈ {0, 1}.

  1. progressing if and only if φ = ∃t 1 . . . ∃t m . x 1 → (y 1 , . . . , y K ) * ψ, where ψ contains only predicate and equality atoms, 2. connected if and only if z 1 ∈ {x i | i ∈ λ ∆ (A)} ∪ {y 1 , . . . , y

K }, for every predicate atom B(z 1 , . . . , z #(B) ) from φ.

https://status.cloud.google.com/incident/appengine/19007

We use the universe C here for simplicity, the definition works with any countably infinite set.

/ 0, for some i ∈ [1, #A], j ∈ [1, M], t ∈ [1, #B ] and ∈ [1, h], such that x i ≈ π z t . Then there exists a tuple of components c ∈ Tuples j I 0 (ν(x i )), such that c = ν (η(z i )) inter( j,t) ∈ Tuples j I (ν(z i )). Hence I 0 ∩I = / 0, which contradicts the fact that the composition γ 0 •γ is defined. Hence, the rule:

A ι (x 1 , . . . , x #(A) , η(x 1 ), . . . , η(x #(A) )) ← ∃y 1 . . . ∃y m ∃η(y 1 ) . . . ∃η(y m ) . ψ * π * * h =1 B ι (z 1 , . . . , z #(B ) , η(z 1 ), . . . , η(z #(B ) ))

is well-formed and thus belongs to ∆. To obtain h ν ∆ A ι (x 1 , . . . , x #A , η(x 1 ), . . . , η(x #(A) )), by the definition of:

it is sufficient to prove the following points:

h 0 ν x 1 → η(x 1 ): by the definition ν, we have ν(η(x 1 )) = h(ν(x 1 )), hence it is sufficient to prove that dom(h 0 ) = {ν(x 1 )}. "⊆" Let c ∈ dom(h 0 ) be a component. By the definition of h 0 = h\ h =1 h , we have dom(h 0 ) = dom(h)\ h =1 dom(h ) = nodes(γ) \ h =1 nodes(γ ) = nodes(γ 0 ), because h ∈ G(γ) and h ∈ G(γ ), for all ∈ [1, h]. Since γ 0 |= ν ∆ ψ, we have c = ν (x), for some x ∈ fv(ψ). Suppose, for a contradiction, that x and x 1 are not the same variable, then x ∈ {z 1 , . . . , z #B }, for some ∈ [1, h], because ∆ is progressing (Def. 12). By Lemma 12, we obtain c ∈ nodes(γ Lemma 15. Let ∆ be a progressing SID and A ∈ def(∆) be a predicate, such that -1] and a store ν. Then, the following hold:

2. there exists a configuration γ, such that h ∈ G(γ) and γ |= ν ∆ A(x 1 , . . . , x #A ).

Proof. By fixpoint induction on the definition of h

). Consider the following well-formed rule from ∆:

, where ν is a store that agrees with ν over x 1 , . . . , x #(A) and η(x 1 ), . . . , η(x #(A) ).

(1) If i = 1 then x 1 → η(x 1 ) is a subformula of ψ, thus ν(x 1 ) = ν (x 1 ) ∈ dom(h) and h(ν(x 1 )) = ν (η(x 1 )) = ν(η(x 1 )). Otherwise, because ∆ is progressing, x i ∈ {z 1 , . . . , z #B }, for some ∈ [1, h] and point (1) follows from the inductive hypothesis.

(2) There exist heaps h 0 , . . . , h h , such that the following hold:

-

By the inductive hypothesis, there exist configurations

We define the configuration γ 0 = (C 0 , I 0 , ρ 0 ), as follows:

and only if z@q k occurs in ψ, otherwise ρ 0 is arbitrary. Moreover, we define the state map ρ as ρ(c)

) is defined, namely that, for all 0 ≤ i < j ≤ h, we have:

-C i ∩ C j = / 0: If i = 0 then either C 0 = / 0, in which case we are done, or C 0 = {ν(x 1 )} = {ν (x 1 )}. By the definition of ψ = x 1 → η(x 1 ) * ϕ and h 0 ν ψ, we obtain ν (x 1 ) ∈ dom(h 0 ). Since dom(h 0 ) ∩ dom(h j ) = / 0, we obtain ν(x 1 ) ∈ dom(h j ).

Since

-I i ∩ I j = / 0: If i = 0, by the definition of I 0 , each interaction from I 0 is of the form (ν (z 1 ), p 1 , . . . , ν (z n ), p n ), such that z 1 .p 1 , . . . , z n .p n is an interaction atom occuring in ψ. Since, moreover, ∆ is progressing, we have x 1 ∈ {z 1 , . . . , z n }, hence ν(x 1 ) ∈ {ν (z 1 ), . . . , ν (z n )}. Let (c 1 , p 1 , . . . , c n , p n ) ∈ I j be an interaction. Since h = G(γ): we prove that dom(h) = h =0 dom(h ) = nodes(γ), as required by Def. 14. The conditions (1-3) for c 0 = ν(x 1 ) are by the definition of ψ; for c 0 ∈ dom(h ) these conditions follow from h ∈ G(γ ). "⊆" Let c ∈ dom(h) be a component. If

=0 nodes(γ ) be a component. If c ∈ nodes(γ 0 ) then either c ∈ C 0 or c occurs in some interaction from I 0 . If c ∈ C 0 then c = ν(x 1 ) ∈ dom(h 0 ) ⊆ dom(h), by the definition of C 0 . Else there exists an interaction (c 1 , p 1 , . . . , c n , p n ) ∈ I 0 , such that c ∈ {c 1 , . . . , c n }. In this case c = ν (z), for some variable z that occurs in an interaction atom from ψ. Since ∆ is progressing,

Let the stem of the above rule from ∆ be:

) and ρ agrees with ρ over nodes(γ ), it follows

by definition, and ( / 0, / 0, ρ) |= ν π, because / 0 ν π. Altogether, we obtain

). We state below the main result of this section on the complexity of the entailment problem. The upper bounds follow from a many-one reduction of Entl[∆, A, B] to the SL entailment A ι (x 1 , . . . , x #A , η(x 1 ), . . . , η(x #A )) ∆ ∃x #B+1 . . . ∃x #B ∃η(x #B+1 ) . . . ∃η(x #B ) . B ι (x 1 , . . . , x #B , η(x 1 ), . . . , η(x #B )), in combination with the upper bound provided by Theorem 5, for SL entailments. If k < ∞, the complexity is tight for CL, whereas gaps occur for k = ∞, < ∞ and k = ∞, = ∞, due to the cut-off on the degree bound (Prop. 1), which impacts the size of ∆ and time needed to generate it from ∆. Theorem 6. If ∆ is progressing, connected and e-restricted and, moreover, (1) We prove that, for each map ι : -1] , such that:

"⇒" Let h be a heap and ν be a store, such that h ν ∆ A ι (x 1 , . . . , x #A , η(x 1 ), . . . , η(x #A )). By Lemma 15, we have h(ν(x i )) = ν(η(x i )), for all i ∈ [1, #A] and, moreover, there exists a configuration γ, such that h ∈ G(γ) and γ |= ν ∆ A(x 1 , . . . , x #A ). By the hypothesis, we obtain γ |= ν ∆ ∃x #A+1 . . . ∃x #B . B(x 1 , . . . , x #B ), hence there exists a store ν , that agrees with ν over x 1 , . . . , x #A , such that γ |= ν ∆ B(x 1 , . . . , x #B ). By Lemma 14, there exists a store ν that agrees with ν over x 1 , . . . , x #B , such that h(ν

"⇐" Let γ be a configuration, ν be a store such that γ |= ν ∆ A(x 1 , . . . , x #A ) and h ∈ G(γ) be a heap. Cleary, such a heap exists, for any given configuration, by Def. 14. By Lemma 14, there exists a map ι : -1] and a store ν, that agrees with ν over x 1 , . . . , x #A , such that ν(η -1] and a store ν that agrees with ν over x 1 , . . . , x #A and η(x 1 ), . . . , η(x #A ). By Lemma 15, we have ν (η Since ∆ is progressing and connected, ∆ is progressing and connected as well. Moreover, ∆ is e-restricted, because ∆ is e-restricted and the construction of ∆ only introduces equalities, not disequalities.

(2) The upper bound relies on the result of [START_REF] Echenim | Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment[END_REF]Theorem 32], that gives a 2 2 poly(width(∆)•log size(∆)) upper bound for SL entailments. Note that the number of variables in each rule from ∆ is the number of variables in its stem rule multiplied by K + 1, hence width(∆) ≤ width(∆)

. The time needed to build ∆ and its size are bounded as follows:

By Prop. 1, we consider the following cases: ) is represented by a configuration γ = (C , I , ρ), such that C = dom(h) and I = {(c 0 , p 0 , . . . , c K , p K ) | h(c 0 ) = c 1 , . . . , c K }. Since ∆ is progressing and connected, the CL SID ∆, obtained from the reduction, is progressing and connected. Since, moreover, the reduction does not introduce disequalities, ∆ is trivially erestricted. Because the reduction takes polynomial time, we obtain a 2EXP-hard lower bound.

Conclusions and Future Work

We study the satisfiability and entailment problems in a logic used to write proofs of correctness for dynamically reconfigurable distributed systems. The logic views the components and interactions from the network as resources and reasons also about the local states of the components. We reuse existing techniques for Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF],

showing that our configuration logic is more expressive than SL, fact which is confirmed by a number of complexity gaps. Closing up these gaps and finding tight complexity classes in the more general cases is considered for future work. In particular, we aim at lifting the boundedness assumption on the degree of the configurations that must be considered to check the validity of entailments.