Luca Padovani

Tzu-Chun Chen

Andrea Tosatto

Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi

We define complete type reconstruction algorithms for two type systems ensuring deadlock and lock freedom of linear π-calculus processes. Our work automates the verification of deadlock/lock freedom for a non-trivial class of processes that includes interleaved binary sessions and, to great extent, multiparty sessions as well. A Haskell implementation of the algorithms is available.

Introduction

Type systems help finding potential errors during the early phases of software development. In the context of communicating processes, typical errors are: making invalid assumptions about the nature of a received message; using a communication channel beyond its nominal capabilities. Some type systems are able to warn against subtler errors, and sometimes can even guarantee liveness properties as well. For instance, the type systems presented in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] for the linear π-calculus [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF] ensure well-typed processes to be deadlock and lock free. Such stronger guarantees come at the cost of a richer type structure, hence of a greater programming effort, when programmers are supposed to explicitly annotate programs with types. In this respect, type reconstruction becomes a most wanted tool in the programmer's toolkit: type reconstruction is the procedure that automatically synthesizes, whenever possible, the types of the entities used by a program; in particular, the types of the channels used by a communicating process. In the present work, we describe type reconstruction algorithms for the type systems presented in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF], thereby automating the static deadlock and lock freedom analysis for a non-trivial class of communicating processes.

A deadlock is a configuration with pending communications that cannot complete. A paradigmatic example of deadlock modeled in the π-calculus is illustrated below

(νa, b)( a?(x).b!x | b?(y).a!y ) (1.1)
where the input on a blocks the output on b, and the input on b blocks the output on a.

The key idea used in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] for detecting deadlocks, which is related to earlier works by Kobayashi [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], is to associate each channel with a number -called level -specifying the relative order in which different channels should be used. In (1.1), this mechanism requires a to have smaller level than b in the left subprocess, and greater level than b in the right one. Since no level assignment can simultaneously satisfy both requirements, (1.1) is flagged as ill typed. This mechanism does not prevent locks, namely configurations where some communication remains pending although the process as a whole can make progress. A deadlock-free configuration that is not lock free is

(νa)( *c?(x).c!x | c!a | a!42 ) (1.2)
where the communication pending on a cannot complete. There are no interleaved communications on different channels in (1.2), therefore the level-based mechanism spots no apparent issue. The idea put forward in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] to reject (1.2) is to also associate each channel with another number -called ticket -specifying the maximum number of times the channel can travel in a message. With this mechanism in place, (1.2) is ill typed because a would need an infinite number of tickets to travel infinitely many times on c.

Finding appropriate level and tickets for the channels used by a process can be difficult. We remedy to such difficulty with three contributions. First, we develop complete type reconstruction algorithms for the type systems in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] so that appropriate level and tickets are synthesized automatically, whenever possible. The linear π-calculus [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF], for which the type systems are defined, can model a variety of communicating systems with both static and dynamic network topologies. In particular, binary sessions [START_REF] Dardha | Session types revisited[END_REF] and, to a large extent, also multiparty sessions [18, technical report], can be encoded in it. Second, we purposely use a variant of the linear π-calculus with pairs instead of a polyadic calculus. While this choice has a cost in terms of technical machinery, it allows us to discuss how to deal with structured data types, which are of primary importance in concrete languages but whose integration in linear type systems requires some care [START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equi-recursive types[END_REF]. We give evidence that our algorithms scale easily to other data types, including disjoint sums and polymorphic variants. Third, we present the algorithms assuming the existence of type reconstruction for the linear π-calculus [START_REF] Igarashi | Type reconstruction for linear π-calculus with I/O subtyping[END_REF][START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equi-recursive types[END_REF]. This approach has two positive upshots: (1) we focus on the aspects of the algorithms concerning deadlock and lock freedom, thereby simplifying their presentation and the formal study of their properties; [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF] we show how to combine in a modular way increasingly refined type reconstruction stages and how to address some of the issues that may arise in doing so.

In what follows we review the linear π-calculus with pairs (Section 2) and the type systems for deadlock and lock freedom of [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] (Section 3). Such type systems are unsuitable to be used as the basis for type reconstruction algorithms. So, we reformulate them to obtain reconstruction algorithms that are both correct and complete (Section 4). Then, we sketch an algorithm for solving the constraints generated by the reconstruction algorithms (Section 5) We conclude presenting a few benchmarks, further connections with related work, and directions of future research (Section 6).

The algorithms have been implemented and integrated in a tool for the static analysis of π-calculus processes. The archive with the source code of the tool, available at the page http://di.unito.it/hypha, includes a wide range of examples, of which we can discuss only one in the paper because of space constraints.

The simply-typed linear π-calculus with pairs

The process language we work with is the asynchronous π-calculus extended in two ways: [START_REF] Amtoft | Type and effect systems: behaviours for concurrency[END_REF] we generalize names to expressions to account for pairs and other data types;

(2) we assume that names are explicitly annotated with simple types possibly inferred in a previous reconstruction phase ("simple" means without level/ticket decorations). We annotate free names instead of bound names because, in a behavioral type system, each occurrence of a name may be used according to a different type. Typically, two distinct occurrences of the same linear channel are used for complementary I/O actions. We use m, n, . . . to range over integer numbers; we use sets of variables x, y, . . . and channels a, b, . . . ; names u, v, . . . are either channels or variables; we let polarities p, q, . . . range over subsets of {?, !}; we abbreviate {?} with ?, {!} with !, and {?, !} with #. Processes P, Q, . . . , expressions e, f, . . . , and simple types t, s, . . . are defined below:

Process P, Q ::= 0 | e?(x).P | e!f | P | Q | (νa)P | *P Expression e, f ::= n | u t | (e,f) | fst(e) | snd(e) Simple type t, s ::= int | p[t] | p[t] * | t × s
Expressions include integer constants, names, pairs, and the two pair projection operators fst and snd. Simple types are the regular, possibly infinite terms built using the rightmost productions in grammar above and include the type int of integers, the type p[t] of linear channels to be used according to the polarity p and carrying messages of type t, the type p[t] * of unlimited channels to be used according to the polarity p and carrying messages of type t, and the type t × s of pairs whose components have respectively type t and s. Recall that linear channels are meant to be used for one communication, whereas unlimited channels can be used any number of communications. We require every infinite branch of a type to contain infinitely many occurrences of channel constructors. For example, the term t satisfying the equation t = ?[t] is a valid type while the one satisfying the equation t = t × int is not. We impose this requirement to simplify the formal development, but it can be lifted (for example, the implementation supports ordinary recursive types such as lists and trees).

Since we are only concerned with type reconstruction, we do not give an operational semantics of the calculus. The interested reader may refer to [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF][START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equi-recursive types[END_REF] for generic properties of the linear π-calculus and to [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] for the formalization of (dead)lock freedom. We conclude this section with a comprehensive example that is representative of a class of processes for which our type systems are able to prove deadlock and lock freedom. (where we have omitted simple type annotations) models a system composed of two neighbor processes connected by channels e and f . The process spawned by c!(e, f ) uses e for sending a message to the neighbor. Simultaneously, it waits on f for a message from the neighbor. The process spawned by c!( f ,e) does the opposite. Each exchanged message consists of a payload (omitted) and a continuation channel on which subsequent messages are exchanged. Above, each process sends and receives a fresh continuation a. Once the two communications have been performed, each process iterates with a new pair of corresponding continuations.

Type systems for deadlock and lock freedom

In this section we review the type systems ensuring deadlock and lock freedom [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] for which we want to define corresponding reconstruction algorithms. Both type systems rely on refined linear channel types of the form p[t] n m where the decorations n and m are respectively the level and the tickets of a channel with this type. Intuitively, levels are used for imposing an ordering on the input/output operations performed on channels: channels with lower level must be used before channels with higher level; tickets limit the number of "travels" for channels: a channel with m tickets can be sent at most m times in a message. From now on, we use T , S, . . . to range over types, which have the same structure and constructors as simple types, but where linear channel types are decorated with levels and tickets. We write T for the stripping of T , namely for the simple type obtained by removing all level and ticket decorations from T . For example,

?[int × ![int] n m ] * = ?[int × ![int]] * .
Note that • is a non-injective function. We need some auxiliary operators. First, we extend the notion of level from channel types to arbitrary types. The level of a type T , written |T |, is an element of the set Z ∪ {⊥, } ordered in the obvious way and formally defined thus:

|T | def =          ⊥ if T = p[S] * and ? ∈ p n if T = p[S] n m and p = / 0 min{|T 1 |, |T 2 |} if T = T 1 × T 2 otherwise (3.1)
As an example, we have

|int × ?[![int] 1 0 ] 0 0 | = min{|int|, |?[![int] 1 0 ] 0 0 |} = min{ , 0} = 0.
Intuitively, the level of T measures the inverse urgency for using values of type T in order to ensure (dead)lock freedom: the lowest level (and highest urgency) ⊥ is given to unlimited channels with input polarity, for which we want to guarantee input receptiveness; finite levels are reserved for linear channels; the highest level (and lowest urgency) is given to values such as numbers or channels with empty polarity whose use is not critical as far as (dead)lock is concerned. Note that |T | is well defined because every infinite branch of T has infinitely many channel constructors.

We also need an operator to shift the topmost levels and tickets in types. We define

$ n m T def =      p[S] n+h m+k if T = p[S] h k ($ n m T 1 ) × ($ n m T 2 ) if T = T 1 × T 2 T otherwise (3.
2) so that, for example, we have

$ 2 1 (int × ?[![int] 1 0 ] 0 0 ) = int × ?[![int] 1 0 ] 2 1 .
Next, we define an operator for combining the types of different occurrences of the same object. If an object is used according to type T in one part of a process and according to type S in another part, then it is used according to the type T + S overall, where T + S is inductively defined thus:

T + S def =                int if T = S = int (T 1 + S 1 ) × (T 2 + S 2 ) if T = T 1 × T 2 and S = S 1 × S 2 (p ∪ q)[T ] n h+k if T = p[T ] n h and S = q[T ] n k and p ∩ q = / 0 (p ∪ q)[T ] * if T = p[T ] * and S = q[T ] * undefined otherwise
Table 1. Typing rules for the deadlock-free (k = 0) and lock-free (k = 1) linear π-calculus.

Typing rules for expressions Γ e : t

[T-INT] Γ n : int un(Γ ) [T-NAME] Γ , u : T u T : T un(Γ )
Type combination is partial and is only defined when the combined types have the same structure. In particular, channel types can be combined only if they have equal message types; linear channel types can be combined only if they have disjoint polarities and equal level. Also, the combination of two channel types has the union of their polarities and, in the case of linear channels, the sum of their tickets. For example, a channel that is used both with type ?[int] 0 1 and with type ![int] 0 2 is used overall according to the type ?

[int] 0 1 + ![int] 0 2 = #[int] 0 3 .
Lastly, we define type environments Γ , . . . as finite maps from names to types written u 1 : T 1 , . . . , u n : T n . As usual, dom(Γ ) is the domain of Γ and Γ 1 , Γ 2 is the union of Γ 1 and Γ 2 when dom(Γ 1 ) ∩ dom(Γ 2 ) = / 0. We extend type combination to type environments:

Γ 1 + Γ 2 def = Γ 1 , Γ 2 if dom(Γ 1 ) ∩ dom(Γ 2 ) = / 0 (Γ 1 , u : T ) + (Γ 2 , u : S) def = (Γ 1 + Γ 2 ), u : T + S We let |Γ | def = min{|Γ (u)| | u ∈ dom(Γ )} be
the level of a type environment, we write un(Γ ) if |Γ | = and un(Γ ) if un(Γ ) and Γ has no top-level linear channel types. Note that un(Γ ) is strictly stronger than un(Γ ). For example, if

Γ def = x : int × / 0[int] 0 0 we have un(Γ ) but not un(Γ ) because Γ (x) has a top-level linear channel type.
The type systems for deadlock and lock freedom are defined by the rules in Table 1 deriving judgments Γ e : T for expressions and Γ k P for processes. The type system for deadlock freedom is obtained by taking k = 0, whereas the type system for lock freedom is obtained by taking k = 1 and restricting all levels in linear channel types to be non negative. We illustrate the typing rules as we work through the typing derivation of the replicated process in Example 2.1. The interested reader may refer to the implementation or [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] for more examples and detailed descriptions of the rules.

Let T and S be the types defined by the equations T = ![S] 0 0 × ?[S] 0 0 and S = ?[S] 1 1 . We build the derivation bottom up, from the judgment stating that the whole process is well typed. Since the process is a replicated input, we apply [T-IN*] thus:

c : ?[T ] * c : ?[T ] * c : ![T ] * , x : T 1 (νa)(fst(x)!a | snd(x)?(y).c!(a,y)) c : #[T ] * 1 *c?(x).(νa)(fst(x)!a | snd(x)?(y).c!(a,y))
In applying this rule we have

Γ 2 = c : ![T ] * so the side condition un(Γ 2 ) of [T-IN*]
is satisfied: since a replicated input process is permanently available, its body cannot contain any free linear channel except those possibly received through the unlimited channel. The side condition un(Γ 2 ), which is stronger than simply un(Γ 2 ), makes sure that a replicated input process does not contain linear channels and therefore is level polymorphic. We will see a use of this feature at the very end of the derivation. The continuation of the process gains visibility of the message x with type T and is a restriction of a linear channel a. Hence, the next step is an obvious application of [T-NEW]:

c : ![T ] * , x : T, a : #[S] 1 3 1 fst(x)!a | snd(x)?(y).c!(a,y) c : ![T ] * , x : T 1 (νa)(fst(x)!a | snd(x)?(y).c!(a,y)) (3.3)
We guess level 1 and 3 tickets for a. The rationale is that a is a continuation channel that will be used after the channels in x, which have level 0, so a must have strictly positive level. Also, in Example 2.1 the channel a travels three times. At this point the typing derivation forks, for we deal with the parallel composition of two processes. This means that we have to split the type environment in two parts, each describing the resources used by the corresponding subprocess in (3.3). We have Γ = Γ 1 + Γ 2 where

Γ def = c : ![T ] * , x : T, a : #[S] 1 3 Γ 1 def = x : ![S] 0 0 × / 0[S] 0 0 , a : ?[S] 1 2 Γ 2 def = c : ![T ] * , x : / 0[S] 0 0 × ?[S] 0 0 , a : ![S] 1 1
Observe that Γ is split in such a way that: c only occurs in Γ 2 , because it is only used in the right subprocess in (3.3); in each subprocess, the unused linear channel in the pair x is given empty polarity; the type of the continuation a has input polarity (and 2 tickets) in Γ 1 and output polarity (and 1 ticket) in Γ 2 . The type of a in Γ 1 is the same as $ 0 1 S, and we use the latter form from now on. We complete the typing derivation for the left subprocess in (3.3) using Γ 1 and applying [T-OUT]:

x : ![S] 0 0 × / 0[S] 0 0 fst(x) : ![S] 0 0 a : $ 0 1 S a : $ 0 1 S x : ![S] 0 0 × / 0[S] 0 0 , a : $ 0 1 S 1 fst(x)!a 0 < |$ 0 1 S| = 1
The side condition 0 < 1 ensures that the message has higher level than the channel on which it travels, according to the intuition that the message can only be used after the communication has occurred and the message has been received. In this case, the level of fst(x) is 0 that is smaller than the level of a, which is 1. Shifting the tickets from the type of a consumes one of its tickets, meaning that after this communication a gets closer to the point where it must be the subject of a communication.

Concerning the right subprocess in (3.3), we use Γ 2 above and apply [T-IN] to obtain

x : / 0[S] 0 0 × ?[S] 0 0 snd(x) : ?[S] 0 0 c : ![T ] * , a : ![S] 1 1 , y : S 1 c!(a,y) c : ![T ] * , x : / 0[S] 0 0 × ?[S] 0 0 , a : ![S] 1 1 1 snd(x)?(y).c!(a,y) 0 < 1
The side condition 0 < 1 checks that the level of the linear channel used for input is smaller than the level of any other channel occurring free in the continuation of the process. In this case, c has level because it is an unlimited channel with output polarity, whereas a has level 1. To close the derivation we must type the recursive invocation of c. We do so with an application of [T-OUT*]:

c : ![T ] * c : ![T ] * a : ![S] 1 1 , y : S (a,y) : $ 1 1 T c : ![T ] * , a : ![S] 1 1 , y : S 1 c!(a,y) ⊥ < 1
The side condition ⊥ < 1 ensures that no unlimited channel with input polarity is sent in the message. This is necessary to guarantee input receptiveness on unlimited channels. There is a mismatch between the actual type $ 1 1 T and the expected type T of the message. The shifting on the tickets is due, once again, to the fact that 1 ticket is required and consumed for the channels to travel. The shifting on the levels realizes a form of level polymorphism whereby we are allowed to send on c a pair of channels with level 1 even if c expects a pair of channels with level 0. This is safe because we know, from the side condition of [T-IN*], that the receiver of the message does not own any linear channel except those possibly contained in the message itself. Therefore, the exact level of the channels in the message is irrelevant, as long as it is obtained by shifting of the expected message type. Level polymorphism is a key distinguishing feature of our type systems that makes it possible to deal with non-trivial recursive processes.

Type reconstruction

We now face the problem of defining a type reconstruction algorithm for the type system presented in the previous section. The input of the algorithm is a process P where names are explicitly annotated with simple types, possibly resulting from a previous reconstruction stage [START_REF] Igarashi | Type reconstruction for linear π-calculus with I/O subtyping[END_REF][START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equi-recursive types[END_REF]. Notwithstanding such explicit annotations, the typing rules in Table 1 rely on guesses concerning (i) the splitting of type environments, (ii) levels and tickets that decorate linear channel types, and (iii) how tickets are distributed in combined types. We address these issues using standard strategies. Concerning (i), we synthesize type environments for expressions and processes by looking at the free names occurring in them. Concerning (ii) and (iii), we proceed in two steps: first, we transform each simple type t in P into a type expression T that has the same structure as t, but where we use fresh level and ticket variables in every slot where a level or a ticket is expected; we call this transformation dressing. Then, we accumulate (rather than check) the constraints that these level and ticket variables should satisfy, as by the side conditions of the typing rules (Table 1). Finally, we look for a solution of these constraints. It turns out that the accumulated constraints can always be expressed as an integer programming problem for which there exist dedicated solvers.

There is still a subtle source of ambiguity in the procedure outlined so far. We have remarked that stripping is a non-injective function, meaning that different types may be stripped to the same simple type. For example, if we take T = ?[T ] 1 1 and S = ?[T ] 0 0 we have T = S = s where s = ?[s]. Now, if we were to reconstruct either T or S from s, we would have to dress s with level and ticket variables in every slot where a level or a ticket is expected. But since s is infinite, such dressing is not unique. For example, T = ?[T] η 1 θ 1 and S = ?[T] η 2 θ 2 are just two of the infinitely many possible dressings of s with level and ticket variables: in T we have used two distinct variables η 1 and θ 1 , one for each slot; in S we have used four. The problem is that from the dressing T we can only reconstruct T , by taking η 1 = θ 1 = 1, whereas from the dressing S we can reconstruct both T (by assigning all variables to 1) as well as S, by taking η 1 = θ 1 = 1 and η 2 = θ 2 = 0. This means that the choice of the number of integer variables we use in dressing (infinite) simple types constrains the types that we can reconstruct from them, which is a risk for the completeness of the type reconstruction algorithms. To cope with this issue, we dress simple types lazily, only to their topmost linear channel constructors, and we put fresh type variables in place of message types, leaving them undressed. It is only when the message is used that we (lazily) dress its type as well. The introduction of fresh type variables for message types means that we redo part of the work already carried out for reconstructing simple types [START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equi-recursive types[END_REF]. This appears to be an inevitable price to pay to have completeness of the type reconstruction algorithms, when they build on top of (instead of being performed together with) previous stages.

To formalize the algorithms, we introduce countable sets of type variables α, β and of integer variables η, θ ; type expressions and integer expressions are defined below:

Type expression

T, S :

:= int | α | p[T] λ τ | p[T] * | T × S Integer expression λ , ε, τ ::= n | η | ε + ε | ε -ε
Type expressions differ from types in three ways: they are always finite, they have integer expressions in place of levels and tickets, and they include type variables α denoting unknown types awaiting to be lazily dressed. Integer expressions are linear polynomials of integer variables. We say that T is proper, written prop(T), if all the type variables in T are guarded by a channel constructor. For example, both int and p[α] * are proper (all type variables occur within channel types), but α and int × α are not. Since the level and tickets of a type expression are solely determined by its top-level linear channel constructors, properness characterizes those type expressions that are "sufficiently dressed" so that it is possible to extract their level and to combine them with other type expressions, even if these type expressions contain type variables.

We now revisit and adapt all the auxiliary operators and notions defined for types to type expressions. Recall that the level of T is the minimum level of any topmost linear channel type in T , or ⊥ if T has a topmost unlimited channel type with input polarity. Since a type expression T may contain unevaluated level expressions, we cannot compute a minimum level in general. However, a quick inspection of Table 1 reveals that minima of levels always occur on the right hand side of inequalities, and an inequality like n < min{m i | i ∈ I} can equivalently be expressed as a set of inequalities {n < m i | i ∈ I}. Following this observation, we define the level |T| of a proper type expression T as the set of level expressions that decorate the topmost linear channel types in T, and possibly the element ⊥. Formally:

|T| def =          {⊥} if T = p[S] * and ? ∈ p {λ } if T = p[S] λ τ and p = / 0 |T 1 | ∪ |T 2 | if T = T 1 × T 2 / 0 otherwise (4.1)
We write un(T) if |T| = / 0, in which case T denotes an unlimited type. Shifting for proper type expressions is defined just like for types, except that we symbolically record the sum of level/ticket expressions instead of computing it:

$ λ τ T def =      p[S] λ +λ τ+τ if T = p[S] λ τ ($ λ τ T 1 ) × ($ λ τ T 2 ) if T = T 1 × T 2 T otherwise (4.2)
Because type expressions may contain type and integer variables, we cannot determine a priori whether the combination of two type expressions is possible. For instance, the combination of ?[T] λ 1 τ 1 and ![S] λ 2 τ 2 is possible only if T and S denote the same type and if λ 1 and λ 2 evaluate to the same level. We cannot check these conditions right away, when T, S and the level expressions contain variables. Instead, we record these conditions into a constraint. Constraints ϕ, . . . are conjunctions of type constraints T = S (equality relations between type expressions) and integer constraints ε ≤ ε (inequality relations between integer expressions). Formally, their syntax is defined by

Constraint ϕ ::= true | T = T | ε ≤ ε | ϕ ∧ ϕ We write ε < ε in place of ε + 1 ≤ ε and ε = ε in place of ε ≤ ε ∧ ε ≤ ε; if E = {ε i } i∈I
is a finite set of integer expressions, we write ε < E for the constraint i∈I ε < ε i ; finally, we write dom(ϕ) for the set of type expressions occurring in ϕ.

The combination operator T S for type expressions returns a pair R; ϕ made of the resulting type expression R and the constraint ϕ that must be satisfied for the combination to be possible. The definition of mimics exactly that of + in Section 3, except that all non-checkable conditions accumulate in constraints:

T S def =                    int ; true if T = int and S = int (p ∪ q)[T ] λ τ+τ ; T = S ∧ λ = λ if T = p[T ] λ τ and S = q[S ] λ τ and p ∩ q = / 0 (p ∪ q)[T ] * ; T = S if T = p[T ] * and S = q[S ] * R 1 × R 2 ; ϕ 1 ∧ ϕ 2 if T = T 1 × T 2 and S = S 1 × S 2 and T i S i = R i ; ϕ i undefined otherwise
Like type combination, also is a partial operator: T S is undefined if T and S are structurally incompatible (e.g., if T = int and S = p[int] * ) or if T and S are not proper. When T S is defined, though, the resulting type expression is always proper.

We use ∆, . . . to range over type expression environments (or just environments, for short), namely finite maps from names to type expressions, and we inherit all the notation introduced for type environments. We let |∆| def = u∈dom(∆) |∆(u)| and write un(∆) if |∆| = / 0 and ∆ has no top-level linear channel type in its range. By now, the extension of to environments is easy to imagine: when defined, ∆ 1 ∆ 2 is a pair ∆; ϕ made of the resulting environment ∆ and of a constraint ϕ that results from the combination of the type expressions in ∆ 1 and ∆ 2 . More precisely:

∆ 1 ∆ 2 def = ∆ 1 , ∆ 2 ; true if dom(∆ 1 ) ∩ dom(∆ 2 ) = / 0 (∆ 1 , u : T) (∆ 2 , u : S) def = ∆, u : R ; ϕ ∧ ϕ if ∆ 1 ∆ 2 = ∆; ϕ and T S = R; ϕ
The last notion we need to formalize, before introducing the reconstruction algorithms, is that of dressing. Dressing a simple type t means placing fresh integer variables in the level/ticket slots of t. Formally, we say that T is a dressing of t if t ↑ T is inductively derivable by the following rules which pick globally fresh variables:

int ↑ int α fresh p[t] * ↑ p[α] * α, η, θ fresh p[t] ↑ p[α] η θ t i ↑ T i (i=1,2) t 1 × t 2 ↑ T 1 × T 2
Note that the decoration of t with fresh integer variables stops at the topmost channel types in t and that message types are left undecorated. By definition, the dressing of a simple type is always a proper type expression.

We can now present the type reconstruction algorithms, defined by the rules in Table 2. The rules in the upper part of the table derive judgments of the form e : T ∆; ϕ, stating that e has type T in the environment ∆ if the constraint ϕ is satisfied. The expression e is the only "input" of the judgment, while T, ∆, and ϕ are synthesized from it. There is a close correspondence between these rules and those for expressions in Table 1. Observe the use of where + was used in Table 1, the accumulation of constraints from the premises to the conclusion of each rule and, most notably, the dressing of the simple type that annotates u in [I-NAME]. Type expressions synthesized by the rules are always proper, so the side conditions in [I-FST] and [I-SND] can be safely checked.

The rules in the lower part of the table derive judgments of the form P k ∆; ϕ, stating that P is well typed in the environment ∆ if the constraint ϕ is satisfied. The parameter k plays the same role as in the type system (Table 1). The process P and the parameter k are the only "inputs" of the judgments, and ∆ and ϕ are synthesized from them. All rules except [I-WEAK] have a corresponding one in Table 1. Like for expressions, environments are combined through and constraints accumulate from premises to conclusions. We focus on the differences with respect to the typing rules.

In rule [T-IN], the side condition verifies that the level of the channel e on which an input is performed is smaller than the level of any channel used for typing the continuation process P. This condition can be decomposed in two parts: (1) no unlimited channel with input polarity must be in P; this condition is necessary to ensure input receptiveness on unlimited channels in the original type system [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] and is expressed in Reconstruction rules for processes ,2)

e i : T i ∆ i ; ϕ i (i=1,2) (e 1 ,e 2 ) : T 1 × T 2 ∆; 1≤i≤3 ϕ i ∆ 1 ∆ 2 = ∆; ϕ 3 [I-NAME]
P k ∆; ϕ [I-WEAK] P k ∆; ϕ P k ∆, u : T; ϕ un(T) prop(T) [I-IDLE] 0 k / 0; true [I-PAR] P i k ∆ i ; ϕ i (i=1
P 1 | P 2 k ∆; 1≤i≤3 ϕ i ∆ 1 ∆ 2 = ∆; ϕ 3 [I-IN] e : ?[T] λ τ ∆ 1 ; ϕ 1 P k ∆ 2 , x : S; ϕ 2 e?(x).P k ∆; 1≤i≤3 ϕ i ∧ T = $ -λ 0 S ∧ λ < |∆ 2 | ⊥ ∈ |∆ 2 | ∆ 1 ∆ 2 = ∆; ϕ 3 [I-OUT] e : ![T] λ τ ∆ 1 ; ϕ 1 f : S ∆ 2 ; ϕ 2 e!f k ∆; 1≤i≤3 ϕ i ∧ T = $ -λ -k S ∧ λ < |∆ 2 | ⊥ ∈ |∆ 2 | ∆ 1 ∆ 2 = ∆; ϕ 3 [I-NEW] P k ∆, a : #[T] λ τ ; ϕ (νa)P k ∆; ϕ [I-IN*] e : ?[T] * ∆ 1 ; ϕ 1 P k ∆ 2 , x : S; ϕ 2 *e?(x).P k ∆; 1≤i≤3 ϕ i ∧ T = S un(∆ 2 ) ∆ 1 ∆ 2 = ∆; ϕ 3 [I-OUT*] e : ![T] * ∆ 1 ; ϕ 1 f : S ∆ 2 ; ϕ 2 e!f k ∆; 1≤i≤3 ϕ i ∧ T = $ -η -k S ⊥ ∈ |∆ 2 | ∆ 1 ∆ 2 = ∆; ϕ 3 η fresh [I-NEW*] P k ∆, a : #[T] * ; ϕ (νa)P k ∆; ϕ

In [T-IN], [T-OUT], and [T-OUT*]

, shifting is used for updating message levels, consuming tickets, and realizing level polymorphism. In rules [I-IN], [I-OUT], and [I-OUT*], analogous shiftings are performed on type expressions, except that they are inverted and recorded in constraints. For example, when typing the continuation P of a process e?(x).P using [T-IN], if e has type ?[T ] n m then the type of x is required to be $ n 0 T . In the reconstruction algorithm, we record this requirement as the constraint T = $ -λ 0 S, where S is the type synthesized for x in P. We invert the shifting because shifting is defined only on proper type expressions, and in [I-IN] (and the other rules mentioned) only S is guaranteed to be proper, while T in general is not.

Finally, note that [I-WEAK] has no correspondent rule in Table 1. This rule is necessary because the premises of [I-IN], [I-IN*], [I-NEW], and [I-NEW*] assume that bound names occur in their scope. Since type environments are generated by the algorithm as it works through an expression or a process, this assumption may not hold if a bound name is never used in its scope. Naturally, the type T of an unused name must be unlimited, whence the constraint un(T). We also require T to be proper, to preserve the invariant that all environments synthesized by the algorithms have proper types. In principle, [I-WEAK] makes the rule set in Table 2 not syntax directed, which is a problem if we want to consider this as an algorithm. In practice, the places where [I-WEAK] may be necessary are easy to spot (in the premises of all the aforementioned rules for the binding constructs). What we gain with [I-WEAK] is a simpler presentation of the rules.

To state the properties of the reconstruction algorithm, we need a notion of constraint satisfiability. A variable assignment σ is a map from type/integer variables to types/integers. We say that σ covers X if σ provides assignments to all the type/integer variables occurring in X, where X may be a constraint, a type/integer expression, or an environment. When σ covers X, the application of σ to X, written σ X, substitutes all type/integer variables according to σ and evaluates all integer expressions in X. When σ covers ϕ, we say that σ satisfies ϕ if σ ϕ is derivable by the rules:

σ true σ T = S σ T = σ S σ ε ≤ ε σ ε ≤ σ ε σ ϕ i (i=1,2) σ ϕ 1 ∧ ϕ 2
Whenever we apply an assignment σ to a set of type expressions in reference to a derivation that is parametric on k, we will implicitly assume that all integer expressions in ticket slots evaluate to non-negative integers and that, if k = 1, all integer expressions in level slots evaluate to non-negative integers. The value of k and the set of type expressions will always be clear from the context.

The reconstruction algorithm is correct, namely each derivation obtained through the algorithm such that the resulting constraint is satisfiable corresponds to a derivation in the type system: Theorem 4.1 (correctness). If P k ∆; ϕ and σ ϕ and σ covers ∆, then σ ∆ k P.

The algorithm is also complete, meaning that if there exists a typing derivation for the judgment Γ k P, then the algorithm is capable of synthesizing an environment ∆ from which Γ can be obtained by means of a suitable variable assignment: Theorem 4.2 (completeness). If Γ k P, then P k ∆; ϕ for some ∆, ϕ, and σ such that σ ϕ and Γ = σ ∆.

Note that the above results do not give any information about how to verify whether there exists a σ such that σ ϕ and, in this case, how to find such σ . These problems will be addressed in Section 5. We conclude this section showing the reconstruction algorithm at work on the replicated process in Example 2.1.

![α 1 ] η 1 θ 1 × / 0[α 2 ] η 2 θ 2 ?[α 3 ] η 3 θ 3 α 1 = ?[α 3 ] η 3 -η 1 θ 3 -k ∧ η 1 < η 3 (2) ![α 4 ] * ![α 5 ] η 5 θ 5 ?[α 6 ] η 6 θ 6 α 4 = ![α 5 ] η 5 -η 4 θ 5 -k × ?[α 6 ] η 6 -η 4 θ 6 -k (3) / 0[α 7 ] η 7 θ 7 × ?[α 8 ] η 8 θ 8 α 8 = ?[α 6 ] η 6 -η 8 θ 6 ∧ η 8 < η 5 (4) ![α 1 ] η 1 θ 1 +θ 7 × ?[α 2 ] η 2 θ 2 +θ 8 #[α 3 ] η 3 θ 3 +θ 5 α 1 = α 7 ∧ α 2 = α 8 ∧ α 3 = α 5 ∧ η 1 = η 7 ∧ η 2 = η 8 ∧ η 3 = η 5 (5) #[α 9 ] * α 9 = ![α 1 ] η 1 θ 1 +θ 7 × ?[α 2 ] η 2 θ 2 +θ 8 ∧ α 9 = α 4
Table 4. Constraint entailment rules.

[S-LEVEL]

ϕ 1 0 ≤ λ p[T] λ τ ∈ dom(ϕ) [S-TICKET] ϕ k 0 ≤ τ p[T] λ τ ∈ dom(ϕ) [S-CONJ] ϕ 1 ∧ ϕ 2 k ϕ i i ∈ {1, 2} [S-SYMM] ϕ k T = S ϕ k S = T [S-TRANS] ϕ k T = R ϕ k R = S ϕ k T = S [S-CHAN] ϕ k p[T] λ 1 τ 1 = p[S] λ 2 τ 2 ϕ k T = S ∧ λ 1 = λ 2 ∧ τ 1 = τ 2 [S-CHAN*] ϕ k p[T] * = p[S] * ϕ k T = S [S-PAIR] ϕ k T 1 × T 2 = S 1 × S 2 ϕ k T 1 = S 1 ∧ T 2 = S 2
Each subprocess triggers one rule of the reconstruction algorithm which synthesizes a type environment and possibly generates some constraints. Table 3 summarizes the parts of the environments and the constraints produced at each step of the reconstruction algorithm with parameter k. We have omitted the step concerning the restriction on a, which just removes a from the environment and introduces no constraints.

Constraint solving

We sketch an algorithm that determines whether a constraint ϕ is satisfiable and, in this case, computes an assignment that satisfies it. The presentation is somewhat less formal since the key steps of the algorithm are instances of well-known techniques. The algorithm is structured in three phases, saturation, verification, and synthesis.

The constraint ϕ produced by the reconstruction algorithm does not necessarily mention all the relations that must hold between integer variables. For example, the constraint η 3η 1 = η 6η 8 ∧ θ 3k = θ 6 is implied by those in Table 3, but it appears nowhere. Finding all the integer constraints entailed by a given ϕ, regardless of whether such constraints are implicit or explicit, is essential because we use an external solver for solving them. The aim of the saturation phase is to find all such integer constraints. Table 4 defines an inference system for deriving entailments ϕ k ϕ . The parameter k plays the same role as in the type system. Rules [S-LEVEL] and [S-TICKET] introduce nonnegativity constraints for integer expressions that occur in level and ticket slots; level expressions are required to be non-negative only for lock freedom analysis, when k = 1; rule [S-CONJ] decomposes conjunctions; rules [S-SYMM] and [S-TRANS] compute the symmetric and transitive closure of type equality; finally, [S-CHAN], [S-CHAN*], and [S-PAIR] state expected congruence rules. We let ϕ def = ϕ k ϕ ϕ . Clearly ϕ can be computed in finite time and is satisfiable by the same assignments as (i.e., it is equivalent to) ϕ.

The verification phase checks whether ϕ is satisfiable and, in this case, computes an assignment σ int that satisfies the integer constraints in it. In ϕ all the integer constraints are explicit. These are typical constraints of an integer programming problem, for which it is possible to use dedicated (complete) solvers that find a σ int when it exists (our tool supports GLPK3 and lpsolve4 ). When this is the case, the type constraints in ϕ are satisfiable if, for each type constraint of the form T = S, either T or S are type variables, or T and S have the same topmost constructor, i.e. they are either both int, or both unlimited/linear channel types with the same polarity, or both product types.

The synthesis phase computes an assignment that satisfies ϕ. This is found by applying σ int to all the type constraints in ϕ, by choosing a canonical constraint of the form α = T where T is proper for each α ∈ dom( ϕ), and then by solving the resulting system {α i = T i } of equations. By [4, Theorem 4.2.1], this system has exactly one solution σ type and now σ int ∪ σ type ϕ. There may be type variables α for which there is no α = T constraint with T proper. These type variables denote values not used by the process, like a message that is received from one channel and just forwarded on another one. These variables are assigned a type that can be computed canonically.

Example 5.1. The constraints shown in Table 3 entail 0 ≤ θ 3k and 0 ≤ θ 5k and 0 ≤ θ 6 -k namely k ≤ θ 3 and k ≤ θ 5 and k ≤ θ 6 must hold. When k = 0, these constraints can be trivially satisfied by assigning 0 to all ticket variables. When k = 1, from the type of a at step (4) of the reconstruction algorithm we deduce that a must have at least 2 tickets. Indeed, a is sent in two messages. It is only considering the remaining processes c!(e, f ) and c!( f ,e) that we learn that y is instantiated with a. Then, a needs one more ticket, to account for the further and last travel in the recursive invocation c!(a,y).

Concluding remarks

A key distinguishing feature of the type systems in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] is the use of polymorphic recursion. Type reconstruction in presence of polymorphic recursion is notoriously undecidable [START_REF] Kfoury | Type reconstruction in the presence of polymorphic recursion[END_REF][START_REF] Henglein | Type inference with polymorphic recursion[END_REF]. In our case, polymorphism solely concerns levels and reconstruction turns out to be doable. A similar situation is known for effect systems [START_REF] Amtoft | Type and effect systems: behaviours for concurrency[END_REF], where polymorphic recursion restricted to effects does not prevent complete type reconstruction [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF].

We have conducted some benchmarks on generalizations of Example 2.1 to Ndimensional hypercubes of processes using full-duplex communication. The table below reports the reconstruction times for the analysis of an hypercube of side 5 and N varying from 1 to 4. The table details the dimension, the number of processes and channels, and the times (in seconds) spent for linearity analysis [START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equi-recursive types[END_REF], constraint generation (Section 4) and saturation, solution of level and ticket constraints (Section 5). The solver used for level and ticket constraints is GLPK 4.48 and times were measured on a 13" MacBook Air running a 1.8 GHz Intel Core i5 with 4 GB of 1600MHz DDR3. Reconstruction times scale almost linearly in the number of channels as long as there is enough free main memory. With N = 4, however, the used memory exceeds 10GB causing severe memory (de)compression and swapping. The running time inflates consequently. We have not determined yet the precise causes of such disproportionate consumption of memory, which the algorithms do not seem to imply. We suspect that they are linked to our naive implementation of the algorithms in a lazy language (Haskell), but a more rigorous profiling analysis is left for future investigation. Integer programming problems are NP-hard in general, but the time used for integer constraint resolution appears negligible compared to the other phases. As suggested by one reviewer, the particular nature of such constraints indicates that there might be more clever way of solving them, for example by using SMT solvers.

Our work has been inspired by previous type systems ensuring (dead)lock freedom for generic π-calculus processes [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] and corresponding type reconstruction algorithms [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF]. These type systems and ours are incomparable: [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] use sophisticated behavioral types that provide better accuracy with respect to unlimited channels as used for modeling mutual exclusion and concurrent objects. On the other hand, our type systems exploit level polymorphism for dealing with recursive processes in cyclic topologies, often arising in the modeling of parallel algorithms and sessions. Whether and how the strengths of both approaches can be combined together is left for future research. A more thorough comparison between these works can be found in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF].

There is a substantial methodological difference between our approach and those addressing sessions, particularly multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF]. Session-based approaches are top down and type driven: types/protocols come first, and are used as a guidance for developing programs that follow them. These approaches guarantee by design a number of properties, among which (dead)lock freedom when different sessions are not interleaved. Our approach is bottom up and program driven: programs come first, and are used for inferring types/protocols. The two approaches can integrate and complement each other. For example, type reconstruction may assist in the verification of legacy or third-party code (for which no type information is available) or for checking the impact of code changes due to refactoring and/or debugging. Also, some protocols are hard to describe a priori. For example, describing the essence of full-duplex communications (Example 2.1) is far from trivial [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF]. In general, processes making use of channel mobility (delegation) and session interleaving, or dynamic network topologies with variable number of processes, are supported by our approach (within the limits imposed by the type systems), but are challenging to handle in top-down approaches. Inference of progress properties akin to lock freedom for session-based calculi has been studied in [START_REF] Mezzina | How to infer finite session types in a calculus of services and sessions[END_REF][START_REF] Coppo | Inference of global progress properties for dynamically interleaved multiparty sessions[END_REF], although only finite types are considered in these works.

The reconstruction of global protocol descriptions from local session types has been studied in [START_REF] Lange | Synthesising choreographies from local session types[END_REF][START_REF] Lange | From communicating machines to graphical choreographies[END_REF]. In this respect, our work fills the remaining gap and provides a reconstruction tool from processes to local session types. We plan to investigate the integration with [START_REF] Lange | Synthesising choreographies from local session types[END_REF][START_REF] Lange | From communicating machines to graphical choreographies[END_REF] in future work.

Example 2 . 1 (

 21 full duplex communication). The term *c?(x).(νa)( fst(x)!a | snd(x)?(y).c!(a,y) ) | c!(e, f ) | c!( f ,e)

  [I-IN] as the side condition ⊥ ∈ |∆ 2 |, which can be checked on type expressions environments directly; (2) the level of e must satisfy the ordering with respect to all the linear channels in P; this is expressed in [I-IN] as the constraint λ < |∆ 2 |, where λ is the level of e. The same side condition and constraint are found in [I-OUT].

  u t : T u : T; true t ↑ T [I-FST] e : T × S ∆; ϕ fst(e) : T ∆; ϕ un(S) [I-SND] e : T × S ∆; ϕ snd(e) : S ∆; ϕ un(T)

Example 4 . 1 .

 41 Below is the replicated process in Example 2.1, where we have numbered and named the relevant rules used by the algorithm as it visits the process bottom-up, left-to-right: *c?(x).(νa)(fst(x)!a | snd(x)?(y).c!(a,y)) (1) [I-OUT] (2) [I-OUT*] (3) [I-IN] (4) [I-PAR] (5) [I-IN*]

Table 2 .

 2 Type reconstruction rules for expressions and processes.

	Reconstruction rules for expressions	e : T ∆; ϕ
	[I-INT]	[I-PAIR]
	n : int / 0; true

Table 3 .

 3 Type environment and constraints generated for the process in Example 2.1.

	i	c	x	a	y	Constraint
	(1)

N

  Processes Channels Linearity Gen.+Sat. Levels Tickets Overall

	1	5	8	0.021	0.006 0.002 0.003 0.032
	2	25	80	0.128	0.051 0.009 0.012 0.200
	3	125	600	1.439	0.844 0.069 0.124 2.477
	4	625	4000	33.803	26.422 1.116 3.913 65.254

[T-PAIR]Γ i e i : T i (i=1,2)Γ 1 + Γ 2 (e 1 ,e 2 ) : T 1 × T 2 [T-FST] Γ e : T × S Γ fst(e) : T un(S) [T-SND]Γ e : T × S Γ snd(e) : S un(T )Typing rules for processesΓ k P [T-IN] Γ 1 e : ?[T ] n m Γ 2 , x : $ n 0 T k P Γ 1 + Γ 2 k e?(x).P n < |Γ 2 | [T-OUT] Γ 1 e : ![T ] n m Γ 2 f : $ n k T Γ 1 + Γ 2 k e!f n < |Γ 2 | [T-IN*]Γ 1 e : ?[T ] * Γ 2 , x :T k P Γ 1 + Γ 2 k *e?(x).P un(Γ 2 ) [T-OUT*] Γ 1 e : ![T ] * Γ 2 f : $ n k T Γ 1 + Γ 2 k e!f ⊥ < |Γ 2 | [T-IDLE] Γ k 0 un(Γ ) [T-PAR] Γ 1 k P Γ 2 k Q Γ 1 + Γ 2 k P | Q [T-NEW] Γ , a : #[T ] m n k P Γ k (νa)P [T-NEW*]Γ , a : #[T ] * k P Γ k (νa)P

http://www.gnu.org/software/glpk/

http://sourceforge.net/projects/lpsolve/

Acknowledgments. The authors are grateful to the reviewers for their detailed comments and useful suggestions. The first two authors have been supported by Ateneo/CSP project SALT. The first author has also been supported by ICT COST Action IC1201 BETTY and MIUR project CINA.


Francesco L De Angelis
email: francesco.deangelis@unige.ch

Giovanna Di
email: giovanna.dimarzo@unige.ch

Marzo Serugendo

Logic Fragments: a coordination model based on logic inference

Chemical-based coordination models have proven useful to engineer self-organising and self-adaptive systems. Formal assessment of emergent global behaviours in self-organising systems is still an issue, most of the time emergent properties are being analysed through extensive simulations. This paper aims at integrating logic programs into a chemical-based coordination model in order to engineer self-organising systems as well as assess their emergent properties. Our model is generic and accommodates various logics. By tuning the internal logic language we can tackle and solve coordination problems in a rigorous way, without renouncing to important engineering properties such as compactness, modularity and reusability of code. This paper discusses our logic-based coordination model and shows how to engineer and verify a simple pattern detection example and a gradient-chemotaxis example.

Introduction

Coordination models have been proven useful for designing and implementing distributed systems. They are particularly appealing for developing self-organising systems, since the shared tuple space on which they are based is a powerful paradigm to implement self-organising mechanisms, particularly those requiring indirect communication (e.g. stigmergy) [START_REF] Viroli | A framework for modelling and implementing self-organising coordination[END_REF]. Chemical-based coordination models are a category of coordination models that use the chemical reaction metaphor and have proven useful to implement several types of self-organising mechanisms [START_REF] Zambonelli | Developing pervasive multiagent systems with nature-inspired coordination[END_REF]. A well-known difficulty in the design of self-organising systems stems from the analysis, validation and verification (at design-time or run-time) of so-called emergent properties -i.e. properties that can be observed at a global level but that none of the interacting entities exhibit on its own. Few coordination models integrate features supporting the validation of emergent properties, none of them relying on the chemical metaphor.

In this paper, we propose to enrich a chemical-based coordination model with the notion of Logic Fragments (i.e. a combination of logic programs). Our logic-based coordination model allows agents to inject Logic Fragments into the shared space. Those fragments actually define on-the-fly ad hoc chemical reactions that apply on matching data tuples present in the system, removing tuples and producing new tuples, possibly producing also new Logic Fragments. Our model is defined independently of the logic language used to define the syntax of the Logic Fragment, an actual instantiation and implementation of the model can use its own logic(s). The advent of new families of logic languages (e.g. [START_REF] Vitória | Modeling and reasoning in paraconsistent rough sets[END_REF]) has enriched the paradigm of logic programming, allowing, among other things, practical formalisation and manipulation of data inconsistency, knowledge representation of partial information and constraints satisfaction. By combining those logics with a chemical-based coordination model, we argue that global properties can be verified at design time.

Section 2 discusses related works, section 3 presents our logic-based coordination model. Section 4 shows two case studies: a simple pattern recognition example and another one with the gradient and chemotaxis patterns. Finally, section 5 concludes the paper.

Related works

Chemical-based coordination models

An important class of coordination models is represented by so-called chemical-based coordination models, where "chemical" stands for the process of imitating the behaviours of chemical compounds in chemical systems.

Gamma (General Abstract Model for Multiset mAnipulation) [START_REF] Banâtre | The gamma model and its discipline of programming[END_REF] and its evolutions historically represents an important chemical-inspired coordination model. The core of the model is based on the concept of virtual chemical reactions expressed through condition-action rewriting pairs. Virtual chemical reactions are applied on input multisets which satisfy a condition statement and they produce as output multisets where elements are modified according to the corresponding action (like for chemical compounds); the execution of virtual chemical reactions satisfying a condition pair is nondeterministic. Gamma presents two remarkable properties: (i) the constructs of the model implicitly support the definition of parallel programs; (ii) the language was proposed in the context of systematic program derivation and correctness as well as termination of programs is easy to prove ( [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]). Its major drawback is represented by the complexity of modeling real large applications.

The SAPERE model [START_REF] Castelli | Pervasive middleware goes social: The sapere approach[END_REF] (Figure 1a) is a coordination model for multiagent pervasive systems inspired by chemical reactions. It is based on four main concepts: Live Semantic Annotations (LSAs), LSA Tuple Space, agents and eco-laws. LSAs are tuples of types (name, value) used to store applications data. For example, a tuple of type (date, 04/04/1988) can be used to define a hypothetical date. LSAs belonging to a computing node are stored in a shared container named LSA Tuple Space. Each LSA is associated with an agent, an external entity that implements some domainspecific logic program. For example, agents can represent sensors, services or general applications that want to interact with the LSA space -injecting or retrieving LSAs from the LSA space. Inside the shared container, tuples react in a virtual chemical way by using a predefined set of coordination rules named eco-laws, which can: (i) instantiate relationships among LSAs (Bonding eco-law); (ii) aggregate them (Aggregate eco-law); (iii) delete them (Decay eco-law) and (iv) spread them across remote LSA Tuples Spaces (Spreading eco-law). Spontaneous executions of ecolaws can be fired when specific commands (named operators) are present in tuple values. When a tuple is modified by an eco-law, its corresponding agent is notified: in this way, agents react to virtual chemical reactions according to the program they implement. The implementation of the SAPERE model, named SAPERE middleware, has been proven to be powerful enough and robust to permit the development of several kinds of real distributed self-adaptive and self-organising applications, as reported in [START_REF] Zambonelli | Developing pervasive multiagent systems with nature-inspired coordination[END_REF]. Nevertheless, the model does not aim at proving correctness or emergence of global properties programs built on it: this means that proving correctness of applications may turn to be a complex task.

Formal approaches for tuple based coordination models

Coordination models based on tuple spaces are amenable to several kinds of analytical formalisation.

PoliS [START_REF] Ciancarini | A coordination model to specify systems including mobile agents[END_REF] is a coordination model based on multiset rewriting in which coordination rules consume and produce multisets of tuples; rules are expressed in a Chemical Abstract Machine style [START_REF] Berry | The chemical abstract machine[END_REF]. In PoliS, properties can be proved by using the PoliS Temporal Logic and the PoliMC model checker.

Tuples centres [START_REF] Omicini | From tuple spaces to tuple centres[END_REF] allow the use of a specification language (named RespecT) to define computations performed in the tuple space. Computations are associated with events triggered internally because of reactions previously fired or during the execution of traditional input/output operations by agents. RespecT is based on first-order logic and unification of unitary clauses (tuple templates) and ground atoms (tuples) represent the basic tuple matching mechanism.

In the ACLT model [START_REF] Denti | Logic tuple spaces for the coordination of heterogeneous agents[END_REF], the tuple space is treated as a container of logic theories, which can be accessed by logic agents to perform deduction processes. Again, the first-order logic and unification of unitary clauses and ground atoms is used as matching mechanism; the model offers specific input-output primitives tailored to provide different meaning for unification by allowing a certain control in selecting the set of unitary clauses to be treated as facts in case of backtracks or temporary missing information in the deduction process.

In our model we do not express coordination in terms of rewriting rules; moreover, the logic layer is enhanced by considering several types of logic languages.

3 Logic-and chemical-based coordination model

Definition of the model

The chemical-based coordination model we present in this paper is designed to exploit several important features of the models cited above in the context of self-organising and self-adaptive applications; our goal is to define a coordination model with the following characteristics: (i) coordination algorithms can be described in an sufficiently abstract way starting from high-level specifications; (ii) the constructs used to express coordination algorithms are amenable to formal analysis of their correctness, they incentivize the decoupling of logic from implementation and they meet software engineering properties such as modularity, reusability and compactness. The rationale leading the definition of our coordination model can be synthesized as the adoption of Kowalski's terminology [START_REF] Kowalski | Algorithm = logic + control[END_REF]: algorithm = logic + control. This formulation promotes the dichotomy of algorithms in: (i) logic components (formulae) that determine the meaning of the algorithm, the knowledge used to solve a problem (i.e. what has to be done) and (ii) control components, which specify the manner the knowledge is used (i.e. how it has to be done).

The coordination model we define (Figure 1b) is a generalization of the SAPERE model with two additional features: (i) LSAs can store not only data tuples but actual logic programs (Section 3.2); (ii) the bonding eco-law is replaced by a new one named Logic eco-law, which is in charge of executing logic programs and performing the bonding actions. The remaining components of the model are exactly the same as the ones of the SAPERE model. The virtual chemical reactions among tuples taking place in the shared container are now driven by logic inferences processes, which produce either data tuples or new logic programs during the "execution" of logic programs (Figure 1c). This process brings the idea promulgated by [START_REF] Kowalski | Algorithm = logic + control[END_REF] in the context of chemical-based coordination models: the logic components of an algorithm are expressed in terms of logic programs, here embedded in LSAs, which can react among each other in a chemical fashion. Similarly, agents implement the control components (written in a programming language such as Java), and they perform computations according to the knowledge inferred by logic programs. This approach to separation and mapping of concepts helps designing coordination algorithms from an abstract point of view. On the one hand, algorithms are thought as interactions of atomic logic entities which define the meaning (in Kowalski's terminology) of subparts of the original algorithm. On the other hand, once logic entities have been defined, a specific problem-solving strategy can be chosen to be implemented for each subpart of the original problem. The intuition of using logic programs is twofold: (i) tuples exchanges represent the basic mechanism to carry out indirect communication among agents, thus the state and the evolution of a coordination process can be defined by analysing the set of tuples in the containers; (ii) tuples are used as inputs (facts) and produced as outputs of logic programs (models and formulae obtained by resolution rules). By considering points (i) and (ii), logic programs provide a natural formal tool to express coordination, allowing for inferred formulae to state relationships among entities of the system, depicting the evolution of coordination processes and proving system properties.

Logic programs

Logic programs [START_REF] Nilsson | Logic, Programming, and PROLOG[END_REF] are sets of logic formulae and are expressed in a logic language (e.g. first-order logic). Executing a logic program means either: (i) providing queries to the program and testing whether they logically follow from the program by using a proof engine (logic inference) or (ii) inferring all sentences that logically follow from the program (logic semantics). An interpretation of a formal language is an interpretation (see [START_REF] Nilsson | Logic, Programming, and PROLOG[END_REF]) of constants, predicate and functions of the language over a given domain. The truth-value of a logic sentence is determined by the interpretation of the logic connectives. Given a logic program P , a model is an interpretation M such that every formula in P is true (depicted as M |= P ). Here we are interested in Herbrand interpretations ( [START_REF] Nilsson | Logic, Programming, and PROLOG[END_REF]): (i) the implicit domain is the Herbrand Universe, the closure of the set of constants under all the functions symbols of the language; (ii) constants are interpreted as themselves and every function symbol as the function it refers to. In classical 2-valued logic programs, Herbrand interpretation can be defined through sets of atoms implicitly interpreted as true.

Example: [START_REF] Nilsson | Logic, Programming, and PROLOG[END_REF]. Clauses are implicitly universally quantified. This is a definite logic program (i.e. containing Horn clauses): x is a variable, c is a constant and here they range over an (implicitly) defined domain.

P = (C(x) ← A(x), B(x); A(c) ← ; B(c) ← ; ) is a defin- ite logic program
The first rule is composed of the head C(X) and the body A(X), B(X) and it can be read as "C(X) is true if both A(X) and B(X) are true". Rules with empty bodies ( ) are named facts and they state sentences whose heads must be considered satisfied; in this case A(c) and B(c) hold. M = {A(c), B(c), C(c)} is a model for the program in the example, because it satisfies all the rules.

Logic languages

In our model, logic programs are executed by the Logic eco-law. An important point in our approach is the generality of the coordination model w.r.t. the logic. We consider only logic languages that support Herbrand's interpretations, whereas we do not put any constraint on the inference methods or the semantics. Both inference methods and semantics are treated as parameters associated with logic programs. From the practical point of view, for each logic language we require the implementation of a dedicated Logic eco-law that executes the corresponding logic programs. This feature makes possible to use, possibly simultaneously: (i)

Logic Fragments

In our model, logic programs are embedded in logic units named Logic Fragments. The following set of definitions will be used to clarify the concept. We assume that P rop, Const and V ar are finite mutually disjoint sets of relation symbols, constants and variables respectively. We will identify variables with letters x, y, . . . and constants with letters a, b, . . . . Definition 1 (Literals, Ground Literals): A literal P is an expression of type P (X 1 , . . . , X n ) or ¬P (X 1 , . . . , X n ) where P ∈ P rop and X i ∈ (Const ∪ V ar) for i = 1, . . . , n. A ground literal is a literal without variables. The set of all ground literals w.r.t. a set Const is denoted G(Const). The power set of G(Const) is depicted P(G). Definition 2 (Valuations): A valuation w is a function from V ar to Const that assigns a constant c i to each variable x i . The set of all possible valuations is depicted as W = {w|w : V ar → Const}. Definition 3 (Instances of Literal): If P is a literal and w is a valuation, with Pw we identify the ground literal where every variable of P has been replaced by a constant according to the definition of w. Pw is named an instance of P . We denote

I P = { Pw |w ∈ W} ⊆ G(Const).
Definition 4 (Logic Programs): A logic program is a set of logic formulae written in a logic language using: (i) literals P1 , ..., Pn defined over P rop, Const, V ar and (ii) logic operators. Definition 5 (A-generator): Given a literal P (X 1 , . . . , X n ), an A-generator w.r.t. a function U : Const n → {T, F } is the finite set:

P U (X 1 , . . . , X n ) = {P (c 1 , . . . , c n ) ∈ I P (X 1 ,...,Xn) |U (c 1 , . . . , c n ) = T }. Example: A U (X) = {A(X)|X ∈ {a, b, c}} = {A(a), A(b), A(c)}, with U (a) = U (b) = U (c) = T .
Definition 6 (I-generator): Given a literal P (X 1 , . . . , X n ), an I-generator w.r.t a function V : P(G) → P(G) and a finite set H ⊆ P(G) is the set:

P H,V (X 1 , . . . , X n ) = {P (c 1 , . . . , c n ) ∈ I P (X 1 ,...,Xn) ∩ V (H)} If V is omitted, we assume that V (H) = H (identity function). Example: if N = {2, 3, 4} and V (N ) = {Even(x)|x ∈ N ∧x is even}, then Even N,V (X) = {Even(2), Even(4)}.
The rationale of such definitions is to provide the program with a set of facts built from conditions holding on tuples stored in the container. The unfolding of these generators produces new facts for the interpretation of the logic program.

By LF we identify the algebraic structure of Logic Fragments, recursively defined as follows: is a special symbol used only in Logic Fragments to depict all the tuples in the container (both LSAs and Logic Fragments). M is the identifier of the way P is "executed" (we will use M = A for the Apt-van Emden-Kowalski and M = K for the Kripke-Kleen semantics). e P is named constituent of the Logic Fragment and it is interpreted as a set of tuples used as support to generate the facts for the program. S is a set of A,I-generators used to derive new facts from P . The function ϕ : P(G) → {T, F } returns T if the tuples represented by the constituent e p satisfy some constraints; the logic program is executed if and only ϕ(e P ) = T (Def. 8). ϕ T is constant and equal to T . For style reason, we will write P M (e P , S, ϕ) instead of (P, M, e P , S, ϕ). Every Logic Fragment is executed by the Logic eco-law; its semantics is defined by using the function v L . Definition 8 (Semantic function): v L : LF → P(G) ∪ { } associates the fragment with the set of tuples inferred by the logic program (consequent) or with , which stands for undefined interpretation. L denotes the set of actual tuples in the container before executing a Logic Fragment. Operators are ordered w.r.t. these priorities: grouping (highest priority), composition, and (lowest priority). v L is recursively defined as follows:

I) v L ( ) L II) v L (e) v L (e) III) v L e 1 ... e n n≥2 if ∃i ∈ {1, . . . , n}.v L e i = n i=1 v L e i otherwise IV) v L e 1 ... e n n≥2 i∈I v L e i if I = {e i |v L (e i ) = , 0 ≤ i ≤ n} = ∅ otherwise V) v L P M (e P , S, ϕ) Q
Q is the consequent of P M and it is defined as follows: if M is not compatible with the logic program P or if v L (e p ) = or if ϕ v L (e p ) = F then Q = . ϕ "blocks" the execution of the program as long as a certain condition over e p is not satisfied. Otherwise, based on S = {P H 0 ,V 0 0 (X 01 , ..., X 0t 0 ), ..., P Hn,Vn n (X n1 , ..., X ntn ), P 0 (Y 01 , ..., Y 0z 0 ), ... P m (Y m1 , ..., Y mzm )}, the Logic eco-law produces the set of facts F s =

n i=0 P v L (H i ),V i i (X i1 , . . . , X it i ) ∪ m i=0 P i (Y i1 , . . . , Y iz i ).
A,I-generators are then used to define sets of ground literals for the logic program which satisfy specific constraints; during the evaluation, for every set H i we have either H i = e p or H i = . Q is finally defined as the set of atoms inferred by applying M on the new logic program P = P ∪ {l ← |l ∈ F s}, enriched by all the facts contained in F s. Note that there may be no need to explicitly calculate all the literals of A,I-generators beforehand: the membership of literals to generators sets may be tested one literal at a time or skipped because of the short-circuit evaluation. Intuitively, composing two Logic Fragments means calculating the inner one first and considering it as constituent for the computation of the second one. Parallel-and ( ) means executing all the Logic Fragments them in a row or none, whereas Parallel-or ( ) means executing only those ones that can be executed at a given time.

Update of the container

In our model, all the Logic Fragments are carried on a snapshot image of the container, i.e. given a Logic Fragment e in the container, if v L (e) = , then it is evaluated as an atomic operation (every symbol in the sub Logic Fragments which composes e is always translated with the same set of actual tuples). Multiple Logic Fragments ready to be evaluated are computed in a non-deterministic order. The tuples inferred by the logic programs (with all used facts) are inserted in the container only when the evaluation of the whole logic program terminates. At that point, the Logic eco-law injects the inferred tuples in the container and notifies the end of inference process to the agent. The Logic Fragment is subject to a new evaluation process as soon as the set F s changes due to updates of the shared container, but there are no concurrent parallel evaluations of the same Logic Fragment at a given time (unless it appears twice); this aspect can potentially hide tuples updates in the evaluation process (Section 5). The representation of the functions associated with A,I-generators depends on the implementation.

Case studies

By using Logic Fragments we can easily tackle interesting coordination problems and properties. Additional examples are reported in [START_REF] De Angelis | Towards a logic and chemical based coordination model[END_REF].

Palindrome recognition

As a first example we show an easy pattern recognition scenario. Assuming that an agent A inserts positive integers into the container, we want to discover which ones are palindromic numbers (i.e. numbers that can be read in the same way from left to right and from right to left). We assume that these integers are represented by tuples of type N (a), where a is a number, e.g. N (3) represents the number 3. Agent A inserts the Logic Fragment LF p : P A p ( , {N , T estP alin}, ϕ p ). P p is the logic program in Code 1.1, evaluated with the Apt-van Embden Kowalski semantics (A). The set S of A,I-generators is composed of two elements: N contains all literals N (a) (numbers) existing in the container ( ); T estP alin(x) contains all the literals of type T estP alin(a), where a is a positive palindromic number less then d max . These two sets of literals are treated as facts for P p . According to ϕ, P p is executed as soon as a number N (a) is inserted into the container. The rule of the logic program P p states that a number a is a palindromic number (P alin(a)) if a is a number (N (a)) and a passes the test for being palindromic (T estP alin(a)). We consider the tuple space shown in Figure 2a and2b. At the beginning, agent A injects LF p (Figure 2a). At a later stage A injects N (22) and the Logic Fragment is then executed. In this case, N is evaluated as {N (22)}. Moreover, T estP alin(a) will contain T estP alin(22), because it is palindromic. This means the consequent Q of LF p contains P alin(22), along with all the facts generated by the A,I-generators used in the logic program. If now agent A injects N (12), the Logic Fragment is re-executed and N is evaluated as {N (22), N (12)}. This second number does not satisfy the palindromic test (N (12) ∈ T estP alin(x)), so the 12 will not be considered as palindromic. Finally A injects N (414) and during the re-execution of LF p we obtain: N = {N (22), N (12), N (414)} and N (414) ∈ T estP alin(x), so the consequent Q will contain P alin(22) and P alin(414) (Figure 2b). Note that if numbers were injected by agents different from A (like a sensor), the same reactions would take place. Proof sketch: The property above states that by using the Logic Fragment LF p we are able to correctly find out all the palindromic integers. Thanks to the logic programs and the semantic of Logic Fragments, we can easily verify that if such integers exist in the container then their literals are inferred in Herbrand model of P p . Moreover, given that such literals are only generated by LF p , if such literals exist in the model then there must be the associated palindromic integers in the shared space.

Gradient and Chemotaxis patterns -general programs

In this second example we use Logic Fragments to implement the gradient and chemotaxis design patterns ( [START_REF] Fernandez-Marquez | Description and composition of bio-inspired design patterns: a complete overview[END_REF]), which are two bio-inspired mechanisms used to build and follow shortest paths among nodes in a network.

The chemotaxis is based on the gradient pattern. A gradient is a message spread from one source to all the nodes in the network, carrying a notion of distance from the source (hop-counter). Gradient messages can also carry user-information. Once a node receives a gradient from a known source whose hop-counter is less than the local one (i.e. a new local shortest-path has been found), the node updates its local copy of the hopcounter (aggregation) and spreads it towards the remaining neighbours with a hop-counter incremented by one unit. In these terms, the gradient algorithm is similar to the distance-vector algorithm. The chemotaxis pattern resorts to gradient shortest-paths to route messages towards the source of the gradient. We can implement the gradient and chemotaxis patterns by using an agent A gc associated with the Logic Fragment: , where a and c are as above and e is the previous node in the path, this will be used to route the chemotaxis message downhill towards the source. LF gc is composed of several Logic Fragments; the parallel-or operator makes the agent A gc to react simultaneously to chemotaxis and gradients messages. The innermost fragment e Pa = P K n ( , S n , ϕ n ) is executed when a gradient message is received from a neighbour ( can be executed directly but the parallel-and operator blocks the execution of outer fragments until P K n ( , S n , ϕ n ) finishes); it initializes the GP ath tuple for the source of the gradient. By using the composition operator, the literals inferred in the model of P n , along with all the tuples in the container (fragment ) are then treated as constituent for the fragment e Pa = P A a (e Pe , S a , ϕ T ), i.e. they are used to generate facts for the program P a . This one is used to aggregate the hop-counter for the source with the one stored in the local container. e Pa is finally treated as constituent for the fragment e Pg = P A g (e Pa , S g , ϕ T ). Note that aggregation happens before spreading, imposing an order on the reactions. P A g is used to verify whether the gradient message must be spread to the neighbours. If so, a literal spreadGradient(a, local, d, c, b) is inferred during the computation of its semantics, where local is translated with the name of the current node. Simultaneously, the Logic Fragment P A ch ( , S ch , ϕ ch ) is executed as soon as a chemotaxis message is received (described as Cmsg(f, g), with f content of the message and g ID of the receiver). That Logic Fragment uses the local copy of the hop-counter to infer which is the next hop to which the chemotaxis message must be sent to (relay node). If the local hop-counter exists, a literal sendChemo(f, g, h) is generated in the model of P ch , with h representing the ID of the next receiver of the chemotaxis message. Otherwise, the message remains in the container until such a literal is finally inferred. All the literals contained in the consequent Q of LF gc are used by the agent A gc to manage the control part of the algorithm, described in the following code. the hop-counter caused by the applications of the aggregation-function; (ii) global properties, based on the local property holding in each node (e.g. we prove the creation of the shortest-path). The details are reported in [START_REF] De Angelis | Towards a logic and chemical based coordination model[END_REF]. Additional studies focusing on the integration of spatial-temporal logics in Logic Fragment are needed to prove the analogous statement when considering mobile nodes.

LFgc : P A g P A a P K n ( ,

Conclusion and Future works

In this paper we have presented a chemical-based coordination model based on a logic framework. Virtual chemical reactions are lead by logic deductions, implemented in terms of combination of logic programs. This approach combines the benefits of using a chemical-based coordination model along with the expressiveness of several distinct types of logic languages to formalise coordination logically. Intuitively, even though no formal verification or validation methods were presented, the rationale behind the proof of the correctness of coordination algorithm follows from a formalisation of the system properties to be proved in terms of logical formulae. This paves the way for at least two formal analysis: (i) what-if assessment -coordination events can be modeled in terms of injected/removed tuples and deducted literals can be used to test the satisfaction of the system properties formulae. This first kind of verification can be done at design time, to assess properties of the whole system under certain conditions (events) and partially at run-time, to infer how the system will evolve assuming a knowledge restricted to a certain subset of locally perceived events; (ii) the second type of design time analysis starts from the literals that satisfy the properties formulae and proceeds backwards, to derive what are the events that lead the system to that given state. Future works will focus on such aspects, to derive formal procedures for correctness verification of algorithm built on top of Logic Fragments. Several kinds of logics present interesting features to model and validate coordination primitives: (i) paraconsistent logics (e.g. [START_REF] Vitória | Modeling and reasoning in paraconsistent rough sets[END_REF]) and (ii) spatial-temporal logics, to assert properties depending on location and time parameters of system components. We plan also to realise an implementation of the model, including several semantics for Logic Fragments taking inspiration from the coordination primitives presented in [START_REF] Denti | Logic tuple spaces for the coordination of heterogeneous agents[END_REF].

Figure 1 :

 1 Figure 1: The generalization of the SAPERE Model

Definition 7 (

 7 Logic Fragments LF): (I) ∈ LF (II) (Grouping) If e ∈ LF then (e) ∈ LF (III) (Parallel-and) If e 1 , e 2 ∈ LF then e 1 e 2 ∈ LF (IV) (Parallel-or) If e 1 , e 2 ∈ LF then e 1 e 2 ∈ LF (V) (Composition) If P is a logic program, M an execution modality, S a set of A,I-generators, ϕ : P(G) → {T, F } and e p ∈ LF then (P, M, e P , S, ϕ) ∈ LF.

Lemma 1 (

 1 Properties of operators): Given a, b ∈ LF with a ≡ b we state that v L (a) = v L (b) for every set of literals L. Then for any a, b, c ∈ LF: I) a a ≡ a (Idempotence of ) II) a b ≡ b a (Commutativity of ) III) a (b c) ≡ (a b) c (Associativity of ) IV) a a ≡ a (Idempotence of ) V) a b ≡ b a (Commutativity of ) VI) a (b c) ≡ (a b) c (Associativity of ) VII) a (b c) ≡ (a b) (a c) ≡ (b c) a (Distrib. of over )

  ϕp( ) = T ⇔ ∃w : N (X)w ∈ T estP alin(x) = {T estP alin(a)|a is a positive palindromic number less than dmax} Logic code 1.1 Definite logic program P p P alin(x) ← N (x), T estP alin(x)

Figure 2 : 1 Property 1 :

 211 Figure 2: Evolution of the container for the example of Section 4.1

  Sn, ϕn), Sa, ϕT , Sg, ϕT P A ch ( , S ch , ϕ ch ) Logic code 1.2 Program P n -Next hop initialization GPath(x,dmax,null) ← ¬existsGPath(x) Logic code 1.3 Program P a -Aggregation cmpGradient(x1, x2, y1, y2, z) ← Gmsg(x1, x2, y1, z), GPath(x1, y2, w) updateGPath(x1, y1, x2, z) ← cmpGradient(x1, x2, y1, y2, z), less(y1, y2) Logic code 1.4 Program P g -Spreading spreadGradient(x1, local, z, y, x2) ← updateGPath(x1, y, x2, z) Logic code 1.5 Program P ch -Chemotaxis sendChemo(m, x, w) ← Cmsg(m, x), GPath(x, y, w) ϕn( ) = T ⇔ ∃w : Gmsg(x1, x2, y, z)w ∈ , ϕ ch ( ) = T ⇔ ∃w : Cmsg(x, y)w ∈ S ch = {Cmsg , GP ath } Sg = {updateGP ath e Pg } Sn = {existsGP ath ,V , Gmsg } Sa = {Gmsg e Pa , GP ath e Pa , less} less(x, y) = {less(a, b)|a < b, a, b ∈ {1, ..., dmax}} existsGP ath(x) ,V = {¬existsGP ath(a) ∈ I ¬existsGP ath(x) ∩ V ( )} V ( ) = {¬existsGP ath(a)|∃w : Gmsg(a, x, y, z)w ∈ ∧ ¬∃GP ath(a, y, w)w ∈ } Gradients are represented by tuples Gmsg(a, b, c, d) where a is the ID of the source, b is the ID of the last sender of the gradient, c is the hopcounter and d is the content of the message. Values null, d max and local are considered constants. Local hop-counter are stored in tuples of type GP ath(a, c, e)

  several types of logic programs (e.g. definite, general logic programs, several types DATALOG or DATALOG-inspired programs) associated with two-valued, multi-valued (e.g. Belnap's logic) or paraconsistent logics; (ii) several inference procedures (e.g. SLD, SLDNF ) and semantics (e.g. Aptvan Emden-Kowalski, Kripke-Kleen, stable,well-founded model semantics)[START_REF] Fitting | Fixpoint semantics for logic programming a survey[END_REF][START_REF] Kowalski | Linear Resolution with Selection Function[END_REF][START_REF] Apt | Contributions to the theory of logic programming[END_REF][START_REF] Emden | The semantics of predicate logic as a programming language[END_REF][START_REF] Vitória | Modeling and reasoning in paraconsistent rough sets[END_REF].

We consider the network of Figure 3; the Logic Fragment can be used to provide the gradient and chemotaxis functionalities as services to other agents running on the same nodes. Assuming that agent A Gm on node A wants to send a query message m 1 to all the nodes of the network, it creates and injects the gradient message Gmsg(A, A, 0, m 1 ). At this point a reaction with LF gc takes place, generating in the consequent Q of LF gc literals GP ath(A, 0, A) (semantics of P n ) and spreadGradient(A, A, m 1 , 0, A) (semantics of P g ). The second literal causes the spreading of the gradient message to nodes B and C. Similar reactions take place in the remaining nodes. If we assume that the gradient passed by node D is the first one to reach E then GP ath(A, 3, D) is inferred in the consequent Q on node E. When the gradient message coming from B reaches E, updateGP ath(A, 1, B, m 1 ) is inferred in the semantics of program P a , so the hop-counter tuple is updated in GP ath(A, 2, B). Now assuming that agent A Cm on node E wants to send a reply-message m 2 to node A, it creates and injects a chemotaxis message Cmsg(m 2 , A). On the basis of the tuple GP ath(A, 2, C), the literal sendChemo(m 2 , A, C) is inferred in the model of P g , so the message is sent to node B. Similar reactions take place on node B, which finally sends the chemotaxis message to node A.

Agent GC

Logic Fragment LFgc

GPath(A,1,A)

Agent GC

Logic Fragment LFgc

GPath(A,2,B)

Node B Node D

Agent GC

Logic Fragment LFgc

GPath(A,2,C)

Node E

Agent GC

Logic Fragment LFgc

GPath(A,1,A)

Node C

Agent GC

Logic Fragment LFgc

GPath(A,0,A) Gmsg(A,A,0,m1)