A formal framework for organization- centered multi-agent system specification: A rewriting logic based approach

Abstract

Formal semantics provide precise specifications of the expected behavior of organizational model based on multi-agent system, allowing users to understand them and also modelers to reason about them and to prove their correctness. A first step was described to provide a formal specification framework among organization-centered multi-agent system by using an existing rewriting logic language called Maude to translate organizational models, which allows addressing these issues. Such formalization provides additional benefits, such as enabling the simulation of the specifications or giving access to the Maude toolkit to reason about them. In this paper, Maude was used to formally describe Agent-Group-Role-based-organization specifications. The proposed framework could, in fact, be used as is or with some extensions to describe other agent organization models. Actually, the results of precedent works [31, 32] were synthesized with additional extensions related to the formal description of the Agent-Group-Role model. This approach is illustrated using the supply chain management (SCM) case study.

Keywords

Formal specification multi-agent system Agent-Group-Role organization Agent UML Maude supply chain management

1. Introduction

The adoption of an organization-centered approach to develop multi-agent system (MAS) is based on the definition of a set of constraints that a group of agents adopts to achieve their social purposes easily [3]. This set of constraints is usually described as organizational models. By having an underlying organization model, the multi-agent system may assure some level of efficiency and efficacy [21], since the model establishes ways to coordinate and control the agents’ behavior [6].

In [31] several methods to modeling organization oriented multi-agent system have been analyzed such as Agent-Group-Role (AGR) [11], Model of Organization for multI-agent SystEms (MOISE $+$ ) [18], INGENIAS [16], Gaia [30] and others. They have modified the multi-agent system construction through giving rise to new organizational concepts. However, they offer only informal or semi-formal descriptions for representing multi-agent system organizational requirements. For this reason the proposed approach offers a joint representation of the organizational requirements while profiting from the advantages of the semi-formal and the formal approaches. Agent-Group-Role is one of the most popular and widely used organizational models. It has normally been described in an intuitive and informal manner, by means of definitions of its main features in natural language. However, this lack of rigorous description can easily lead to imprecisions and misunderstandings that might hinder the proper usage and analysis of the model, and the development of correct multi-agent system [17].

The main purpose and justification of this paper is formalization. So, a rewriting logic based approach is described for prototyping the Agent-Group-Role model for multi-agent systems organization to be able to reason, on the one hand, about the organizational model, and on the other hand, about its general semantics. This formal approach allows validation and verification and is presented through a case study. First, a formal specification of Agent-Group-Role is given then it is refined for a specific application that is supply chain management. The specification approach is based on the use of rewriting logic [13], and its implementation in Maude [25] with the graphical formalism Agent UML in order to formally specify a system in terms of Agent-Group-Role model.

Maude supports user-definable syntax and, in consequence, it offers prototype parsers for free. Another advantage of using Maude is that it provides tool support for interesting possibilities such as model simulation, reachability analysis and model checking [25]. Furthermore, because the rewriting logic specifications are executable, the proposed formal framework can be used as a prototype, which allows simulating it in order to be able to provide a first feedback about the suitability of the solution. Maude [17] offers different possibilities for realizing the simulation, including step-by-step execution, several execution strategies, etc. Although this work does not focus on model checking, the fact that Maude provides verification facilities is an important motivation for this effort of formalizing Agent-Group-Role model in Maude.

This paper is structured as follows: Section 2 presents briefly the background concepts that are used along the proposed approach towards achieving formal specification framework among Agent-Group-Role based multi-agent system. Section 3 describes how Agent-Group-Role organizational model can be encoded in Maude when using the translation process. Section 4 details the application of a formal specification process of an Agent-Group-Role based multi-agent system for modeling and formalizing a supply chain management case study according to the proposed framework. Section 5 provides a brief overview of major related works. Finally, some conclusions and future research activities are outlined in Section 6.

2. Literature review

2.1 Agent-Group-Role organizational model

Ferber and Perrot in [9] argue that organization is one of the basic concepts of any multi-agent system, being such organization a predefined unit or emerging from interactions occurring during system execution. Usually, organizational models provide means for designing the way multi-agent system should coordinate and control the behavior of its agents, specifying constraints in a number of dimensions. Structural constraints, for instance, define the roles and groups that will form the multi-agent system and functional ones specify the way agents that play such roles within some group should behave in order to achieve goals. Furthermore, some models provide rules and norms for rewarding and/or punishing agents, depending on their behavior in an organization [7].

The Agent-Group-Role model [11], is the evolution of the AALAADIN model [10]. It was developed aiming at providing a simple and concise way to describe multi-agent organizations. As its acronym suggests, it is based on three primitives: agents, groups and roles. Agents are proactive, autonomous and communicative entities that populate these organizations by playing (multiple) roles within (several) groups. An important characteristic of the Agent-Group-Role model is that no constraints are placed upon the architecture of an agent or about its mental capabilities [22]. Thus, an agent may be as reactive as an ant, or as clever as a human. Groups can be defined as a set of agents sharing some common characteristic. A group is used as a context for a pattern of activities, and is used for partitioning organizations, two agents may communicate if and only if they belong to the same group, but an agent may belong to several groups. This feature will allow the definition of organizational structures. Lastly, roles are abstract representations of agent functionalities in a group. Roles are local to groups, and a role must be requested by an agent. A role may be played by several agents. In this model, a group is described by a group structure. Such structure contains all the characteristics that define a group, for example its name and the roles agents are allowed to play in it. Thus, it is possible to conceive groups as instances of group structures.

As it is mentioned in [11] Agent-Group-Role defined two types of constraints between roles, namely correspondence and dependence. If there is a correspondence constraint between two roles A and B, it means that an agent who plays A will automatically play B. In its turn, a dependence constraint between A and B means that playing A is a prerequisite to play B. These three primitive concepts satisfy a set of axioms that unite them. They denote by $x$ .send( $y, m$ ) the action of an agent $x$ sending a message m to an agent $y$ , by roleIn( $r, g$ ) the statement that the role is defined in a group $g$ , and by plays( $a, r, g$ ) the statement that the agent a plays the role $r$ in $g$ . They also denote by GStruct( $g, g s$ ), the statement that $g$ is a group considered as an instance of the group structure $g s$ , and member( $x, g$ ) the statement that an agent $x$ is a member of a group $g$ . Here are the axioms of the structural aspect of the Agent-Group-Role model:

Every agent is member of a (at least one) group: $\forall x$ : Agent, $\exists g$ : Group, member( $x, g$ ) (1)

Two agents may communicate only if they are members of the same group: $\forall x,y$ : Agent, $\forall m$ : Message, $x$ .send( $y, m$ ) $\Rightarrow\exists g$ : Group, member( $x, g$ ) $\wedge$ member( $y, g$ ) (2)

Every agent plays (at least one) role in a group: $\forall x$ : Agent, $\forall g$ : Group $\Rightarrow\exists r$ : Role, plays( $x, r, g$ ) (3)

An agent is a member of the group in which it plays a role: $\forall x$ : Agent, $\forall g$ : Group, $\forall r$ : Role, plays( $x, r, g$ ) $\Rightarrow$ member( $x, g$ ) (4)

A role is defined in a group structure: $\forall x$ : Agent, $\forall g$ : Group, $\forall r$ : Role, plays( $x, r, g$ ) $\Rightarrow\exists gs$ : GroupStructure $\wedge$ GStruct( $g,\textit{GS}$ ) $\wedge$ roleIn( $r,\textit{GS}$ ) (5)

Figure 1 represented the Agent-Group-Role meta-model. Several notations may be used to represent organizations. In [8] a notation based on UML has been proposed to represent groups and roles. This is a very convenient notation to represent the abstract structures of an organization.

Finally, it is stated in the description of this model [6] that it is possible to define interaction relationships between roles, in order to constrain the communication performed by agents. However, no detailed explanation about the nature of these interactions is provided, leaving it as an open aspect for implementation. In the case of Agent-Group-Role, two dimensions were identified in the analysis presented in [23]. First, the notions of groups and roles compound the structural dimension. Furthermore, the definition of interactions between agents forms the dialogical dimension.

Figure 1.

The UML meta-model of Agent-Group-Role [11].

2.2 Rewriting logic and Maude formal language

Rewriting logic [17] is a logic of change that can naturally deal with state and with highly nondeterministic concurrent computations. A distributed system is axiomatized in rewriting logic by a rewrite theory R $=$ ( $\sum$ , E, R), where ( $\sum$ , E) is an equational theory describing its set of states as the algebraic data type T ${}_{\sum/E}$ associated to the initial algebra ( $\sum$ , E), and R is a collection of rewrite rules. Maude’s underlying equational logic is membership equational logic [1], a Horn logic whose atomic sentences are equalities $t=t_{0}$ and membership assertions of the form $t$ : S, stating that a term $t$ has sort S. Such a logic extends order-sorted equational logic, and supports sorts, subsort relations, subsort overloading of operators, and definition of partial functions.

Maude [25] is a high-level language and a high-performance interpreter in the OBJ algebraic specification family that supports membership equational logic [1] and rewriting logic [13] specification and programming of systems. Thus, Maude integrates an equational style of functional programming with rewriting logic computation. Because of its efficient rewriting engine, it is able to execute more than 3 million rewriting steps per second on standard PCs, and because of its meta-language capabilities, Maude turns out to be an excellent tool to create executable environments for various logics, models of computation, theorem provers, or even programming languages.

In this section those Maude’s features necessary for understanding the paper are informally described; the interested reader is referred to [25] for more details. Maude is powerful for specifying and programming systems. It is based on rewriting logic [24, 26, 12]. Maude allows describing easily the intra and inter-object concurrency. In rewriting logic, the logic formulas are called rewriting rules. They have the following forms: R: [ $t$ ] $=>$ [ $t^{\prime}$ ] or R: [ $t$ ] $=>$ [ $t^{\prime}$ ] if C. Rule R indicates that term $t$ becomes (is transformed into) $t^{\prime}$ . On its second form, a rule could not be executed except that a certain condition C is verified. Term $t$ represents a partial state of a global state S of the described system. The modification of the global state S of the system to another state S’ is realized by the parallel rewriting of one or more terms that express the partial states. The distributed state of a concurrent system is represented as a term whose sub-terms represent the different components of the concurrent state [5].

Real-Time Maude (RT-Maude) [39] is a specification language and a formal tool built as an extension of Full Maude by reflection. It provides special syntax to specify real-time systems, including distributed object-oriented ones, where the time can be either discrete or continuous. It offers a range of formal analysis capabilities, including simulation, reachability analysis, and model checking. Real-Time Maude systematically exploits the underlying Maude efficient rewriting, search, and Linear Temporal Logic (LTL) model-checking capabilities to both execute and formally analyze real-time specifications.

Ölveczky and Meseguer found a simple way to express real-time and hybrid system specifications directly in rewriting logic [14, 35, 36, 37, 39]. Such specifications are called real-time rewrite theories. The best tool currently available to specify and analyze systems as real-time rewrite theories is Real-Time Maude. For example, any rewriting logic semantics of a programming language or of a modeling language expressed in Maude or Real-Time Maude automatically provides a tool supporting simulation, reachability analysis, and Linear Temporal Logic model checking for such a language.

Authors of [14] showed also that, by making the clock an explicit part of the state, these theories can be inferred into semantically equivalent ordinary rewrite theories [36, 35, 37]. Thus, they can model the state of a real-time or hybrid system as a pair ({ $t$ }, $r_{0}$ ), with { $t$ } the current state and r0 the current global clock time. Then the above rule will be like:

$\displaystyle(\{t\},r_{0})\to(\{t^{\prime}\},r_{0}+r)\text{ if C}$ (6)

Rewrite rules can then be either instantaneous rules, that take no time and only change some part of the state $t$ , or tick rules, that advance the global time of the system according to some time expression $r$ and may also change the global state $t$ .

By characterizing the enabledness of each rule and using conditional rules and frozen operators [41], it is always possible to define tick rules so that instantaneous rules are always given higher priority; that is, so that a tick rule can never fire when an instantaneous rule is enabled [38]. When time is continuous, tick rules may be nondeterministic, in the sense that the time $r$ advanced by the rule is not uniquely determined, but is instead a parametric expression (however, this time parameter is typically subjected to some equational condition C). In such cases, tick rules need a time sampling strategy to choose suitable values for time advance.

Besides being able to show that a wide range of known real-time models (including, for example, timed automata, hybrid automata, timed Petri nets, and timed object-oriented systems) and of discrete or dense time values, can be naturally expressed in a direct way in rewriting logic (see [37]), an important advantage of the above approach is that one can use an existing implementation of rewriting logic to execute and formally analyze real-time specifications.

Of course, one would like to simulate and formally analyze real-time systems specified as real-time rewrite theories. The Real-Time Maude tool [36, 39] has been developed for this purpose. In this way, a wide range of applications, including schedulers, networks, cyber-physical systems, and real-time programming and modeling languages, have been specified, and have been formally analyzed by model checking their temporal logic properties [14].

A Real-Time Maude specification is a tuple ( $\sum$ , E, IR, TR), where:

( $\sum$ , E) is a theory in membership equational logic [4], with $\sum$ a signature and E a terminating and confluent set of conditional equations and membership axioms. ( $\sum$ , E) specifies the system’s state space as an algebraic data type.

IR is a set of conditional instantaneous rewrite rules specifying the system’s instantaneous (i.e., zero-time) local transition patterns.

TR is a set of tick rewrite rules which model the time elapse in the system and have the form:

$\displaystyle\{t\}=>\{t^{\prime}\}\text{ in time }\tau\text{ if cond}.$ (7)

where $\tau$ is a term denoting the duration of the rule, $t$ and $t^{\prime}$ are terms, and {_} is an operator encapsulating the global state, so that the form of the tick rules ensures that time advances uniformly in all parts of the system.

Intuitively, the tick rule says that it takes time $\sigma(\tau)$ to go from state { $\sigma$ ( $t$ )} to state { $\sigma$ ( $t^{\prime}$ )} for any substitution $\sigma$ of the variables in $t$ , $t^{\prime}$ , and $\tau$ that satisfies the condition cond [40].

Finally, Maude [17] is a very expressive language, which allows many different ways to represent the same concepts or the same behaviors. Each representation, although functionally and semantically equivalent, may be different regarding other non-functional aspects such as performance, readability, understandability, etc.

2.3 Rewriting logic and multi-agent system organization

There is currently few works applying rewriting logic to multi-agent system organizational models and particularly to Agent-Group-Role model. Consequently, Maude has not been used widely in the multi-agent system Organization community, and in particular not in the area of agent organizational models. Thus, the proposed rewriting logic based approach is distinguished from other works by explicitly addresses the formalization of an organizational model with Maude language. Nevertheless, some works [20, 19, 27, 33] are founded on the usage of rewriting logic and Maude in the context of agent programming languages with organizational foundation. More details on these works are given below.

Authors of [20] mention that programming language provides constructs inspired by social and organizational concepts. Depending on the scheduling mechanism of such constructs, different operational semantics can be defined. They show how one such possible operational semantics can be prototyped in Maude. According to them, prototyping by means of rewriting is important since it allows them both to design and to experiment with the language definitions. To illustrate this, authors define particular properties (like enforcement and regimentation) of the coordination artifacts which they then verify with the Maude Linear Temporal Logic model-checker. So they describe a rewrite-based framework for prototyping the language for normative multi-agent systems. Their main purpose is verification.

A very similar work of the usage of Maude in the normative multi-agent systems area is presented in [19]. The Authors present a programming language that is designed to facilitate the implementation of norm-based organization artifacts. The operational semantics of the language is prototyped in Maude and properties of the coordination artifacts are model-checked with the Maude Linear Temporal Logic model-checker.

Moreover, author of [27] focuses on organization based coordination artifacts domain. They said that a specific proposal for the design and development of exogenous coordination mechanisms for multi-agent systems is the introduction of an organization-based programming language [28, 29]. This proposed programming language is designed to facilitate the implementation of organization based coordination artifacts in terms of norms and sanctions. Such artifacts, also called “multi-agent organizations”, refer to norms as a way to signal when violations take place and sanctions as a way to respond in the case of violations. Basically, a norm-based artifact observes the actions performed by the individual agents, determines the violations caused by performing the actions, and possibly imposes sanctions. The operational semantics of this programming language makes it easy to prototype it in Maude [24]. The Maude implementation of the interpreter of this organization based coordination language [19] allows model checking organization-based programs, and in order to reason about organization-based coordination programs, a logic is devised to reason about such programs [28].

Finally, in [33] authors presents an implementation of (a simplified version of) the cognitive agent programming language 3APL in the Maude term rewriting language. According to them, Maude is based on the mathematical theory of rewriting logic. The language has been shown to be suitable both as a logical framework in which many other logics can be represented, and as a semantic framework, through which programming languages with an operational semantics can be implemented in a rigorous way. They explore the usage of Maude in the context of agent programming languages, and argue that, since agent programming languages such as 3APL have both a logical and a semantic component, Maude is very well suited for prototyping such languages. Further, they show that, since Maude is reflective, 3APL’s meta-level reasoning cycle or deliberation cycle can be implemented very naturally in Maude. Moreover, although they have implemented a simplified version of 3APL, authors argue that Maude is very well suited for implementing various extensions of this implemented version. An important advantage of Maude, besides the fact that it is well suited for prototyping agent programming languages, is that it can be used for verification as it comes with a Linear Temporal Logic model checker. Although this paper does not focus on model checking 3APL, the fact that Maude provides these verification facilities is an important motivation for their effort of implementing 3APL in Maude.

3. The proposed Agent-Group-Role formal organizational framework

3.1 Preview on the framework

While there are many useful models of multi-agent systems, they are typically defined in an informal way. Consequently, multi-agent system designers have been unable to fully exploit these models commonalities and specialize or reuse them for specific problems. In order to fully exploit these models and facilitate their reuse a formal approach is proposed based upon organizational concepts. The formal notation is the result of the composition of Maude and Agent UML formalisms. The semantics of these multi-formalisms is defined by rewriting logic. This operational semantics enables validation and verification of specifications. The proposed approach is presented through the specification of the supply chain management case study which has been used to design organizational multi-agent systems based on Agent-Group-Role model. According to [43] and the experience bear this out, that the formal specification can be used to describe model concepts which can be refined to fulfil a particular system needs.

The proposed Framework adopts a rewriting logic based approach to describe the organization constraints related to Agent-Group Role model originally present in Section 2, through the definition of a set of Maude modules (see Fig. 2). One of the benefits of such an encoding is that it is systematic. In order to describe the Agent-Group-Role model using Maude, the formal representation of the meta-model introduced in [32] will be followed, which is inspired in the Maude representation of object-oriented systems mentioned above.

Figure 2.

The formal framework modules.

Given that there are two organizational dimensions in Agent-Group-Role according to the study presented in [23]. First, the notions of groups and roles compound the structural dimension. Furthermore, the definition of interactions between agents forms the dialogical dimension. The translation with rewriting logic language will formalize Agent-Group-Role Concepts according to their corresponding dimension, in a similar way as done in [32].

Thus, In order to describe the Agent-Group-Role model in terms of rewriting logic, it is necessary, first, to define the syntax of the model, and then describe the correspondent semantics in terms of them using Maude formal language. This last is chosen as a rewriting logic language implementation since it is well-suited for prototyping Agent-Group-Role organizational model and since it comes with a Linear Temporal Logic model-checker. Furthermore, the Maude module importation helps in building up modular applications from short modules, making it easy to debug, maintain or extend. In what follows, the basic syntactic constructions which are needed for understanding how rewriting logic is being incorporated into Agent-Group-Role framework are briefly presented.

Consequently, the Agent-Group-Role model for multi-agent system Organization is prototyped in several modules: the nine first one (Module 1; until Module 9), define the syntax of the model, and the latter (Modules 10–13), implement the semantics. The following lines in Definition 1 are extracted from the syntactic modules to describe the structural dimension of Agent-Group-Role. They represent the declaration and the types on which Agent-Group-Role model depends:

Definition 1: Describing structure of system states
sorts State NameState Action Condition.
sorts GroupList Group AgentRole Message.
class Agent $\|$ CurrentState: State, PlayRole: AgentRole, GrList: GroupList, AcqList:
AcquaintanceList, MBox: MailBox.
op SendMessage: Message $\to$ Msg.
op ReceiveMessage: Message $\to$ Msg.
op TargetState: State Condition $\to$ State.

On the other hand, the semantics part is implemented by rewrite rules related to the dialogical dimension of Agent-Group-Role that help describe how the state of the organization might change over time. For space limitations reasons, one conditional rewrite rule is presented in Definition 2.

Definition 2: Specifying how the system might change
crl [Send-Cli]: Event(A, S, Cond)
$<$ A: Client $\|$ CurrentState: S, AcqList: ACL, Order: P, Deadline: D, Cost: Pr $>$
$=>$

<

A: Client

|

CurrentState: TargetState(S, Cond), AcqList: TailA(ACL), Order: P, Deadline: D, Cost: Pr

>

SendMessage(A: ActionToAccomplish(S, Cond): HeadA(ACL))

Event(HeadA(ACL), CorrespondingState(S), CorrespondingCondition(ActionToAccomplish(S, Cond)))

if (IsSendingAction(ActionToAccomplish(S, Cond))

==

true).

More details on the various syntactic and semantics modules defined in Fig. 2 are given.

3.2 Framework architecture

The proposed framework (see Fig. 2) is composed of several Maude modules: functional modules (fmod), object-oriented modules (omod), and timed object-oriented modules (tomod). However, as the schema of module is extensively used, a list of common Maude notations and operators is presented in Table 1 to describe how a module is formatted, and how to read its schema.

The framework main modules are represented below.

Firstly, the functional Module 1 describes the different states of the agent and how to go from one state to another one through actions. Indeed, agents behave according to actions in the environment or inner actions. Each time actions occur, agents move from one state to another one.

Table 1
Common notations and operators used in Maude modules

	Notations/Operators	Description
Import modules	Protecting $<$ ModuleName $>$ .	Only using without altering
	Extending $<$ ModuleName $>$ .	Only extending constructors
	Including $<$ ModuleName $>$ .	Altering behaviors of ADT and deduction rules
Abstract data	Sorts .. *** sorts Action Plan.	Give names for data types.
type (ADT)	Subsorts .. *** subsort Action $<$ Plan.	Impose orderings on sorts.
Operators	op $<$ opname $>$ : $<$ sort-1 $>$ … $<$ sort-k $>\to$	Defined on sorts (types).
	$<$ sort $>$ [ $<$ operatorattributes $>$ ].
Equations	eq [ $<$ Label $>$ ]: $<$ Term-1 $>=<$ Term-2 $>$ .	Provide the Maude interpreter with certain rules to simplify an expression.
	ceq [ $<$ Label $>$ ]: $<$ Term-1 $>=<$ Term-2 $>$ if $<$ Cond-1 $>\wedge$ … $\wedge<$ Cond-k $>$ .	Execute a reduction only if its Cond-i reduces to true.
Rewrite rules	rl [ $<$ Label $>$ ]: $<$ Term-1 $>=><$ Term-2 $>$ .	Specifying how the system might change over time.
	crl [ $<$ Label $>$ ]: $<$ Term-1 $>=><$ Term-2 $>$ if $<$ Cond-1 $>\wedge$ … $\wedge<$ Cond-k $>$ .	Cond-i is a conjunction of boolean expressions, equality tests, …
Object and class	$<$ O: C/att1 : val1,…, attn : valn $>$	O is the object identifier of sort Oid
		C is the class of the object
		att1 to attn are the attributes of the object
		val1 to valn are their current values
Message	op SendMessage: Message - $>$ Msg.	Messages are defined as terms of sort Msg.
Variables	var A: Agent.	The declaration of a variable A of sort Agent.
Tick rules	Unconditional: rl [l]: { $t$ } $=>$ { $t$ ${}^{\prime}$ } in time $\mu$ .Conditional: crl [l]: { $t$ } $=>$ { $t$ ${}^{\prime}$ } in time $\mu$	Model elapse of time in a system.The Global State of the system should always
	if cond.	have the form { $t$ }, to ensure that time advances uniformly in all parts of the system.
Functional modules	(fmod $<$ ModuleName $>$ is	Describing structure and properties of
	$<$ imports $>$ * reuse, modularity $<$ sorts $>$ * data types and subtyping $<$ ops $>$ * names/and arities of operations $<$ eqs $>$ * how to compute functions	system states (and ADT).
	endfm)
System modules	(mod $<$ ModuleName $>$ is	Defines a set of computations over the ADT specified
	*** functional part	by the functional part.
	$<$ imports $>$ * reuse, modularity $<$ sorts $>$ * data types and subtyping $<$ ops $>$ * names/and arities of operations $<$ eqs $>$ * how to compute functions	Also contain rewrite rules.
	$<$ rules $>$ endm)
Object-oriented	(omod $<$ ModuleName $>$ is	Provide syntactic sugar for object-oriented rewrite
modules	$<$ DeclarationsAndStatements $>$	theories.
	endom)
	class C $\|$ att1: s1,…, attn: sn.	Declare classes.
	subclass C $<$ C1…Cn.	Allowing subclass declarations.
Timed module	{_}: System - $>$ GlobalSystem	Automatically imports the sorts System and GlobalSystem and the operator {_}.
Timed object-	(tomod $<$ ModuleName $>$ is	Support object-oriented specification of
oriented modules	$<$ DeclarationsAndStatements $>$ endtom)	real-time systems.

Module 1: AGENT-STATE-CHART
(fmod AGENT-STATE-CHART is
sorts State NameState. sort Action. sort Condition.
op AgentState: NameState - $>$ State. op IsInternalAction: Action - $>$ Bool.
op TargetState: State Condition - $>$ State. op ActionToAccomplish: State Condition - $>$ Action.
…
endfm)

In the object oriented Module 2 the basic concept of group is defined.

Module 2: GROUP
(omod GROUP is
including STRING.
sorts GroupList Group.
subsort Group $<$ GroupList. subsort String $<$ GroupList.
op _: _: Group GroupList - $>$ GroupList. op EmptyGroupList: - $>$ GroupList.
var Gr: Group. var GrL: GroupList.
eq Gr: EmptyGroupList $=$ Gr.
endom)

The functional Module 3 is used to define the basic concept of Agent-Group-Role model which is role that agents can plays within groups.

Module 3: ROLE
(fmod ROLE is
sort AgentRole.
endfm)

The identification mechanism for agents is defined by the object oriented Module 4.

Module 4: AGENT-IDENTIFICATION
(omod AGENT-IDENTIFICATION is
sort Identifier.
subsort Oid $<$ Identifier.
endom)

For the description of the proposed message structure and the communication operations (sending/ receiving) used by agents in order to exchange messages, the object oriented Module 5 is defined, which imports Modules 1, 4 and 6.

Module 5: AGENT-MESSAGES
(omod AGENT-MESSAGES is
protecting AGENT-STATE-CHART.
protecting AGENT-IDENTIFICATION.
protecting AGENT-ACQUAINTANCES.
sort Message. sort Content.
subsort Action $<$ Content.
subsort Acquaintance $<$ Identifier.
op SendMessage: Message - $>$ Msg.
op ReceiveMessage: Message - $>$ Msg.
op _: _: _: Identifier Content Identifier - $>$ Message.
op GetIdent: Message - $>$ Identifier.
vars A A1: Identifier. var Cont: Content.
eq GetIdent (A: Cont: A1) $=$ A.
endom)

Communicating agents are generally endowed with a Mailbox containing the received messages of other agents and a list of its acquaintances. In this case, the functional Modules 6 and 7 that import the Module 5, are proposed to manage respectively Mailboxes and acquaintance lists of agents.

Module 6: AGENT-ACQUAINTANCES
(fmod AGENT-ACQUAINTANCES is
including STRING.
sorts AcquaintanceList Acquaintance.
subsort Acquaintance $<$ AcquaintanceList.
subsort String $<$ Acquaintance.
op HeadA: AcquaintanceList - $>$ Acquaintance.
op ErrorAcquaintance: - $>$ Acquaintance.
op TailA: AcquaintanceList - $>$ AcquaintanceList.
op _: _: Acquaintance AcquaintanceList - $>$ AcquaintanceList.
…
var Ac: Acquaintance. vars AcL: AcquaintanceList.
eq Ac: EmptyAcquaintanceList $=$ Ac.
eq IsEmptyAcquaintanceList(Ac: AcL) $=$ false.
eq IsEmptyAcquaintanceList(EmptyAcquaintanceList) $=$ true.
…
endfm)

Module 7: AGENT-MAIBOX
(fmod AGENT-MAILBOX is
protecting AGENT-MESSAGES.
sort MailBox. subsort Message $<$ MailBox.
op FrontMBox: MailBox - $>$ Message. op RemoveMBox: MailBox - $>$ MailBox.

op __: Message MailBox -

>

MailBox. op InsertInMBox: Message MailBox -

>

MailBox.

…

var M: Message. var MB: MailBox.

eq RemoveMBox(EmptyMailBox)

=

ErrorMailBox.

eq FrontMBox(M MB)

=

eq M EmptyMailBox

=

eq InsertInMBox(M, MB)

=

if MB

==

EmptyMailBox then M else M MB fi.

…

endfm)

In the object oriented Module 8 called AGENT-CLASS, the agents’ base class structure is defined. This class (line [1]) has as attributes: CurrentState, PlayRole, GrList, AcqList, and MBox, to contain in this order: its current state, the role played by the agent, its group list, its acquaintances and its mailbox list. This module imports Modules 1–3, 5 and 7.

Module 8: AGENT-CLASS
(omod AGENT-CLASS is
protecting AGENT-STATE-CHART.
protecting GROUP. protecting ROLE.
protecting AGENT-MESSAGES. protecting AGENT-MAILBOX.
class Agent $\|$ CurrentState: State, PlayRole: AgentRole, GrList: GroupList, AcqList: AcquaintanceList, MBox: MailBox. - - -[1]
endom)

To describe the supervisor of each agents group, the SuperAgent class is defined with the attribute Responsibility (line [1]) in the object oriented Module 9 that imports the Module 8 as a subclass of Agent class (line [2]).

Module 9: SUPERVISOR-AGENT-CLASS
(omod SUPERVISOR-AGENT-CLASS is
extending AGENT-CLASS.
sort Manager.
subsort String $<$ Manager.
class SuperAgent $\|$ Responsability: Manager. - - -[1]
subclass SuperAgent $<$ Agent. - - -[2]
endom)

AGENTI-INTRA-BEHAVIOR functional Module 10 that import Module 1 are used to illustrate agents’ system behaviors through the different states, condition and action of each agent. In order to respect interactions between these agents as illustrated in protocol diagrams, connections between them are performed through the functional Module 11. This last imports the different Module 10.

Module 10: AGENTI-INTRA-BEHAVIOR
(fmod AGENTI-INTRA-BEHAVIOR is
protecting AGENT-STATE-CHART.
*************** User Part
…
endfm)

Module 11: AGENT-INTER-BEHAVIORS
(fmod AGENT-INTER-BEHAVIORS is
protecting AGENTI-INTRA-BEHAVIOR.
…
op CorrespondingState: State - $>$ State. op CorrespondingCondition: Action - $>$ Condition.
*************** User Part
…
endfm)

Each use case defined in the different protocol diagrams is associated with one timed object- oriented Module 12, which has the same name as the corresponding use case. These modules include different rewriting rules showing the interaction scenarios between the agents. These rules may be instantaneous or tick, conditional or unconditional.

Module 12: USE-CASE_i
(tomod USE-CASE_i is
including AGENT-CLASS. including SUPERVISOR-AGENT-CLASS.
including AGENT-INTER-BEHAVIORS.
rl [1]: Configuration_1 $=>$ Configuration_2.
…
rl [m]: Configuration_2m-1 $=>$ Configuration_2m.
endtom)

Once generated, all USE-CASE_i modules are imported in the timed object oriented Module 13 which describes all system’s organizational requirements.

Module 13: AGR-BASED-MAS
(tomod AGR-BASED-MAS is
including USE-CASE_1.
…
including USE-CASE_m.
endtom)

The tick rule used to ensure the progress of time is given in Definition 3, where the message Timer is used to change the Agent clock defined by the attribute Clock (line [1]).

Definition 3: Specifying elapse of time in system.
crl [tick]: {Timer(TimeOut) - - -[1]
$<$ A: Agent $\|$ PlayRole: Initiator, Clock: T $>$ REST: Configuration} - - -[1]
$=>$ {Timer(TimeOut monus 1) $<$ A: Agent $\|$ Clock: T plus 1 $>$ REST: Configuration}
in time 1 if (TimeOut $>$ zero).

Figure 3.

The supply chain management [34].

4. Case study: Supply chain management (SCM)

4.1 Description

The development of software is a complex process, charged by the risk of making mistakes in each of the different stages. The use of formal notation since the analysis phase will reduce greatly this risk.

In the current economic climate a lot of research is presently being carried out in the domain of multi-agent systems concerning the modeling and optimization of supply chains [4]. The supply chain management [34] models the production in companies from placing an order to the delivery. This application implies receiving an order as well as generating a plan for producing this order, negotiating the price and the delay, modifying the plan if some constraints are violated, producing the product and finally, delivering it. The supply chain management considers three types of actors (see Fig. 3):

The clients who place, modify and delete orders,

The company with the customer relationships and the production and,

The providers of raw materials who are another companies.

In [4] authors said that in the literature various models of multi-agent systems for supply chain management and for modeling supply chain elements can be found, especially for companies and their various departments. A wider overview of the different solutions can be found in [42, 44]. Examples of multi-agent systems for supply chain management are presented. They are then described to consider the researched problem, the applied approach, number of agents and roles played by them. From this overview, one can notice that agents are applied to supply chain management, its construction and coordination. They are used to increase flexibility, for a better choice of business partners and to simulate the emerging global cooperation from local competition.

In order to validate the proposed approach, a simple supply chain management organization built according to Agent-Group-Role organizational model for multi-agent system development was instantiated, consisting of two agents groups. The first Group is consisted of the Client who passes, modifies and deletes the commands; Order-Acquisition; and Logistics agents. The second Group contains Scheduler; Dispatcher; Resource; Transporter; and Provider agents. Moreover, for each group a Supervisor agent is defined as shown in Fig. 4, its role is to coordinate agents group interactions.

Figure 4.

Multi-agent system structure of the supply chain management.

4.2 Agent organizational model for supply chain management

Using the elements of the Agent-Group-Role model, presented in the previous section, description of the multi-agent system for modeling and formalizing of supply chain management was done. The multi-agent system decomposition for supply chain management based on Agent-Group-Role concepts is represented by several agents regrouped in two groups as shown in Fig. 5:

Group 1 has the following agents:

Agent client represents a final customer, ordering goods produced by the company, modifying or deleting orders. It cooperates with Agent order-acquisition.

Agent order acquisition receives the orders from the agent client and negotiates the price and the delay with the agent logistics. It is responsible for the connection between clients and the company. It informs clients as soon as deliveries are postponed or delivered.

Agent logistics is the supervisor of this group to manage other agents, negotiates the delay and the price with the agent order acquisition. As soon as orders are accepted, it asks the agent scheduler to generate a plan for this order. This plan is sent to the agents transporter, resource and dispatcher. It asks for a new plan as soon as some modifications appear either if the client wants to modify the order or if some delays arise on the production. All agents, being the parts of the company, are subordinate to the Logistics agent, determining strategies and modifying the goal functions of agents.

Furthermore, Group 2 contains the five agents:

Agent scheduler is the supervisor of this second group, it generates a plan according to the order, the delay and the allocation of workers and resources.

Agent transporter is responsible for the delivery of raw materials for the production and for the delivery of the final product to the client.

Agent resource manages the allocation of materials in order to realize the order. If the materials are not available, it places an order to the agent provider.

Agent dispatcher manages worker agents. It allocates work to worker agents, and informs if some problems arise occurring a delay for the delivery.

Agent provider provide raw materials if the company has not enough materials for the order. In fact, it is an order acquisition agent from another company.

Figure 5.

Agent-Group-Role based decomposition of the supply chain management.

4.3 Agent UML diagrams for supply chain management

4.3.1 Conceptual class diagram of supply chain management

Class diagrams [34] correspond to the architecture of the system. These diagrams seem to be interesting in order to represent the different agent roles and the relations between them. UML and as a consequence Agent UML allow to represent several level of abstractions when designing class diagrams. Actually, sometimes it is not interesting to have an accurate view of the system with all the dependencies and all the attributes. High-level class diagrams allow to seize the system in its entirety. A class diagram for the conceptual level to the supply chain management example according to Agent-Group-Role model is shown in Fig. 6. A package is a standard mechanism in Agent UML for grouping elements. Indeed, in Fig. 6 one global package named Organization contains two other packages named Group 1 and Group 2 in order to regroup all the agents of the supply chain management.

Figure 6.

Agent UML conceptual class diagram of supply chain management.

Figure 7.

Supply chain management use case diagram.

4.3.2 Use case diagram of supply chain management

Use case diagrams represent the use cases, the actors, the relationships between the actors and the use cases. The main advantage of this diagram is to focus on the what and not on the how, that is to say on the system behavior and not how the system is implemented. As illustrated in Fig. 7, the eight agents of the supply chain management describe above interact with the three organizational agent use cases: Place-command, Modify-command, and Delete-command. The use case Place-command is linked to the use case Modify-command by the relationship “Include” and to Delete-command use case by the relationship “Extend”.

Figure 8.

Supply chain management protocol diagram for place-command use case [34].

4.3.3 Protocol diagram of supply chain management

Protocol diagrams [34] called Sequence diagrams in UML describe the message flow between agents. In fact, messages do not go from one agent to another one but from one role to another one. The advantage of this approach is to reduce the size of the diagram. Several works exist on protocol diagrams [15, 2] among others. Several interactions exist in the example of supply chain management give numerous protocol diagrams. Here are the lists of scenarios that give interaction protocols:

Order a product where all the agents in the multi-agent system intervene.

Modify an order where all the agents in the multi-agent system intervene.

Cancel an order where the agents client, order acquisition, and logistics, intervene.

Here the order is focused on one product. This protocol interaction is really central in the multi-agent system and all agents are used. Actually, the agent client passes an order (or command), the agent order acquisition receives the order and negotiates the price and the delay with the agent client and the agent logistics. The logistics computes the price and the delay according to the information coming from the agent scheduler. The last one needs to ask the agents transporter, resource and dispatcher for generating a plan and defining a delay.

Finally, the agent provider is called if the agent resource does not have the materials for the order. The corresponding protocol diagram is shown in Fig. 8. It is not explain in details since many messages are used. Several notions from protocol diagrams are present in this diagram:

The roles played by agents, for instance client, order acquisition, etc.

The messages between roles, for instance purchase (order, delay, price) between the agent client and the agent order-acquisition.

4.4 Application of the translation process

Given the above, the concrete multi-agent system case study based on Agent-Group-Role organizational model is instantiated with the rewriting logic based framework. This is done by applying the translation process and creating other Maude modules where the use cases presented in Fig. 7 are implemented.

The generated formal description corresponding to the translation into Maude language of the supply chain management diagrams implies all the modules cited above (see Section 3), which remain unchanged with the definition of new and extended Modules 14–18.

Module 14: SUPERVISOR-AGENTS
(tomod SUPERVISOR-AGENTS is
extending SUPERVISOR-AGENT-CLASS.
*************** User Part
subclass Logistics $<$ SuperAgent. subclass Scheduler $<$ SuperAgent.
class Logistics. class Scheduler.
endtom)

Module 15: AGENTS
(omod AGENTS is
extending AGENT-CLASS.
*************** User Part
including STRING. including NAT.
subclass Client $<$ Agent. subclass Order-Acquisition $<$ Agent.
subclass Transporter $<$ Agent. subclass Dispatcher $<$ Agent.
subclass Resource $<$ Agent. subclass Provider $<$ Agent.
class Client $\|$ Order: String, Deadline: Nat, Cost: Nat.
class Provider $\|$ PriceConstraint: Nat, Cost: Nat.
class Transporter $\|$ DelayConstraint: Nat, Deadline: Nat.
class Dispatcher $\|$ DelayConstraint: Nat, Deadline: Nat.
class Order-Acquisition. class Resource.
endom)

Module 16: PLACE-COMMAND
(tomod PLACE-COMMAND is
including NAT-TIME-DOMAIN. including AGENTS.
including SUPERVISOR-AGENTS. including AGENT-INTER-BEHAVIORS.
*************** User Part
subsort String $<$ Identifier. ops Event GetEvent: Identifier State Condition - $>$ Msg.
op Execute: Action - $>$ Msg. ops IsAcceptedDelay IsAcceptedPrice: - $>$ Msg.
ops IsRefusedDelay IsRefusedPrice: - $>$ Msg. op UpDateAcqList: MailBox - $>$ AcquaintanceList.
op SchedulePlan: - $>$ Msg. op ModifyOrder: - $>$ Msg.
…
vars A A1 A2 A3 A4 A5 A6 A7: Identifier. vars S S1 S2 S3 S4 S5: State.
vars MB: MailBox. vars ACL: AcquaintanceList.

vars Cond Cond1: Condition. var Act: Action. var M: Message.

eq UpDateAcqList(MB)

=

if MB

==

EmptyMailBox then EmptyAcquaintanceList

else GetIdent(FrontMBox(MB)): UpDateAcqList(RemoveMBox(MB))fi.

- - - - - - - - - - - - - - -

|

Sending (Agent Client)

|

- - - - - - - - - - - - - - - - - - - - - - - -

crl [Send-Cli]: Event(A, S, Cond)

<

A: Client

|

CurrentState: S, AcqList: ACL, Order: P, Deadline: D, Cost: Pr

>

=><

A: Client

|

CurrentState: TargetState(S, Cond), AcqList: TailA(ACL), Order: P, Deadline: D, Cost: Pr

>

SendMessage(A: ActionToAccomplish(S, Cond): HeadA(ACL)) Event(HeadA(ACL),

CorrespondingState(S), CorrespondingCondition(ActionToAccomplish(S, Cond)))

if (IsSendingAction(ActionToAccomplish(S, Cond))

==

true).

- - - - - - - - - - - - - - -

|

Receiving (Agent Client)

|

- - - - - - - - - - - - - - - - - - - - - - - -

crl [Receive-Cli1]: Event(A, S, Cond)

SendMessage(A1: Cont: A)

<

A: Client

|

CurrentState: S, AcqList: ACL

>

=><

A: Client

|

CurrentState: TargetState(S, Cond), AcqList: ACL

>

if (IsReceivingAction(ActionToAccomplish(S, Cond))

==

true) and (Cond

==

ReceiveAccept).

crl [Receive-Cli2]: Event(A, S, Cond)

SendMessage(A1: Cont: A)

<

A: Client

|

CurrentState: S, AcqList: ACL

>

=><

A: Client

|

CurrentState: TargetState(S, Cond), AcqList: ACL

>

ModifyOrder

if (IsReceivingAction(ActionToAccomplish(S, Cond))

==

true) and (Cond

==

ReceivePropose).

…

Module 17: ROLE
(fmod ROLE is
sort AgentRole.
*************** User Part
ops Client Order-Acquisition Logistics Scheduler Transporter Dispatcher Resource Provider: - $>$ AgentRole.
endfm)

Module 18: AGR-BASED-MAS
(tomod AGR-BASED-MAS is
including PLACE-COMMAND.
including MODIFY-COMMAND.
including DELETE-COMMAND.
endtom)

Figure 9.

Supply chain management initial configuration.

4.5 Validation of the generated description

Once the supply chain management example is encoded in Maude applying the translation process between Agent UML diagrams presented in Subsection 4.3 and the proposed framework, the result is a rewriting logic specification of the supply chain management use cases.

Maude offers tool support for interesting possibilities such as model simulation, reachability analysis and model checking [25]. Because the rewriting logic specifications produced are executable, this specification can be used as a prototype, which allows us to simulate it. Maude [17] offers different possibilities for realizing the simulation, including step-by-step execution, several execution strategies, etc. The result of the process is the final configuration of objects reached after the rewriting steps, which is nothing but a model. So, the formal specification is used in combination with Maude tool in order to generate simulation traces. Simulation is a very useful tool able to provide a first feedback about the suitability of a solution.

To validate the example of supply chain management, an initial configuration is considered where the agent Client starts by passing an order (or command) with some constraints in the delay and price product, this later finishes by satisfying the requirements of the other agents that composed the supply chain management. Figure 9 illustrates the timed O.O module SUPPLY-CHAIN-MANAGEMENT, which imports the basic module AGR-BASED-MAS of the framework to specify an initial configuration of the system. It describes supply chain management agents in their initial states.

According to the way in which the Maude rules are defined, the result of the unlimited rewriting of such a configuration is illustrated by Fig. 10. This result configuration shows all the agents in their success states which explains that the constraints imposed by the agent client have been accepted by all agents of the system.

Figure 10.

Result of the unlimited rewriting of the supply chain management initial configuration.

5. Related works

In Organization-Centered Multi-Agent System (OCMAS), there is a definition of a set of constraints that is usually described by organizational models, such as Agent-Group-Role [11], Model of Organization for multI-agent SystEms [18], and others and their associate infrastructures. The adoption of an underlying organizational model may provide the system adaptability at runtime [7].

This work is an integration of results presented in [31, 32] with additional extensions related to the description of the Agent-Group Role model. In particular, a similar approach to [32] is followed to move the knowledge of the Agent-Group-Role to a rewriting-based framework, as a step towards providing formal semantics among Agent-Group-Role based multi-agent system. To do so, a rewriting programming language must be introduced as a specification language to describe the translation process of the organizational model.

The key idea is to investigate the possibility of translating Agent-Group-Role organizational model to the Maude language that was left open in [32]. The initial work consisted in understanding the main aspects of the Agent-Group-Role organizational model and then describing it in terms of rewriting logic. The results presented in Section 4 shows that this translation is feasible, at least for this model.

Furthermore, in [20, 19, 27] authors describe the usage of rewriting logic and Maude in the context of agent programming languages with organizational foundation. These works thus differs from the proposed rewriting logic based approach in that it implements an agent programming language which already has a formal semantics, independent of Maude. Consequently, its techniques for implementation are based on the idea that transition rules can be translated into rewrite rules.

Another example of the usage of Maude in the context of agent programming languages area is presented in [33]. In this work, authors remark that, since agent programming languages such as 3APL have both a logical and a semantic component, Maude is very well suited for prototyping such languages. Moreover, although they have implemented a simplified version of 3APL, authors argue that Maude is very well suited for implementing various extensions of this implemented version. An important advantage of Maude, besides the fact that it is well suited for prototyping 3APL, is that it can be used for verification as it comes with a Linear Temporal Logic model checker.

6. Conclusion

Several methods describing multi-agent system organizational requirements are proposed. However, they only offer informal or semi-formal descriptions. In this paper, an approach which allows specification and validation of organization-centered multi-agent system is presented. More precisely, a particular organizational multi-agent system model is specified. This formalization shows that this approach can be applied to organizational models that were not formally analyzed at the beginning. The proposed approach allows capturing functional, static, and dynamic aspects of multi-agent system based on Agent-Group-Role organizational model using Agent UML diagrams, and then translating this graphical description in Maude.

Thus, a rewriting logic based approach is applied to specify formally this model. The advantages of the approach are, first, that the Agent-Group-Role model is presented in formal and non ambiguous terms and second that the specification decomposes the model in formal concepts which can be reused in specific applications. So, using formal notations to specify Agent-Group-Role model makes it possible to produce precise organizational descriptions. This also offers a better support to their verification and validation processes. The validation phase enables specifications simulation with predefined interaction scenarios such as the supply chain management case study. Also the specification of others organizational multi-agent models is planed following the process described in this paper. This will constitute a library of reusable generic multi-agent models.

Furthermore, the possibility of including a temporal dimension to deal with agents temporal constraints issues must be investigated to specify the concrete model of Real-Time Multi-Agent System through Real-Time Maude language. This is the first step in achieving organizational formalization through a rewriting logic based language. Further work will follow this way by analyzing temporal organizational concepts of real-time multi-agent system.

Footnotes

Authors’ Bios

Mohamed Amin Laouadi is an Assistant Professor at the Department of Computer Science of the University of Ferhat Abbas Setif 1, Setif in Algeria. He holds the Magister in Computer Science (Artificial Intelligence) from the University of Badji Mokhtar Annaba (Algeria) in 2010. Currently, he is a PhD student at University of Annaba. His main areas of interest include agent-oriented software engineering, multi-agent system and formal methods.

Farid Mokhati is a Professor of Computer Science at the Department of Mathematics and Computer Science of the University of Oum El-Bouaghi in Algeria. He holds a University accreditation (Habilitation Universitaire) in Computer Science (Distributed Artificial Intelligence) awarded by BADJI Mokhtar University (Annaba) in Algeria. Currently, he is the head of ReLa(CS)2 Laboratory and the head of DISE team (Distributed-Intelligent Systems Engineering). His main areas of interest include object and agent-oriented software engineering and formal methods.

Hassina Seridi-Bouchelaghem is a Professor of Computer Science at the Department of Computer Science of the University of Badji Mokhtar Annaba in Algeria. She received her Master’s in Computer Science and Engineering from Badji Mokhtar University in 1997 and PhD in Computer Science and Engineering in 2006. Currently, she is the Head of the team ‘TEL, Data mining and Web Technology’ at LabGED Laboratory. She has broad interests in information system on the web and especially service web, software engineering, Social semantic web, e-learning application, recommender systems.

References

Bouhoula

Jouannaud

J.P.

and Meseguer

, Specification and proof in membership equational logic, in: Theoretical Computer Science 236(1-2) (2000), 35–132.

Bauer

Muller

J.P.

and Odell

, An extension of UML by protocols for multi-agent interaction, in: International Conference on Multi-Agent Systems (ICMAS’00), Boston Massachussetts, USA, July 2000, 207–214.

Lemaître

and Excelente

C.B.

, Multi-agent organization approach, in: Proceedings 2nd Iberoamerican Workshop on Distributed Artificial Intelligence and Multi-Agent Systems, Toledo, USA, 1998, 7–16.

Nawarecki

and Koźlak

, Building multi-agent models applied to supply chain management, Control and Cybernetics 39(1) (2010), 149–176.

Mokhati

Badri

and Zerrougui

, A novel conformance testing technique for agent interaction protocols, in: Proceedings of Science and Information Conference (SAI), London UK, 7–9 October 2013, 485–495.

Muramatsu

F.T.

Vitorello

T.M.

and Brandao

A.A.F.

, Towards organizational interoperability through artifacts, in: Agent Environments for Multi-Agent Systems – 10 Years Later, 2014, Paris. E4MAS @ AAMAS-2014 Agent Environments for Multi-Agent Systems – 10 Years Later. IFAAMAS, Liverpool, UK, 2014, 1–14.

Muramatsu

F.T.

Vitorello

T.M.

and Brandao

A.A.F.

, Towards organizational interoperability through the environment, in: Revised Selected and Invited Papers of the 4th International Workshop on Agent Environments for Multi-Agent Systems IV, Springer-Verlag, New York, USA, 2014, 209–231.

Parunak

H.V.D.

and Odell

, Representing social structure in UML, in: Agent-Oriented Software Engineering II, Springer, Montreal, Canada, 2002, 1–16.

Ferber

and Perrot

J.F.

, Les systèmes multi-agents: Vers une intelligence collective, Inter-Editions, 1995.

10.

Ferber

and Gutknecht

, A meta-model for the analysis and design of organizations in MAS, in: Proceedings of Third International Conference on Multi Agent Systems, IEEE Press, July 1998, 128–135.

11.

Ferber

Gutknecht

and Michel

, From agents to organizations: An organizational view of multi-agent systems, in: International Workshop on Agent-Oriented Software Engineering, Springer, Berlin Heidelberg, Germany, 2003, 214–230.

12.

Meseguer

, Rewriting as a unified model of concurrency, in: ACM SIGPLAN OOPS Messenger, New-York, USA 2(2) (1991), 86–88.

13.

Meseguer

, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science 96(1) (1992), 73–155.

14.

Meseguer

, Twenty years of rewriting logic, The Journal of Logic and Algebraic Programming 81(7–8) (2012), 721–781.

15.

Odell

Parunak

H.V.D.

and Bauer

, Extending UML for agents, in: Proceedings of the Agent-Oriented Information Systems Workshop at the 17th National conference on Artificial Intelligence Wagner

et al, eds, ICue Publishing, Austin, Texas USA (July 2000), pp. 3–17.

16.

Pavon

Fuentes

and Gomez

, The INGENIAS methodology and tools, in: Agent-Oriented Methodologies, IGI Global (2005), 236–276.

17.

Troya

and Vallecillo

, A rewriting logic semantics for ATL, Journal of Object Technology 10(5) (2011), 1–29.

18.

Hübner

J.F.

Bordini

R.H.

and Picard

, A model for the structural, functional, and deontic specification of organizations in multiagent systems, in: Proceedings of the 16th Brazilian Symposium on Artificial Intelligence (SBIA’02), Springer, Berlin Heidelberg, Germany, 2002, 118–128.

19.

Astefanoaei

Dastani

Meyer

J.J.C.

and de Boer

F.S.

, A verification framework for normative multi-agent systems, in: Proceedings of 11th Pacific Rim International Conference on Multi-Agents (PRIMA), Hanoi, Vietnam (15–16 December 2008), 54–65.

20.

Astefanoaei

Dastani

Meyer

J.J.C.

and de Boer

F.S.

, On the semantics and verification of normative multi-agent systems, in: J UCS 15(13) (2009), 2629–2652.

21.

Gasser

, Organizations in multi-agent systems, in: Pre-Proc of the 10th European Worshop on Modeling Autonomous Agents in a Multi-Agent World (MAAMAW’2001), Annecy, France, 2001.

22.

Coutinho

L.R.

Sichman

J.S.

and Boissier

, Modeling organization in MAS: A comparison of models, in: First Workshop on Software Engineering for Agent-Oriented Systems (SEAS’05) (2005), 1–10.

23.

Coutinho

L.R.

Sichman

and Boissier

, Modelling dimensions for agent organizations, in: Dignum

, ed, Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models 2 (2009), pp. 18–50.

24.

Clavel

Duran

Eker

Lincoln

Marti-Oliet

Meseguer

and Talcott

, All about Maude – a high-performance logical framework, LNCS 4350 (2007).

25.

Clavel

Duran

Hendrix

Lucas

Meseguer

and Ölveczky

, The Maude formal tool environment manuel, in: International Conference on Algebra and Coalgebra in Computer Science, Springer, Berlin Heidelberg, Germany (2007), 173–178.

26.

Clavel

Duran

Eker

Escobar

Lincoln

Marti-Oliet

Meseguer

and Talcott

, Maude Manual (version 2.7.1), SRI International, Menlo Park, USA, CA 94025 (2016).

27.

Dastani

, Programming multi-agent systems, in: International Workshop on Computational Logic in Multi-Agent Systems, Springer, Berlin Heidelberg, Germany (2008), 13–16.

28.

Dastani

Grossi

Tinnemeier

and Meyer

J.J.

, Normative multi-agent programs and their logics, in: Proceedings of First International Workshop, KRAMAS, Sydney Australia (17 September 2008), 16–31.

29.

Dastani

Tinnemeier

and Meyer

J.J.

, A programming language for normative multi-agent systems, in: Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models, IGI Global (2009), 397–417.

30.

Wooldridge

Jennings

N.R.

and Kinny

, The Gaia methodology for agent-oriented analysis and design, Journal of Autonomous Agents and Multi-Agent Systems 3(3) (2000), 285–312.

31.

Laouadi

M.A.

Mokhati

and Seridi-Bouchelaghem

, Towards an organizational model for real time multi-agent system specification, in: Proceedings of Science and Information Conference (SAI), London UK (7-9 October 2013), 577–584.

32.

Laouadi

M.A.

Mokhati

and Seridi-Bouchelaghem

, A novel organizational model for real time MAS: Towards a formal specification, in: Chen

et al, eds, Intelligent Systems for Science and Information, Studies in Computational Intelligence 542 (2014), pp. 171–180.

33.

Van Riemsdijk

M.B.

De Boer

F.S.

Dastani

and Meyer

J.J.C.

, Prototyping 3APL in the Maude term rewriting language, in: Proceedings of the 7th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA VII), Hakodate, Japan (8–9 May 2006), 95–114.

34.

Huget

M.P.

, An application of agent UML to supply chain management, in: Proceedings of Agent Oriented Information System (AOIS-02) Giorgini

et al. eds, (short presentation of the technical report ULCS-02-015), Bologne, Italie, 2002.

35.

Ölveczky

P.C.

and Meseguer

, Specifying real-time systems in rewriting logic, Electronic Notes in Theoretical Computer Science 4 (1996), 284–309.

36.

Ölveczky

P.C.

, Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic, Ph.D. thesis, University of Bergen, Norway, 2000.

37.

Ölveczky

P.C.

and Meseguer

, Specification of real-time and hybrid systems in rewriting logic, Theoretical Computer Science 285(2) (2002), 359–405.

38.

Ölveczky

P.C.

and Meseguer

, Real-Time Maude 2.1, Electronic Notes in Theoretical Computer Science 117 (2005), 285–314.

39.

Ölveczky

P.C.

and Meseguer

, Semantics and pragmatics of real-time Maude, Higher-Order and Symbolic Computation 20(1–2) (2007), 161–196.

40.

Ölveczky

P.C.

and Meseguer

, The real-time Maude tool, in: TACAS 8 (2008), 332–336.

41.

Bruni

and Meseguer

, Generalized rewrite theories, in: ICALP 3 (2003), 252–266.

42.

Moyaux

T.H.

Chaib-Draa

and D’Amours

, Supply chain management and multiagent systems: An overview, in: Chaib-Draa

and Muller

, eds, Multiagent Based Supply Chain Management, Studies in Computional Intelligence 28 (2006), pp. 1–27.

43.

Hilaire

Simonin

Koukam

and Ferber

, A formal approach to design and reuse agent and multiagent models, in: Proceedings of Agent-Oriented Software Engineering V, 5th International Workshop, AOSE, New York, USA (2004), 142–157.

44.

Shen

and Norrie

D.H.

, Agent-based systems for intelligent manufacturing: A state-of-the-art survey, Knowledge and Information Systems 1(2) (1999), 129–156.

A formal framework for organization- centered multi-agent system specification: A rewriting logic based approach

Abstract

Keywords

1. Introduction

2. Literature review

2.1 Agent-Group-Role organizational model

3. The proposed Agent-Group-Role formal organizational framework

3.1 Preview on the framework

Table 1 Common notations and operators used in Maude modules

4.1 Description

4.3.1 Conceptual class diagram of supply chain management

4.4 Application of the translation process

6. Conclusion

Footnotes

Authors’ Bios

References

Table 1
Common notations and operators used in Maude modules