be proven. This model has significant advantages that make it a good choice for specifying multi-agent systems:

-the verification process is fully specified thanks to proof schemas; -the verification of the correctness of the different parts of an agent is compositional. The main consequence is that partial proofs are possible: a local modification of a specification does not require to verify the whole behaviour of the agent again; -the verification process of a system made of many agents is also compositional and so, proving the correctness of a multiagent system relies essentially on the proofs of the agents, and only few proofs have to be performed at the system level; -the program implementing the MAS derived from the specifications can be produced automatically thanks to automata.

However, there are few limitations to this model:

-communications between agents are not yet modeled; -specifying an agent with several achievement goals is not easy, although it is possible; -specifying agents performing concurrent tasks is not possible. This article demonstrates how recursive agents can be used to solve these limitations. After a brief reminder of the GDT model, we describe formally how the model can be extended to define recursive agents (informally, a recursive agent is an agent whose behaviour is partly achieved by "sub-agents"). Several design patterns allowing the implementation of standard behaviours with recursive agents are then presented in section 4. Modeling communications and integrating them with those design patterns is also discussed in section 5. The consequences of using recursive agents on the proof obligations are detailed in section 6. Finally, a comparison with other works is performed before concluding.

The GDT4MAS model

The GDT4MAS [START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF] model has been developed to specify and to verify the behaviour of multi-agent systems. This model is an extension of the GDT model that was introduced in [START_REF] Mermet | An agent compositional proof system[END_REF] and that has already been extended in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF]. It has been formally defined using the Linear Temporal Logic (LTL) [START_REF] Chandy | Parallel Program Design: A Foundation[END_REF]. As a consequence, in the sequel, the following standard operators of the temporal logic are used: always (2), eventually (⋄) and next (•).

Environment

In the GDT4MAS model, an agent is situated in an environment defined as follows:

Definition 1 (Environment) An environment is a triple E = (V E , I E , s E ), where:

-V E is the set of environment variables, -I E is the invariant of the environment, -s E is the set of stable properties of the environment.

Please note that:

-environment variables can a priori be modified by any agent of the system.

Their value can also change without any action of an agent; -the invariant of the environment is a predicate that is always true. It specifies the set of valid states of the system; -a stable property S is a predicate that may be false at the begining of the system. However, if S becomes true, it will remains true.

Example 1 (The RoM problem) The RoM (Robots on Mars) problem has been specified in [START_REF] Bordini | Verifiable multiagent programs[END_REF]. Two agents collaborate to clean the Mars Planet represented as a grid. Robot R2 can burn pieces of garbage that are on its cell, but it is unable to move. Robot R1 can pick up and drop waste, and it can move (the complete solution using GDTs can be found in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF]).

In this example, the invariant property specifies the size of the grid and the fact that each cell is either clean or dirty. It can be written: G ∈ x min ..x max × y min ..y max → {clean, dirty}

The fact that a cell different from R2's cell is empty is an example of stable property, as no agent can drop a piece of garbage (except R1 on R2's cell).

Agent Type and Agent

An agent is specified by instantiating an agent type. An agent type is specified as follows:

Definition 2 (Agent type) Let E be an environment. An agent type T is a tuple:

(name t , V t i , V t s , V t E , init t , I t , L t , S t , Actions t , Beh t ))

Where:

name t is the name of the type; -V t i is the set of internal variables; the internal variables of an agent ag are variables that the other agents cannot see and that may only be modified by ag; -V t s is the set of surface variables of this type and we have V t s ⊆ V t i .

Surface variables are variables that other agents can see but cannot modify; -V t E is the set of environment variables seen; this is a subset of the variables of the environment in which the agent is situated; -init t is the list of initial values of the internal variables; -I t is the invariant property; this predicate only deals with internal variables; -L t is the set of leads-to properties relying on environment and surface variables; informally, a leads-to b means that if a becomes true, b will eventually be true; -S t is the set of the stable properties of the agent; -Actions t is the set of capabilities; -Beh t describes the behaviour of the agent using a parameterised GDT, or pGDT (see section 2.3).

Example 2 (Agent type of robot R2) Robot R2 is defined by its position that is determined by two surface variables, (x R2 , y R2 ), its status (busy or not, specified by a boolean variable busy), a leads-to property that specifies that it always cleans the cell on which it stays, a set of actions Actions 2 (not detailed here) and a behaviour GDT (x, y) not detailed yet. So we have:

T R2 (x, y) =    
R2, {busy, x R2 , y R2 }, {x R2 , y R2 }, {G}, {f alse, x, y}, busy

∈ B ∧ (x R2 , y R2 ) ∈ N 2 , {2(G(x R2 , y R2 ) = dirty → ⋄G(x R2 , y R2 ) = clean)}, {}, Actions R2 , GDT R2    
Example 3 (Invariant) The invariant I t of an agent a is a predicate that must be verified in every state of a. It states the type of the internal variables of a, but it can also be used to specify other safety properties, as, for instance:

battery level < 10 → wif i = of f
Given this definition, an agent can be defined as follows:

Definition 3 (Agent) An agent a is defined by a tuple (name, type, param) where:

-name is the name of the agent; -type is the type of the agent; -param is a list of values for the parameters of the GDT.

If a = (name a , type a , param a ) is an agent, we will write name(a) to denote its name (name a ), type(a) its type and param(a) its list of parameters.

In this definition, the parameters allow to specialise both the initialisation and the behaviour.

Example 4 (Specification of two robots of type R2) Suppose there are two robots of type R2. The first one, called R2 a , is situated in the cell (x a , y a ). The second one, called R2 b , is situated in the cell (x b , y b ). These robots will be specified by the following two tuples (R2 a , T 2, (x a , y a )) and ((R2 b , T 2, (x b , y b ))).

The complete description of the system can be found in [START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF].

Behaviour

The behaviour of an agent type is specified by a parameterised Goal Decomposition Tree (or parameterised GDT). A GDT is essentially a tree of goals, in which each goal is decomposed into simpler subgoals, combined via a decomposition operator. The definition of a GDT is given hereafter. A parameterised GDT is obviously a GDT with parameters (see [START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF]).

Definition 4 (GDT) A GDT of an agent type AT is a triple (pre, tc, root) where:

-pre is the precondition of the GDT; it must be established by init AT and if the behaviour of the agent must be executed several times, it must be preserved.

-tc is the triggering context of the GDT. An agent executes its behaviour each time its triggering context is true (and it is not already executing its behaviour). This triggering context can be set to the boolean constant true if the agent must execute its behaviour for all time.

-root is the root goal of the GDT.

Each node (or goal) in a GDT has a name and is formally specified by a Satisfaction Condition (SC) and a Guaranteed Property in case of Failure (GPF). An SC (resp. GPF) is a temporal formula linking the states before the beginning of the goal resolution process and after it when this process succeeds (resp. fails). If G is a goal, we write SC G (resp. GP F G ) its SC (resp. its GPF). Notice that, as described in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF], GPFs can be inferred from leaf goals. In SCs and GPFs, variables known by the agents (internal or environment variables) can be either primed or unprimed. Unprimed occurences refer to the values of the variables in the state in which the goal resolution process begins whereas primed occurences correspond to the values of the variables in the state in which the goal resolution process ends. Thus, progress goals can be defined.

Definition 5 (Progress goal) A Progress goal is a goal whose satisfaction condition establishes a relation between the values of the variables before the goal resolution process and the values of the variables after the goal resolution process.

Example 5 (Progress goal) The goal that consists in increasing the value of a variable x is a progress goal that can be specified by the satisfaction condition x ′ > x. In the same way, a goal that specifies that after its execution, the value of a variable y must be equal to the value of the variable x before the resolution process is a progress goal that is specified by the satisfaction condition y ′ = x. However, goals are not always Progress goals.

Definition 6 (State Reaching goal) A State reaching goal is a goal whose SC does not establish a link between the value of variables before the resolution process and after. In the satisfaction conditions of such goals, variables are never primed.

Example 6 (State Reaching goal) The goal filling a tank can be specified by the following satisfaction condition tank = tank max where tank max is a constant.

In addition, a goal is typed with two flags:

-the laziness flag: a goal G is said to be lazy (L) if its resolution process is executed only if the SC of G is false when G is to be executed. On the contrary, a goal is said to be non-lazy (NL) if its resolution process is executed as soon as the goal is to be executed. -the necessary satisfiability flag: a goal is said to be necessarily satisfiable (NS) if each execution of the goal resolution process ensures the establishement of the SC of the goal. Otherwise, the goal is said to be non-necessarily satisfiable (NNS). Notice that this flag can be inferred from leaf goals using the process given in [START_REF] Simon | Goal Decomposition Tree: An agent model to generate a validated agent behaviour[END_REF]. When an NNS goal fails, its GPF is however established. The GPF of NS goals is assumed to be f alse.

Example 7 (Lazy and Non-Lazy goals) A progress goal cannot be a lazy goal.

For instance, a progress goal with a satisfaction condition x ′ = x + 1 that requires a change of the value of x during the goal resolution process implies that a goal resolution process runs. A state reaching goal is a goal that specifies a desired state, such as a goal g with the satisfaction condition x = 10. In most cases, such a goal will be labelled Lazy (L) because, when this goal has to be achieved, is the value of x is already 10, the agent is satisfied and nothing has to be done. However, in some cases, the resolution process associated to g will also perform other tasks that are necessary for the overall behaviour of the agent. In that case, g will be labelled N L.

Example 8 (NS and NNS goals) Consider a robot with an arm and a projector. The robot can always switch its projector on. As a consequence, the goal consisting in switching the projector on is labelled NS (necessarily satisfiable).

The arm can also take objects. But this action does not always succeed (the object may be too much round for instance). So the goal consisting in catching an object should be labelled NNS. However, even if the robot fails to catch the object, after the goal, its clamp will be closed. So, the GPF of the goal could specify this.

Finally, the resolution process of a goal can be either an action (for a leaf goal) or a combination of one or several subgoals using a decomposition operator (for non-leaf goals).

Internal goal

Definition 7 (Internal goal) Let A be an agent in an environment E. An Internal goal G of a GDT is a 7-tuple:

(name, Op , Children , sc, gpf , lz , nsat ) where:

-name is the name of the goal; -Op is a decomposition operator; -Children is a sequence of goals whose length -sc is the Satisfaction Condition of the goal; -gpf is the Guaranteed Property in case of Failure of the goal; -lz is the laziness flag of the goal; -nsat is the necessary satsfiability flag of the goal; matches the arity of Op .

In our model, several decomposition operators have been defined using temporal logic. The definitions given hereafter are only informal ones (see [START_REF] Simon | Goal Decomposition Tree: An agent model to generate a validated agent behaviour[END_REF] for more details):

-SeqAnd is an operator that allows the decomposition of a goal sequentially into two subgoals. For instance, to achieve the goal x ′ = (x + 1) 2 , we can choose to first achieve the goal x ′ = x + 1 and then to achieve the goal

x ′ = x 2 .
-SeqOr is an operator that allows the decomposition of a goal G into two subgoals G 1 and G 2 with the following informal semantics: if the resolution process of G 1 succeeds, then G is achieved. Otherwise, the agent has to attempt to achieve G 2 . -And is a non-deterministic operator that allows to decompose a goal into two subgoals that can be achieved in any order to achieve the parent goal.

For instance, to achieve the goal x ′ = x + 3, we either try to achieve x ′ = x + 1 and then x ′ = x + 2 or try to achieve x ′ = x + 2 and then

x ′ = x + 1.
-Or is a non-deterministic or operator.

-SyncSeqAnd(V) and SyncSeqOr(V) are operators that can lock environment variables V to prevent from any concurrent access. -Case(cond 1 , cond 2 ) decomposes a goal into two subgoals with conditions for each subgoal. -Iter decomposes a goal G into a subgoal S. Iterating on the resolution of S will eventually achieve goal G. For instance, we could have SC G ≡ (x ′ = x -10) and SC S ≡ (x ′ = x -1).

Example 9 (Internal goal and decomposition operator) The main goal G 1 of robot R2 is to clean its cell and to be not busy. This can be specified by the following SC : SC G1 ≡ ¬busy ∧G(x R2 , y R2 ) = clean. This goal can be achieved by first picking up the waste on the cell (x R2 , y R2 ) (goal G 2 , the robot is then busy) and then by burning the piece of garbage (goal G 3 , the robot is not busy anymore). So we specify that

G 1 is decomposed into G 2 SeqAnd G 3 with SC G2 ≡ busy ∧ G(x R2 , y R2 ) = clean and with SC G3 ≡ ¬busy ∧ G(x R2 , y R2 ) = clean.

Leaf goal and action

An action specifies a capability of an agent and is formally defined as follows:

Definition 8 (Action) An action a is a 5-tuple (name a , pre a , post a , gpf a , nsat a ), where:

-name a is the name of the action, -pre a is the precondition of the action (a predicate that must be true in the state in which the action must be executed), -post a is the postcondition of the action (the property that is established if the action succeeds), -gpf a is the guaranteed property in case of failure of the action (the property that is established if the action fails), -nsat a is the necessary satisfiability of the action; it is true if the action always succeeds, false otherwise.

A leaf goal is a node that is not decomposed into subgoals but that has an action linked to it: Definition 9 (Leaf goal) A leaf goal G is a 6-tuple:

(name, a, sc , gpf , lz , nsat ) where:

-name is the name of the goal, -sc , gpf , lz and nsat play the same role as for internal goals, -a is the name of the action that will be executed to achieve the goal.

Example 10 (Leaf goal and Action) The goal G2 of robot R2 presented in example 9 is a leaf goal. The action linked to it is the action specified by the following tuple: (pick action, ¬busy ∧ G(x R2 , y R2 ) = dirty, busy ∧ G(x R2 , y R2 ) = clean, f alse, true). Indeed, to pick a piece of garbage, the robot arm must be empty and a piece of garbage must be on the cell of the robot. Once the action has been executed, the robot is busy but the cell is clean. We assume that this action always succeeds.

Definition 10 (Goal execution) In the rest of the paper, the expression "executing a goal" is often used. This means "executing its resolution process", that is to say, for an internal goal, executing its subgoals as specified by the operator, and, for a leaf goal, executing the action associated with this goal.

Formal semantics

The formal semantics of the GD4MAS model has been given in [START_REF] Mermet | Agent design with Goal Decomposition Trees[END_REF][START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF] using temporal logic. In particular, each operator is defined by a set of temporal formulae (slightly different depending on whether the goal is L or NL). Some of these formulae are common to all operators, the others are specific. To define these formulae, new temporal variables have been specified:

-init g is a variable that is true in every state where goal g begins to be executed. It is false in the other states;

-end g is true in every state where the execution of g ends; -in g is true during the execution of the goal g (between init g and end g and false otherwise). So, in g verifies the following formulae:

-2(init g → in g ): when the execution of g begins, in g is true, -2(in g ∧ ¬end g → •in g ): if in g is true and g does not end, then in g remains true, -2(¬in g ∧•¬init g → •¬in g ): in g cannot become true when the execution of g does not start, -2(end g ∧•¬init g → •¬in g ): if the execution of g ends, then in g becomes false (except if a new execution of g starts immediately) -sat g is true when the execution of the goal g ends successfully (the goal is achieved).

Example 11 (SeqAnd formal semantics) The formal semantics of the SeqAnd operator is defined by the following formulae (g1 and g2 are the first and second subgoals of g):

-general formulae:

-2(¬in g1 ∨ ¬in g2 ): both subgoals are not executed simultaneously; -2(in g1 ∨ in g2 → in g ): executing a subgoal means executing the parent goal; -2(¬init g ∨ ¬end g ): trying to achieve a goal requires at least one state transition; -2((in g ∧ ¬end g ) → ¬init g ): while the execution of g is in progress, no other execution can begin; -formulae specific to the SeqAnd operator:

-2(sat g1 → •init g2 ): the execution of g2 begins just after g1 has been achieved; -2((end g1 ∧ ¬sat g1 ) → •end g ): if the execution of g1 ends with a failure, then the execution of goal g ends; -2(sat g2 → (end g ∧ sat g )): if goal g2 is achieved, then g is also achieved; -2(end g2 ∧ ¬sat g2 → •end g ): if g2 is not achieved, the execution of g also ends; -2(init g → init g1 ): starting to execute g consists in starting to execute g1.

Proof

In the context of the GDT4MAS model, several kinds of proof must be performed:

-the preservation of the invariant of the system by each agent; -the preservation of the invariant of each agent by itself; -the establishment of the satisfaction condition of the leaf goals if the action linked to them succeeds; -the establishment of the precondition of an action each time it is used; -the establishment of the leads-to properties of an agent by its GDT;

-the correctness of each goal decomposition.

The proofs to perform are called proof obligations (PO). They are generated using proof schemas (PS). Details about proof schemas and their validity can be found in [START_REF] Mermet | Agent design with Goal Decomposition Trees[END_REF]. In order to have compositional proofs, a Proof Context (PC) is associated with each node. It is used as a local hypothesis for each local proof. The proof context of each node is inferred from the GDT thanks to rules that are given in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF] and are validated in [START_REF] Mermet | Agent design with Goal Decomposition Trees[END_REF][START_REF] Mermet | Agent design with Goal Decomposition Trees: Companion paper[END_REF]. Notice that the proof context of a node only depends on its parent node or its sibling node. Here, a simplified proof schema for the SeqAnd operator is given, as well as the sketch of the proof schema of the Iter operator.

Verifying a SeqAnd decomposition

Let A be a goal decomposed into B SeqAnd C. The notation φ[a/b] is used to represent the formula obtained by substituting within φ any free occurence of b by a. Using V in the following formula means that this substitution is performed for any free variable occuring in the formula. The simplified proof schema associated with such a decomposition is the following1 :

(SC B )[V tmp /V ′ ] ∧ (SC C )[V tmp /V ] → SC A
This proof schema is called simplified because it does not take into account:

-the hypotheses that can be assumed (context, invariants, etc.) -the fact that environment variables may have been modified between the execution of the resolution process of B and the execution of the resolution process of C -the fact that the satisfaction conditions of state-reaching goals are specified without using primed variables Notice that the effective proof schema that can be found in [START_REF] Mermet | Agent design with Goal Decomposition Trees[END_REF] takes this into account.

Example 12 (Proof Obligation generation for a SeqAnd) Consider the case where SC A ≡ x ′ = (x + 1) 2 , SC B ≡ x ′ = x + 1 and SC C ≡ x ′ = x 2 . Applying the simplified proof schema of the SeqAnd operator gives the following proof obligation:

x tmp = x + 1 ∧ x ′ = x tmp 2 → x ′ = (x + 1) 2
Which is obvious (proof is left to the reader).

Verifying an Iter decomposition

We do not give here the detailed proof schema of the Iter operator, but only its principle. When a goal G is decomposed into a subgoal S thanks to the Iter operator, we have to prove that goal G will eventually be achieved. To do so, a variant is used. A variant is a decreasing sequence defined on a well-founded structure (a well-founded structure is a pair (set, ≤) on which each decreasing sequence is bounded). So proof obligations are generated to establish that:

-each time S is executed (successfully or not), the variant decreases; -when the variant reaches its lower bound, the goal G is achieved. This proof process is a standard proof process for loop termination. A consequence is that each time an Iter operator is used, we prove that the number of iterations that may be performed is finite.

External goals

In order to specify collaborating agents, external goals have been defined.

Definition 11 (External goal) An external goal E of a GDT T of an agent

A is a leaf goal of T specified by a tuple (name, sc , lz ). Such a goal is a goal that cannot be achieved by A. However, it is required to prove that another agent in the system will achieve such a goal when needed. When E is to be executed by A, A waits until E is achieved. An external goal is obviously an NS goal.

Example 13 (External goal) In the RoM problem, R1 must wait for R2's cell to be empty before dropping the waste it carries on it. This goal is not achieved by R1 but by R2. So, it is an external goal.

The proof process associated with external goals is described in [START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF].

Graphical representation

Internal goals and leaf goals are represented by ellipses2 . When a goal is decomposed into two subgoals, the parent goal is linked to its children with two edges and the name of the decomposition operator is written between both edges. If a goal is decomposed into one subgoal (this is the case with the Iter operator), the name of the operator is written near the edge. An NS goal is represented by two concentric ellipses. The name of the action linked to a leaf node is written under the representation of the node.

An external goal is represented by a rectangle. A Lazy goal is indicated by a kind of tab with an "L" label. Non-Lazy goals are optionally indicated by the same tab with an "NL" label.

In most cases, the figure representing a goal (either an ellipse or a rectangle) is labeled with the name of the goal. However, it can also be directly labeled with its satisfaction condition.

Example 14 (Graphical representation of a GDT) In the case of the RoM problem, the GDT of robot R1 is shown in figure 1. Details about this GDT can be found in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF].

Related work

The GDT4MAS model is connected to several different kinds of works. A detailed comparison with these works can be found in [START_REF] Simon | Goal Decomposition Tree: An agent model to generate a validated agent behaviour[END_REF] but is summarised hereafter. First of all, there are links with formal agent models like MetateM [START_REF] Fisher | A survey of concurrent METATEM -the language and its applications[END_REF], Desire [START_REF] Brazier | Simulating Social Phenomena[END_REF] or Gaïa [START_REF] Wooldridge | The gaia methodology for agent-oriented analysis and design[END_REF]. These works are focused on agent models on which it is possible to reason. There are also links between our proposal and agent programming languages like AgentSpeak [START_REF] Rao | AgentSpeak(L): BDI agents speak out in a logical computable language[END_REF], 3APL [START_REF] Dastani | Programming agent deliberation: An approach illustrated using the 3apl language[END_REF], ConGolog [START_REF] De Giacomo | Congolog, a concurrent programming language based on the situation calculus[END_REF]. These languages allow to specify agents behaviours which can be directly executed, which is one of the goals of the GDT model. However, 3APL does not allow to prove the specified behaviour and ConGolog is dedicated to situation calculus. Our approach can also be compared to goal-oriented MAS development methods like Prometheus [START_REF] Khallouf | Towards goal-oriented design of agent systems[END_REF], MaSe [START_REF] Scott | Automated derivation of complex agent architectures from analysis specifications[END_REF], KAOS or Tropos. Indeed, our proposal is also intended to provide a complete MAS design process from the specification to the implementation. Moreover our approach takes place in the framework of "formal transformation systems" as defined in [START_REF] Scott | Automated derivation of complex agent architectures from analysis specifications[END_REF]. Other works use the term of subgoal, but with different meanings. For instance, in [START_REF] De Boer | A Verification Framework for Agent Programming with Declarative Goals[END_REF], a subgoal S of a goal G is a logical consequence of G, whereas in [START_REF] Thangarajah | Detecting and Exploiting Positive Goal Interaction in Intelligent Agents[END_REF], a subgoal S of a goal G is a goal whose achievement is necessary to achieve G and as a consequence, corresponds to our subgoals when the And operator is used. Last but not least, our proposal can be directly compared to SMA verification methods. Two subtypes can be distinguished: theorem proving based (like in PROSOCS) and model checking.

PROSOCS [BED + 06] agents are agents whose behaviour is described by goal decomposition rules à la Prolog. Rules are parameterised by time variables allowing to perform proofs about the evolution of the system state. Many characteristics of PROSOCS agents are very interesting for performing proofs, and a proof procedure has been implemented in Prolog. However, the system is limited to propositional logic formulas. The Goal method [START_REF] De Boer | A Verification Framework for Agent Programming with Declarative Goals[END_REF] also has a proof model, but the notion of Progf Obligation is missing.

Model checking is a verification method consisting in testing all the situations which may be encountered by the system. Two kinds of model checking techniques can be distinguished: bounded model checking [START_REF] Bordini | Verifiable multiagent programs[END_REF] and unbounded model checking [ALW04,RL04,KLP04]. However, with the two techniques, proofs can only be performed on finite models or on models that can be considered as finite ones.

The recursive extension of the GDT4MAS model

As stated in the introduction, the GDT4MAS model lacks expressiveness. However, the gaps detected (several achievement goals, concurrent tasks, message reception management) can all be filled by introducing parallelism into the agents. Indeed, managing concurrent task and several achievement goals can be obviously achieved by introducing parallelism. But managing message reception can also be performed so: with such a system, a task can be dedicated to the management of the message reception, letting the main process run normally, and being able to react as soon as possible to message reception.

Using an agent for each task is a way to specify parallel tasks. As a consequence, as our model allows the specification of agents, it seems a natural way to specify an agent needing parallel tasks by using several internal agents.

Recursive agents

Given definitions 2 and 1, it can be seen that an agent type T = (name t , V t i , V t s , V t E , init, I t , L, S t , Actions, Beh t ) can be considered as an environment E t = (V Et , I Et , s Et ) computed as follows:

V Et = V t i ∪ V t E I Et = I t ∧ I E s Et = S t
So, the following transformer function is introduced:

Notation 1 envir function Let T be an agent type. We note envir(T ) the environment that can be computed from T .

This transformation allows the consideration of sub-agents:

Definition 12 (Recursive agent and Sub-agent) Let A and R be two agents. If the environment of A is envir(R), then R is called a recursive agent.

A is called a sub-agent of R.

Definition 13 (Recursive Multi-Agent System) A recursive Multi-Agent System is a multi-agent system made of at least one recursive agent. Such a system can also contain non-recursive agents.

Please note that sub-agents are also agents, and so:

-are associated with an agent type with a GDT; -are specified by an invariant; -have a set of internal variables; -run with an interleaving parallelism model; -. . . Please note also that a recursive agent is also an agent and so, the fact that it has a recursive structure is not seen by other agents of the system in which it is situated. This is a key point to preserve the compositional aspect of the GDT model.

By introducing recursive agents, we first want to allow an agent to perform several plans in parallel. As a consequence, sub-agents have to contribute to the goal of the agent they are part of. To do so, new decomposition operators must be introduced. But before that, we have to be able to specify that an agent is included in another agent.

Here are some identified properties about sub-agents. Let A be an agent situated in an environment E. Let S be a sub-agent of A. The following properties must be verified:

-S cannot be a sub-agent of another agent (this differs from other recursive agent models, as the one described in [START_REF] Hepple | A Common Basis for Agent Organisation in BDI Languages[END_REF]), -S cannot read variables of E that A is unable to see, -internal variables of A must be considered by S as environment variables because they can also be modified by other sub-agents of A, -S must be able to exchange information with other sub-agents of A.

We then need to describe the structure of a recursive agent model.

Relationship between an agent and its sub-agents

In order to help the reader and to maintain consistency with the existing terminology, we have chosen to reuse the two following terms introduced in [START_REF] Hepple | A Common Basis for Agent Organisation in BDI Languages[END_REF].

Definition 14 (Context agent) Let A and a be two agents where a is a sub-agent of A. A is called the context agent of a.

Definition 15 (Content agent) Let A and a be two agents where a is a sub-agent of A. a is called a content agent of A.

A shared point between the huge number of agent's definitions is that agents are autonomous entities [START_REF] Ferber | A meta-model for the analysis and design of organisations in multi-agent systems[END_REF][START_REF] Wooldridge | Agent theories, architectures, and languages: a survey[END_REF]. This is also our point of view. However, as content agents have to participate to the goals of their context agent, it seems natural that their context agent has a kind of control over them. So, we choose to give to context agents the following responsabilities:

-it is the role of the context agent to specify when a content agent starts to live; -although a content agent can die when it wishes, its context agent can also force it to die. These responsabilities will be operated differently, according to the decomposition operators. As a consequence, it is also clear that a recursive agent is not a MAS: its context agents are parts of a structured single behaviour.

Parallel decomposition operators (PDO)

Informal definition

Until now, decomposition operators consisted in decomposing a goal into one or several subgoals. Now, new decomposition operators are needed in order to help to decompose a context agent into several content agents. More precisely, as content agents have to contribute to goals of the context agents, these operators decompose a goal of the context agent into sub-agents that will contribute to the resolution of this goal. More formally:

Definition 16 (Parallel Decomposition Operator (PDO)) Let A be a context agent and ca = {a i , 1 ≤ i ≤ n} the set of its content agents. A Parallel Decomposition Operator is an operator allowing the decomposition of a goal G of A into a list of pairs (SC j , a j ) where a j is an agent of ca and SC j is the satisfaction condition of the main goal of a j .

To simplify, we will write in the sequel that a goal is decomposed by a PDO into subagents.

From then on, two PDOs can be informally described:

Definition 17 (The ParAND PDO) The ParAND PDO (Parallel And) allows a decomposition of a goal G of a context agent A into a set of content agents ca with the following semantics: when A has to achieve a goal G, all the content agents of ca start the execution of their behaviour. As soon as one of these agents stops with a failure (it fails to achieve its main goal), A stops all the other agents of ca and ends the resolution process of G. G may be achieved or not. If all the agents of ca stop successfully, the resolution process of G ends and G is achieved.

Definition 18 (The ParOR PDO) The ParOR PDO (Parallel Or) allows a decomposition of a goal G of a context agent A into a set of content agents ca with the following semantics: when A has to execute goal G, all the content agents of ca start the execution of their behaviour. As soon as one of these agents stops successfully, A stops all the other agents of ca, ends the resolution process of G and G is achieved. If all the agents of ca stop with a failure, the resolution process of G ends. G may be achieved or not.

A synchronised version of the parAN D operator is also proposed: the SyncP arAN D V operator. This operator enables to lock a set V of environment variables during the execution of the parallel decomposition.

Formal semantics

The semantics of the ParAND and ParOR operators can be now formally specified. We assume that the goal of the context agent to be decomposed is called G. We also consider that this goal will be achieved thanks to n content agents a i and that the main goal of each agent a i is called mg i and its satisfaction condition is SC i .

For each content agent a i , A new variable must be introduced: ended i , that memorises the fact that a i has already ended or not. In other words, when ended i is true, it means that agent a i has ended since the beginning of the execution of G. The values of these variables can be computed has follows:

2(∀i.(init G → ¬ended i ))
(1)

2(∀i.(¬ended i ∧ ¬end mgi → •¬ended i )) (2) 2(∀i.(end mgi → ended i )) (3) 2(∀i.(ended i ∧ in G → •ended i )) (4)
Formula 1 specifies that when the execution of G begins, no content agent may have ended. Formula 2 specifies that a non-ended agent cannot be ended if it does not end. Formula 3 specifies that an agent becomes ended when it ends. And finally, formula 4 specifies that during the execution of G, an ended content agent remains ended.

As the parent goal of a PDO is a goal, formulae defining the value of in G and that were given in section 2.4 apply and so, they are not given in the following table. On the contrary, as a PDO does not decompose a goal into subgoals but into content agents, general formulae of the other decomposition operators that were also given in section 2.4 do not apply.

Formal semantics of the parAND operator is given in table 1.

init G → n i=1 (initmg i ) (5) ∀i. (endmg i ∧ ¬satmg i ) → end G ∧ (∀j.(¬ended j → endmg j )) ¡¡ (6) (∀i. (ended i ) ∧ ∀i. (end i → sat i )) → (end G ∧ sat G ) (7)
Table 1 ParAND formal semantics

These formulae have the following meanings:

-formula 5 specifies that all content agents start when the execution of G starts; -formula 6 specifies that if one of the content agents ends with failure, then the execution of G ends and the other content agents are interrupted (That is to say, for each content agent of an agent A, if it ends with a failure, the executions of the parent goal and of the other content agents of A end) ; -formula 7 specifies that if all the content agents end successfully, then the execution of G ends successfully. Please note that this formula does not specify that content agents that have ended before the last one ended successfully. Indeed, in this case, formula 6 specifies that the other agents are stopped.

Formal semantics of the parOR operator is given in table 2.

init G → n i=1 (initmg i ) (8) ∀i. (endmg i ∧ satmg i ) → end G ∧ sat G ∧ (∀j.(¬ended j → endmg j )) ¡¡ (9) (∀i. (ended i ) ∧ ∀i. (endmg i → ¬sat i )) → •end G (10)
Table 2 ParOR formal semantics Formula 9 specifies that when one of the content agents ends successfully, then the parent goal ends also successfully and the other content agents must be interrupted.

Finally, formula 10 specifies that if all the content agents end with failure then the execution of G ends (if already ended content agents had ended successfully, by formula 9, other content agents should have been stopped.

Using recursive GDT4MAS agents

In previous articles, we have shown that many features of the GDT4MAS model make it suitable to solve concrete problems. For instance, the fact that environment variables can evolve regardless of the agents makes our model usable to model complex systems. The compositional aspect of the proof is also a key feature, because, contrary to verification methods based on modelchecking, the verification process remains tractable even with many agents and infinite state spaces. The application of the model to few case studies (a prey-predator system -in which we have proven that the predators catch the moving prey -, the robots on mars problem, and an extension of this problem with several robots of type R2) has shown it should be adequate to specify and implement real-size problems, even if the lack of a CASE-tool to support the method prevents us from proceeding to such an application. We claim that the extension proposed in this paper not only does not reduce the usability of the method, but rather should increase it.

There are two main ways to use recursive agents: with a top-down approach or with a bottom-up one. The first case will appear during the design phase, when having to design an agent that must perform several tasks in a concurrent way. The second case is a consequence of the specifications of the studied problem: when an agent relies on several modules, or when the robot being modeled is made of several actuators, and if certain tasks can only be performed by one of these modules or actuators, the designer will use recursive agents.

Design patterns using PDO

As stated above, recursive agents can be used to solve different kinds of standard problems. As a consequence, to help the designer to build a MAS, several design patterns are given in order to answer to these different situations.

Graphical representation

The overall graphical representation of a GDT has already been presented. To distinguish children nodes of PDO that correspond to content agents, they are represented by hexagons. Such an hexagon is labeled by a couple "name : SC" where name is the name of the content agent and SC is the satisfaction condition of its main goal.

Several autonomous actuators

A basic usage of PDOs is to allow an agent to perform several tasks simultaneously. This is for instance necessary for a robot with several actuators working independently, like an autonomous motion system and an autonomous camera: the robot can move while observing its environment. In this case, a content agent can be associated with each actuator. For instance, in figure 2, agent A 1 would be in charge of moving the robot whereas agent A 2 would manage the camera. The GDT of the content agents are not represented.

Several achievement goals

Another trivial usage of the ParAND PDO is the following: an agent has several achievement goals to achieve. With the previous GDT models, this could be implemented by two different means. The first solution (see figure 3) was to decompose the main goal of the agent with an AND operator between the different achievement goals of the agent. However, this meant that the agent had to achieve completely one of the goals before trying to achieve another one. The second solution (see figure 4) was to propagate the conjunction of satisfaction conditions of the different achievement goals to the leaf nodes. This leads however to a less clear specification.

With the recursive GDT model, the more intuitive specification given in figure 5 can be used. In this version, two content agents (whose GDTs are not represented on the figure) are dedicated to achieve each one of the 2 achievement goals.

Allowing an external event to interrupt a task

Suppose that an agent A has, as part of its GDT, a task T to perform (that is to say a goal to achieve). Suppose also that depending on external events (a message income, an evolution of the environment, etc.), this task becomes not relevant anymore. This can be implemented thanks to recursive agents by the GDT structure presented in figure 6. In this figure, agent A uses two content agents. The first one, A T is dedicated to the achievement of the task T . The second one, A E , detects the external event E that would make T not relevant anymore. The expected behaviour of A is the following: if T is achieved before E occurs, then T is achieved for A and it can continue to execute its normal behaviour. On the contrary, if E occurs before T is achieved, the resolution process has to be stopped and A must continue its normal behaviour. This correponds to the ParOr Semantics. The behaviour of agent A E is very simple: its GDT is made of a single node, its root node, which is also an external goal (and thus, a leaf node), waiting for the external event.

Sharing reactive and autonomous behaviours

Suppose an agent A has an autonomous cognitive behaviour. Suppose then that this agent must also respond to external events in a reactive manner. Such an agent can be decomposed into two content agents: the first one, A C will achieve the cognitive behaviour of A. The second one, A R will take into account the reactive behaviour. We might imagine that the end of the cognitive behaviour determines the end of the agent execution, and that the reactive behaviour must remain active while the cognitive behaviour has not been completely performed. This can be implemented by a GDT structure following the schema presented on the figure 7 for agent A and on the figure 8 for the agent A R . On this last figure, the exernal goal waits for an event to occur (its SC is a formula describing the event) and the goal labeled SC R is the root goal of a sub-tree. The behaviour of this agent is then the following:

-it waits for an event to occur (external goal); -when this event occurs (SeqAnd), it reacts (sub-tree with root goal SC R ); -as the root goal of this agent is not achieved (its SC is f alse), it waits for the event again;

Please note that this implies to allow iter parent goals that are not necessarily satisfiable, which was not allowed before. This can be done because in that case, the termination is however guaranteed (because the execution of A C will eventually stop and this will stop the execution of A R , as specified by the formal semantics of ParOR). This termination problem will be discussed in section 6. Reacting to a message without waiting explicitly for it was not very easy to specify with the previous version of the GDTs. Indeed, it required to test very often if the message had been received or not. The recursive agents help to give a pretty solution to this problem: the design pattern sharing reactive and autonomous behaviours presented above in section 4.5 can be used and the external goal of the reactive component (see figure 8) can be replaced by a leaf goal with the received() action attached to it.

To examplify this, in this article, a simplified version of a communication system is described. Firstly, only peer-to-peer messages are studied and not broadcast communications. We also suppose that each agent has an infinite message queue where all incoming messages are stored until they are read. We also suppose messages are read in the order they are received and that reading a message removes it from the queue. Other kinds of communications could be easily modeled but this is not the main aim of this article.

Sending a message

We choose to specify the sending of a message by an atomic action send(dest, msg) where dest is the identifier of the agent the message is sent to. This action adds to the end of the message queue of the dest agent the couple (f rom, msg), where f rom is the identifier of the sender and msg is the message itself. As any agent can write a message into the message queue of a given agent, it means that message queues must be considered, for the proof, as environment variables. So, we choose to represent message queues by a unique functional environment variable mq3 . As in [START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF], we suppose that A is an environment variable containing the set of agents of the MAS. The type of mq is the following:

mq ∈ A → seq(A × M SG)
where M SG is the type of the messages (no assumption on this type is made here) and seq is a set-theory constuctor for sequences.

As a consequence, writing send(dest, msg) as an action of an agent a will be a shortcut for the following expression:

mq ′ (dest) = mq(dest) • (a, msg)
where • denotes the addition at the end of a sequence.

Reading a received message

Reading messages received by an agent a consists in reading the head of mq(a). This will be performed by an action noted (sender',msg')=received() returning two values: the sender of the message and the message itself. This action is a shortcut for the following action:

(sender ′ , msg ′ ) = head(mq(a)) ∧ mq ′ = tail(mq(a))
By convention, if mq(a) is an empty sequence, head(mq(q)) equals (null, null) and tail(mq(a)) is an empty sequence.

Managing communications

Managing message sending is straightforward: the send action must be associated with a leaf node specifying when a message must be sent.

Waiting for a message is also easy: an external goal consisting in waiting for the message queue to be modified can be introduced in the GDT where the message is awaited. This goal can be part of a content agent dedicated to message reception management, as specified in the introduction of this section, while another content agent achieves the main goal.

Proof schemas

As stated in section 2.5, a key concept of the GDT4MAS model is the notion of proof schema. This concept, that can also be found for instance in the B method for the verification of standard software [START_REF]The B-Book[END_REF], gives a way to generate a set of formulae whose truth establishes the correctness of the software. As new constructs are introduced in this article, the associated proof schemas must be provided.

Variables status

Let A be a context agent. Let b and c be two content agents of A. Then, internal variables of A and environment variables of A are environment variables for b and c. b (resp. c) may moreover have its own internal variables that can be neither seen nor modified by c (resp. b) or A. However, b (resp. c) may have surface variables whose values can be read by c (resp. b) and A.

Relationships between agents

In the work considered here, a content agent represents a part of a context agent, and as a consequence, cannot be a part of several context agents. So, in the model presented here, the MAS structure is a tree of agents.

Operators' Proof Schemas

Proof schema associated with parAND

When a goal G is decomposed into a set of content agents sa i by a ParAND operator, it means that when all the content agents have achieved their main goal, the parent goal is also achieved. So, we would expect a proof schema such as: (SC i ) → SC G (where SC i is the satisfaction condition of the main goal of a i ).

But the two following constraints must be considered:

-as content agents do not end at the same time, environment variables can be modified between the end of a content agent and the end of the last content agent. -internal variables of content agents cannot be seen by the context agent.

As a consequence, in the proof schemas, the satisfaction conditions of the main goal of the content agents must be restricted to surface variables. We note P s the projection of a property P of an agent a to the surface variables of a 4 . Then, the first part of the proof schema associated with the ParAND operator, and that helps to satisfy formula 7, is the following:

n i=1 ((SC i ) s ) → SC G (11)
Moreover, we also have to establish rule 5 which specifies that when the context agent has to achieve goal G, each subagent of G starts to execute its GDT. Given the definition of the triggering context of an agent given in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF], this can be ensured by proving that the context C G of the parent goal of the parAND operator implies the triggering context T C i of each of the content agents introduced by the operator. So, the second part of the proof schema associated with the parAND operator is the following:

C G → n i=1 (T C i ) (12)
For the synchronised version SyncP arAN D V , the projection used in equation 11 is performed on surface variables and on the locked variables.

Proof schema associated with ParOR

The reasoning process to determine the proof schema associated with the parOR operator is the same as the one done for the parAND operator. So, the proof schema is made of two parts:

-the first one must establish that the parent goal is achieved when one of the content agents achieves its main goal, and so, helps to establish rule 9; -the second one must establish that content agents start their execution when the context agent starts executing the parent goal, and so, helps to establish rule 8.

This leads to the following proof schema made of two parts where (SC i ) s,e is the projection of SC i to the union of the surface variables and the environment variables of the context agent :

n i=1 ((SC i ) s,e ) → SC G (13)
Please note that the satisfaction conditions of the main goals of the content agents are projected on surface variables and also on environment variables because as soon as a content agent achieves its main goal, the parent goal of the parOR operator is achieved.

C G → n i=1 (T C i ) (14)

Necessary Satisfiability inference

As explained before, the Necessary Satisfiability flag of internal goals of an agent are inferred from the leaf nodes by rules associated with each decomposition operator. Such rules can also be given for parallel operators.

NS inference for the ParAND operator

The parent goal of a ParAND operator is NS if all the main goals of its subagents are NS.

NS inference for the ParOR operator

The parent goal of a ParOR operator is NS if at least one of the main goals of its subagents is NS.

GPF Propagation rules

Guaranteed Properties in Case of Failure are properties that are guaranteed to be established by the execution of a goal if it is not achieved. As explained in previous papers about GDTs [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF], they can be computed in a bottom-up manner from leaf nodes to the root node. The same process can be applied to parallel operators.

GPF inference for the ParAND operator

The parent goal of a parAND operator fails as soon as one of its subagents ends without having achieved its main goal. So, we have:

GP F G = n i=1 ((GP F i ) s,e ) (15)
where GP F i is the GPF of the main goal of the content agent a i . The projection is on surface variables and environment variables because as soon as a content agent ends without having achieved its main goal, the parent goal fails.

GPF inference for the ParOR operator

The parent goal of a parOR operator fails if all the subagents have ended without having achieved their main goal. So we have:

GP F G = n i=1 ((GP F i ) s ) (16)

Termination

Termination is a necessary property to ensure that the behaviour of an agent is correct. Until now, in the standard GDT model, agents had to terminate, and thus, a variant had to be associated with each iter operator to ensure this. However, as stated above in section 4.5, it may be interesting to have a subagent whose behaviour does not end explicitly. However, as this content agent must eventually terminate, such a content agent must be used under constraints.

Definition 19 (infIter) A new iteration operator called infIter is introduced. The definition of this operator is identical to that of the standard iter operator but termination is not required.

Definition 20 (Infinite agent) an infinite agent is an agent whose GDT contains an infIter operator.

Please note that the behaviour of an infinite agent may be finite.

Proposition 1 Infinite agent usage An infinite agent can only be used as a subagent of a parOR operator and of which at least one subagent is finite and has an NS main Goal.

This last proposition guarantees the termination of a recursive agent even if some of its content agents are infinite.

Example of application

We propose to extend the problems of robots on Mars already presented in this paper by giving more details on the structure of the robot R2. Robot R2 has an arm that can collect wastes and put them in a tank with a limited capacity of 10 pieces of garbage. When this tank contains at least 3 pieces of garbage, a conveyor belt brings all the wastes one by one to the incinerator of the robot. From an external point of view, the behaviour of R2 remains the same: when its cell is dirty, the robot will eventually clean the cell. From an internal point of view, however, the robot is made of several systems that can act concurrently.

Robot R2

Robot R2 has a single internal variable: the tank, represented by an integer variable T . The root goal of R2 G 1 is to have its cell empty and not to have its tank full. So we have SC G1 = G(x R2 , y R2 ) = clean ∧ T < 10. Robot R2 will begin to execute its behaviour when its cell is not empty or when its tank contains at least 3 pieces of garbage. So we have T C R2 = G(x R2 , y R2 ) = dirty ∨T ≥ 3. Then the behaviour of R2 consists in cleaning its cell and saving the tank to be full. These two tasks will be performed by the two effectors of the robots (the arm and the conveyor belt) and so, are associated with the root goal using a SyncP arAN D operator. The GDT of R2 is shown in figure 9.

The arm of R2

The arm of R2 has a single internal variable, busy, a boolean that is true if and only if the arm carries a waste. As a content agent of R2, its environment variables are the internal variables and the environment variables of R2. Here, environment variables of the arm are G, the grid (G is an environment variable of R2) and the tank T (T is an internal variable of R2). The triggering context of R2 is true. Two actions are available for the arm: pick and drop. Both actions are NS. Their preconditions are pre pick ≡ ¬busy ∧ G(x R2 , y R2 ) = dirty and pre drop ≡ busy ∧ T < 10. Their postconditions are post pick ≡ busy ∧ G(x R2 , y R2 ) = clean and post drop ≡ ¬busy ∧ T ′ = T + 1.

The GDT of the arm of R2 is presented in figure 10. The main goal of the arm is lazy. Indeed, if the cell (x R2 , y R2 ) is not dirty, the arm has nothing to do. Otherwise, it must first pick the piece of garbage and then, it must drop the waste it carries in the tank as soon as it is not full. As the arm is unable to empty the tank, emptying the tank is an external goal. Please note that the arm can drop its waste in the tank while the conveyor belt is emptying it (as soon as there is at least one slot available).

The conveyor belt

The conveyor belt has no internal variable. Its only environment variable is the tank (T ). The triggering context of R2 is true. The only action this agent can perform is the convey action. Its precondition and postcondition are pre convey ≡ T > 0 and post convey ≡ T ′ = T -1. This agent has also a leads-to property: T = 10 leads -to T = 0.

The main goal of the conveyor belt is to prevent the tank from being full. This goal is of course lazy. If the tank contains less than 3 wastes, there is

Verification of the behaviour of R2

To verify the correctness of the behaviour of R2, we have to apply the proof schemas on each content agent of R2 (the arm and the conveyor belt) but also on the main agent itself (R2).

R2

As the behaviour of R2 is reduced to a parAND operator, we just have to apply the proof schema associated with this operator and that is given in equations 11 and 12. Both of the following properties are obtained:

(G(x R2 , y R2 ) = clean) ∧ T < 10 → (G(x R2 , y R2 ) = clean ∧ T < 10) (17) C G1 → (true ∧ true) (18)
The verification of both formulae is trivial. For the second one, the value of C G1 is not calculated because it is not required to verify the property.

arm of R2

Verifications of both SyncSeqAnd decompositions are trivial and so are not presented here, as well as the linked to the leaf goals. We briefly detail the verification associated with the achievement of the external goal (called E in the sequel). Given the proof schema presented in [START_REF] Mermet | GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent Systems[END_REF], we have to prove that there is in the system an agent with a leads-to property A leads -to B with C E ∧ ¬SC E → A and B → SC E . Indeed, another agent in the system, the conveyor belt, has a leads-to property T = 10 → T = 0. Moreover, T = 10 is a logical consequence of ¬SC E (as SC E = ¬(T = 10)) and T = 0 implies SC E . So the achievement of the external goal each time it is required is proven.

conveyor belt of R2

Verifying the behaviour of the conveyor belt is a standard proof of a GDT: verifying the case decomposition is trivial (as T < 3 → T < 10 and T = 0 → T < 10) and verifying the Iter decomposition is easy as the variant to choose is T (a natural), the subgoals makes T decrease, and the fact that the variant reaches its lower bound (T = 0) trivially implies the satisfaction condition of the parent goal (T = 0).

Comparison with other works

Several works dealing with recursive agents exist. In the sequel, we compare our proposal with other ones.

Motivation of the recursive model

Some work use recursive agents to model organisations. These organisations can be human organisations [START_REF] Adam | Flexible hierarchical organisation of role based agents[END_REF] or organisations of agents [START_REF] Hepple | A Common Basis for Agent Organisation in BDI Languages[END_REF][START_REF] Dennis | Language constructs for multi-agent programming[END_REF]. The aim of the latter is to propose a very general but simple framework which can be used to specify most of the proposed models for organisational structuring in multiagent systems such as teams [START_REF] Cohen | [END_REF][START_REF] Tidhar | Team-oriented programming: Prelimaniry report[END_REF], roles and organisations [START_REF] Ferber | A meta-model for the analysis and design of organisations in multi-agent systems[END_REF] or roles and permissions [NVSB + 07]. The aim is clearly different from ours: whereas they want to model organisations and groups, we want to model components of an agent. This explains a first difference between their work and ours: for them, an agent can be part of several context agents but for us, this is impossible. However, although the main aim is different from ours, our proposal is very close to this framework which is inspired from the group notion used in METATEM [START_REF] Fisher | A survey of concurrent METATEM -the language and its applications[END_REF]. Please notice that, although this framework is intended to be independent of the underlying language for agents, this language is restricted to a "BDI-like" language, contrary to our proposal.

In [START_REF] Giret | Towards an abstract recursive agent[END_REF], the authors try to specify a model for an abstract recursive agent as a mean to integrate different pre-existing MAS. Using this model should help to consider each MAS as a whole, i.e. as an agent with individual goals, beliefs, actions... This possibility is essential to be able to use the MAS in a new context. Please note that in this proposal, an abstract recursive agent exists only during the analysis and design stages but has no implementation. Actually the authors claim that abstract agents are "modeling artifacts to represent MAS" and their behaviour. More precisely, as abstract agents are recursive ones, they contain agents from behaviour of which the behaviour of the abstract agent can be defined. An abstract recursive agent can be seen as a set of interacting agents when considering its internal structure but can also be seen as a single agent with its own properties resulting from those of its component agents. These concepts are illustrated with an example dealing with mobile physical cooperative robots. A robot can be modeled by an abstract agent containing multiple interacting agents, each of which being responsible for a part of the robot functionalities; this is comparable to one of the design patterns proposed in this paper (see section 4.2).

Holonic manufacturing systems [START_REF] Botti | ANEMONA: A multi-agent methodology for Holonic Manufacturing Systems[END_REF] typically use recursive agents to model robots made of several actuators, which corresponds to one of the design patterns we propose to help a designer to use our recursive agents.

Finally, our work present some similarities with the proposals described in [JT02,GHG + 08]. Indeed, in these both articles, recursive agents are used to help to model complex systems.

Verification

Most recursive agent models do not deal with verification. Indeed, they have not been developed for that (see [START_REF] Adam | Flexible hierarchical organisation of role based agents[END_REF] for instance).

In [START_REF] Giret | Towards an abstract recursive agent[END_REF] for instance, ordered sequences of actions are used to obtain the set of goals of the abstract agent using a function f . Unfortunately, even if the authors give properties about this function, they do not provide any mean to determine this function in a given context, and so no verifcation can be performed.

In their papers, Fisher et al. explain that a context agent adds a kind of glue to its content agents thanks to a special specification that they call N SPEC (this glue is a formal specification that makes all the content agents work together). However they do not give any key to write such a specification or guarantee its consistency with the specification of the content agents. And so, once again, proofs can no be performed.

Verification is however taken into considerations in a few works. In [START_REF] Jonker | Compositional Verification of Multi-Agent Systems: A Formal Analysis of Pro-activeness and Reactiveness[END_REF], the authors present a way to specify a multiagent system with a tree of properties dedicated to sub-processes. Moreover, examples of compositional proofs are presented. Our solution gives however many answers to questions raised by this article. For instance, Jonker et al. use a few decomposition operators without giving their semantics, and properties to verify are not justified whereas our proof schemas and their verification validate our method.

The verification is clearly the main goal in [GHG + 08], where examples of proofs are performed thanks to model checking and thanks to theorem proving by induction. However, verifications are performed on roles, which does not take into account compositional problems occuring when an agent implement several roles. Moreover, the notion of proof obligation is not integrated to the work, bringing no warranty on the correctness of the system verified.

Expressiveness

In several models, an agent can be a content agent of several subagents [GHG + 08, ASM08,HDF08]. Moreover, in these model, the recursive structure changes dynamically. This is well suited to model organisations, a goal of most of these models, but it makes proofs harder, and we chose a less expressive model to increase the success rate of proofs. To simplify proofs once again, our content agents are not visible outside their context, contrary to most holonic systems [START_REF] Adam | Flexible hierarchical organisation of role based agents[END_REF][START_REF] Fischer | Holonic multiagent systems -theory and applications[END_REF] and to the model presented in [START_REF] Hepple | A Common Basis for Agent Organisation in BDI Languages[END_REF]. This makes the model more compositional, maximizing reuse and compositionality (let recall that compositionality is a key concept to verify multi-agent sytems). However, we introduced environment variables and surface variables to express interactions between agents, a concept missing for instance in [START_REF] Jonker | Compositional Verification of Multi-Agent Systems: A Formal Analysis of Pro-activeness and Reactiveness[END_REF].

The problem of task interruption has been addressed in few articles, but never with recursive agents. The solution proposed in [START_REF] Thangarajah | Aborting Tasks in BDI Agents[END_REF] propose repair plans when a task is aborted, a feature that our design pattern does not provide yet, but in this article, tasks cannot be interrupted anytime, and a task that must be interruptible must be modified, whereas our construct does not require to modify the task itself.

Gap between specification and implementation

The model we propose is the only one we know that, thanks to automata composition patterns associated to decomposition operators, allows a code generation from a verified specification.

Conclusion and Perspectives

In this paper, a new extension of the GDT model has been presented. The first aim of this extension, called "recursive GDT agents", is to allow agents to run parallel plans, that is to say to execute two subgoals at the same time. This was not really possible in the previous version of the GDT model: an agent had to finish the execution of a subgoal before beginning the execution of another one. The main principle of this proposal is to introduce the notion of "content agent". As a consequence, at different points in time during its execution, an agent can choose to manage the execution of subgoals resulting from a goal decomposition by assigning them to content agents. Content agents are GDT agents, which are not perceived by agents which are outside their context agent, and which can be controlled by the agent they are included in. As presented in the paper, this notion is very close to context and content notions proposed by Fisher et al. in [START_REF] Hepple | A Common Basis for Agent Organisation in BDI Languages[END_REF]. That is why the same terminology has been used for our proposal even if some differences exist.

Formal definitions of the notions of content agent and context agent have first been given. Decomposition operators called "parallel decomposition operators" have also been introduced. These operators help to decompose a goal into subgoals which are executed by different content agents, and to specify formally how a context agent and its content agents interact. Such subgoals are modeled by leaf nodes in the GDT of the context agent. The formal semantics of these operators is provided using logical variables and LTL rules as for other decomposition operators.

We have also shown that the recursive GDT notions give pretty solutions to very common behaviours by providing design patterns to build GDT agents, that is to say partial GDTs which can be instantiated and then integrated in effective GDTs. Another interesting aspect of this new proposal has also been shown: the correctness of the behaviour of GDT agents using content agents can be easily proven (contrary to the other recursive agent models we studied). Indeed, proof schemas associated with the new parallel operators are given. The main interest of this extension is that, with the same mechanism, various behaviours can be specified. More precisely, as far as we know, this is the only work until now that leads to prove in a compositional way the behaviour of agents with interruptible behaviours.

Several perspectives derive from the work presented in this article. At first, we wish to extend thes set of design patterns presented here to design a kind of library which could be associated with a MAS design method using the GDT model. This library can be also completed by parameterised GDT's presented in [START_REF] Mermet | Specifying, verifying and implementing a MAS: A case study[END_REF]. We also aim at completing the set of design patterns with new ones helping to model classical communication protocols. The set of parallel decomposition operators introduced in this article is reduced. A future work will also consist in specifying new PDOs. CASE-tools to support the GDT model are limited to prototypes. A great effort has to be performed to develop other tools. Indeed, one of the main interest of the GDT model is that it has been designed to make the verification process automatic, but the implementation has not not yet been fulfilled.

Fig. 1

 1 Fig. 1 example of a GDT

Fig. 2

 2 Fig. 2 design pattern for a robot with several autonomous actuators

Fig. 3

 3 Fig. 3 2 achievement goals: first old version

Fig. 5

 5 Fig. 5 2 achievement goals: new version

Fig. 7

 7 Fig. 7 Reactive and autonomous agent

Fig. 9

 9 Fig.9GDT of robot R2g

Fig. 10

 10 Fig.10GDT of the arm of R2

Fig. 11

 11 Fig.11GDT of the conveyor belt of R2

In this proof schema, V tmp is a set of fresh variables containing a variable v tmp for each variable v of V .

This ellipse may be a circle.

Considering message queues as a unique environment variable is only for the proof. Concretely, the message queue of an agent should be a variable of the agent itself.

and so, (SC i )s is the projection of SC i to the surface variables of a.


GDT4MAS : a formal model and language to specify and verify multiagent systems

Bruno Mermet, Gaële Simon

To cite this version:

Bruno Mermet, Gaële Simon. GDT4MAS : a formal model and language to specify and verify multiagent systems. Verification and validation of multi-agent models for complex systems, 2011, paris, France. hal-00955956


Petros Evgenikos

George Yannis

Panagiotis Papantoniou

Alan Kirk

Pete Thomas

Deniz Atalar

Thierry Hermitte

Pierre Van Elslande

REVIEW OF CURRENT IN-VEHICLE SAFETY SYSTEMS AND RELATED DATA SOURCES

Keywords: Safety systems, data sources, system evaluation, adaptive cruise control

When considering how safety systems fulfil drivers' needs, leading to an evaluation of overall benefit, it is important to understand the overall functionality of the system, take into account as many design parameters as possible and consider previous evaluation work. The objective of this research is to provide an inventory of invehicle technological systems that are present on current production models, using a standard template. A catalogue listing details such as the aim of the system, the functions covered by the system, phase of the accident upon which the system is acting, the level of intervention, technical specifications and previous evaluations is developed for 31 active, passive and integrated safety systems and the example of the Adaptive Cruise Control system is presented in this paper. Moreover, a review of existing identification procedures related to safety systems is carried out, aiming to underline the available information sources that could be used to gather data on safety equipment using a common format, review the variable level of quality and the feasibility and length of time that it would take to collect the data.

Results revealed that although there are many different implementations of safety systems with different performance parameters, the development of a safety systems inventory can become a useful tool for analysts to establish a feel for a generic system, project the functionality of such a system onto available accident data and importantly to evaluate if the system really meets drivers' needs.

The use of an assembled standard template can further act as a central register, in which analysts can quickly acquire detailed information on the system along with web links to vehicle manufacturer, governmental, safety and research organisation websites.

Furthermore, two main safety systems data collection methods were identified through the review of different data sources, either using the make/model/ variant approach or the VIN number method, demonstrating the feasibility of recording all active, passive and integrated safety systems implemented within a vehicle to a European wide database.

INTRODUCTION

In spite of countless amounts of research and development, road safety is still one of the main societal concerns today. It is not only a matter of concern for the European Commission and National Governments but also for several stakeholders such as the vehicle industry, insurance companies, non-governmental organisations and more generally for every single road user. Car manufacturers have made strong efforts towards the improvement of passive (and also active) safety of their vehicles for the past 20 years. However, current road safety research has shown that preventive (prevention of accidents) and active safety (recovery of an emergency situation) should now, particularly, be brought forward (TRACE, 2007).

There are two main objectives of this research: The first one is to develop a standard template to be used for the collection of all related information to in-vehicle technological systems that are present on current production models. A list of all currently available safety systems is provided and the standard template for information on Adaptive Cruise Control (ACC) is established as an example. Adaptive Cruise Control (ACC) systems have been actively developed and introduced into the consumer market by vehicle manufacturers in the past decade. They extend earlier systems (CCC -Conventional Cruise Control) to cases when driving at a fixed constant speed is not possible because of traffic conditions (Bifulco et.al., 2011).

The second objective outlines the approach undertaken to understand the feasibility of recording all of the active, passive and integrated safety systems found within a vehicle to a European wide database. The aim is to underline the available information sources that could be used to gather data on safety equipment, to review the variable level of quality and the feasibility and length of time that it would take to incorporate these information into a single database. This will in turn lead to a possibility of developing a standard recording system for every passenger vehicle that is introduced to the European market.

A review of Welsh's previous work on the development of a fitment database (2009) is carried out, according to which governmental organisations, commercial organisations, research bodies, motor manufacturers and the insurance industry were contacted, together with a literature review with regards to the feasibility of a fitment database for the United Kingdom.

In summary two main methods of data collecting by the various sources were identified. Either collecting data according to a make/model/ variant approach or according to a Vehicle Identification Number (VIN). Regarding the first method, an outline of three possible approaches and a possible method that would combine these approaches is presented.

The created database would ideally list the vehicles according to the make, model and production year the safety systems were present from, with the possibility of more specific data in the case of the use of the VIN number. By using the make and model of the vehicle as an identifier this would enable standard equipment details to be linked with other databases [START_REF] Welsh | Feasibility study for equipment database and exposure data evaluation[END_REF].

LIST OF SAFETY SYSTEMS

The aim for presenting the list of 31 safety systems is to cover many types of road users and vehicles; cars, goods vehicles, buses, powered two wheelers and pedestrians, along with infrastructure technologies. These technologies currently fall under four possible headings (DaCoTA, 2012): 1. Passive safety measures: reducing the consequences of an accident by managing the crash forces. 2. Active safety measures: reducing the possibility of accidents occurring by taking preventative measures. 3. Integrated safety measures: aiming at integrating active and passive safety systems within a vehicle to allow the vehicle to adapt to a pre-crash situation and either stop the crash from occurring or reducing the crash consequences by reacting to the crash appropriately. 4. Rescue safety measures: also known as tertiary technologies. Optimising the rescue phase by supplying information on crash severity and location to rescue services.

As expected with such a wide range of safety systems different functional modes are present, from systems that are completely automatic (for example, electronic stability control) to those requiring driver reaction (for example, lane departure warning).

According to the literature review, these are 31 safety relevant systems that are currently becoming established on vehicles or are likely to be realised in the near future.

The category column in Table 1 was included to put the safety systems into generic descriptive categories that could be used regarding drivers' needs and system effectiveness evaluation (TRACE, 2007).

STANDARD TEMPLATE FOR INFORMATION COLLECTION -ACC EXAMPLE

The aim of developing a standard template for each safety system is to give a good representation of generic system functions and parameters whilst also describing the functionality of current technologies fitted to vehicles.

The structure of this proposed standard template starts with the thorough description of each system examined. A thorough and complete description of the system's aim is presented, along with pictures or figures that describe the system operation. Then, the intentional and unintentional functions covered by the system, as well as the phases of the accident sequence upon which the system is acting, are described. Subsequently, in each template the different levels of intervention that the examined safety system can provide are described. Furthermore, technical specifications are provided aiming to give a good representation for generic system functions and parameters whilst also describing the functionally of current technologies fitted to vehicles, giving examples of particular vehicles. Finally, previous evaluations in terms of both methodology and results are provided as links, in order to recognize previous evaluations of safety systems.

The standard templates are developed for each of the 31 safety systems presented above to act as a central place in which analysts can quickly acquire the information needed to consider how safety systems fulfill driver's needs. For the purposes of this research, information collected through the proposed standard template is presented for the Adaptive Cruise Control (ACC) navigation system, as an example.

Aim of the system

If a leading vehicle is travelling at a lower speed than the user's vehicle, or is located within the preset time or distance headway, the ACC system intervenes via braking pressure or throttle/engine torque control so that the headway increases. The system only intervenes if the current preselected speed or headway would lead to a likely collision or the speed would reduce the set headway. ACC may employ radar, laser or machine vision to continuously monitor the leading vehicle. Auxiliary detectors also monitor the speed, yaw and cornering rate of the vehicle to maintain tracking of the leading vehicle in the same lane when cornering.

Functions covered by the system  Keeps a set distance to vehicle in front  Detecting a fixed obstacle on the road  Predicting that another user will stop or slow down  Predicting that another user will move off or fail to stop  Improved traffic flow Phases of the accident sequence upon which the system is acting

Technical Specifications

In slow traffic or traffic jams, the automatic emergency braking function of Subaru's system aims to stop and hold one vehicle until the vehicle in front starts moving again, even if the driver is pressing the accelerator. In the case that the system, wiring, microprocessor or the code goes wrong, the worst that could happen could be almost entirely mitigated by good back-up procedures. (Moon et.al, 2009).

Previous evaluations

REVIEW OF EXISTING IDENTIFICATION PROCEDURES RELATED TO SAFETY SYSTEMS

The aims of this section are to underline the available materials that could be used with regards to understanding safety systems, to review the variable level of quality and the feasibility and length of time that it would take to incorporate these measures. This will in lead to a possibility of developing a standard recording system for every passenger vehicle that is introduced to the European market.

In summary, two main methods of source data were identified, either collecting data according to a make/model/ variant approach or a VIN number method.

Make/model/ variant approach With regards to the make model approach three possibilities exist. A literature source addresses the availability of safety equipment fitted as standard. This does not require a large amount of resources but does require a labour intensive method due to the nature of the data procession.

A second approach would be to use JATO as a private group to collect the data with an applicable data file. JATO Dynamics is a research company that aims at delivering up to date and accurate automotive data for companies and the specification data cover 44 countries. This file would then be incorporated within a database and used to collate with existing databases. After this procedure two approaches could be taken.

Either JATO would be used as a subcontractor to collect annual data for upload into said database or the methods identified above with regards to literature sources could be used as a further development of the JATO data. This method has a higher cost compared with the literature source approach but would be easier to use, as the data would be given in a file that is ready for use within a fitment database.

VIN based data sources

The Vehicle Identification Number (VIN) is a 17 digit alpha/numeric code that uniquely identifies all registered vehicles. It is a mix of manufacturer, SAE and ISO elements. These elements are broken down into: the World Manufacturer Identifier (WMI), the Vehicle Descriptor Section (VDS) and the Vehicle Identifier section (VIS) [START_REF] Welsh | Feasibility study for equipment database and exposure data evaluation[END_REF]. The VIN can be used either directly by decoding information contained within the VDS to identify the make/model and then refer to a literature source, to or by using the VIN as an identifier for a more detailed vehicle specification held by the manufacturer. Table 5 summarizes the findings found by [START_REF] Welsh | Feasibility study for equipment database and exposure data evaluation[END_REF] with regards to methods for building a fitment database: Literature, JATO Net, VIN decoder, VIN link to manufacturer databases.

CONCLUSION

This paper describes the development of safety systems descriptions to support work on drivers' needs and evaluations of safety benefit. For this purpose, a standard template was created for 31 safety systems including details such as the aim of the system, the functions covered by the system, phase of the accident upon which the system is acting, the level of intervention, technical specifications and previous evaluations. The example of the Adaptive Cruise Control system is presented.

The use of an assembled standard template can further act as a central register, in which analysts can quickly acquire detailed information on the system along with web links to vehicle manufacturer, governmental, safety and research organisation websites.

This paper also identifies the advantages of setting up a database that contains safety equipment. This database would enable the analysis of current and future active, passive, integrated and rescue systems implemented in vehicles in conjunction with accident and naturalistic driving data, providing a better understanding of driving behaviour and safety system performance. In summary, two main methods of source data were identified either a make/model/ variant approach or a VIN number method.

Make model approach does not require a large amount of resources but does require a labour intensive method due to the nature of the data procession. With regards to a VIN based approach the best results would be achieved by directly using manufacturer data. This data would be received directly from manufacturers and as such would require the support of the manufacturers. Furthermore, the equipment data for each VIN would be assembled within a database to be subsequently combined with accident data.

It is considered that the most reliable and effective method to assemble an equipment database within Europe would be to use a combined model. As part of the data needed for a revised PTI process the VIN for each relevant vehicle would be included within a database together with the relevant safety equipment. This would include both standard equipment for that model of vehicle as well as the optional equipment installed. The database would be in a format that could be combined with the vehicle registration data at national level and subsequently with macroscopic and in-depth accident data.

Table 1 :

 1 Safety systems

	Name	Abb.	Category
	Advanced Adaptive Front Light System	AAFS	Visibility
	ABS (Antilock Braking System)	ABS	Dynamic Control Longitudinal
	Adaptive Cruise Control	ACC	Dynamic Control Longitudinal
	Airbag Pedestrian Protection	PedPro	Protection
	Alcolock Keys	AK	Driver Behaviour
	Anti Whiplash Seat	AW	Protection
	Automated Headlights	AutoLights	Visibility
	Blind Spot Detection	BS	Visibility
	Brake Assist	BA	Dynamic Control Longitudinal
	Collision Avoidance and Automatic	CA (AEB)	Dynamic Control Longitudinal
	Emergency Braking (not pedestrian)
	Collision Warning	CW	Warning
	Drowsy Driver Detection System	DDS	Driver Behaviour
	eCall	eCall	Localization/Prevention
	Electronic Stability Control	ESC	Dynamic Control lateral
	Event Data Recorder	EDR	Driver Behaviour
	Intelligent Speed Adaptation	ISA	Dynamic Control Longitudinal and
			Speed / Warning
	Intersection Control	IC	Communication
	Lane Changing Assistant	LCA	Warning
	Lane Keeping Assistant	LKA	Dynamic Control Lateral
	LDW (Lane Departure Warning)	LDW	Dynamic Control Lateral
	Low Friction Detection	LoFrctD	Localization/Prevention
	Night Vision	NV	Visibility

Table 2 :

 2 Phases of the accident sequence

	Phases	Evaluation of actions
	Driving Phase	ACC may employ radar, laser or machine vision (camera) to continuously monitor the leading vehicle
	Rupture Phase	The system intervenes if the current preselected speed or headway would lead to a likely collision
	Emergency Phase	The system decelerates the vehicle
	Crash Phase	If a collision is inevitable the system may have been able to decrease speed and lower crash severity
	Rescue Phase	ACC may employ radar, laser or machine vision (camera) to continuously monitor the leading vehicle
	Level of intervention

Table 3 :

 3 Level of intervention

	Specifications

   ISO/DIS 22178 Intelligent transport systems -Low speed following (LSF) systems -Performance requirements and test procedures  ISO/DIS 22179 Intelligent transport systems -Full speed range adaptive cruise control (FSRA) systems -Performance requirements and test procedures

	 ISO 15622:2002 Transport information and control systems -Adaptive Cruise Control Systems -Performance requirements and test procedures [15622]  SAE J2399 Adaptive Cruise Control (ACC) Operating Characteristics and User
	Interface [J2399]
	 FMCSA-MCRR-05-007 Concept of Operations and Voluntary Operational
	requirements for Forward Collision Warning Systems (CWS) and Adaptive Cruise
	Control (ACC) Systems On-Board Commercial Motor Vehicles [FMCSA05b]

Table 4 :

 4 VIN data Managed by SAE and denotes the country of origin and the manufacturer. VDS: For some manufacturers, e.g. Mercedes Benz, the VDS contains Model and Variant information, which could be cross referenced with manufacturer information to indicate the standard equipment fitted. It may be possible to decode an option fitted to a single model, by a single manufacturer. E.g. for a 2006 Ford Focus the option of a handling pack may be indicated by the sequential number within the VIS. Unfortunately for the majority of manufacturers VIS is simply a sequential number in order to bring the VIN up to the required 17 digits.

	Standard	1	2	3	4	5	6	7	8	9	10 11 12 13 14 15 16 17
	ISO 3779	WMI			VDS						VIS
	WMI:

VIS:

Table 5 :

 5 Fitment data comparison from[START_REF] Welsh | Feasibility study for equipment database and exposure data evaluation[END_REF]

		When combined with other method	Yes	Yes	No	When combined with other method
	Update process	Manual	Provided by JATO Net	Manual	Manual	Upon request

This work has been undertaken in the EC funded DaCoTA project.