An Integrated Semantics of Social Commitments and Associated Operations

Abstract

-In this paper, we develop a unified semantic model for social commitments and associated operations. We propose a logical model based on CT L¤ with modalities of commitments and associated operations that represent the dynamic behavior of agents. Our semantics differs from the previous proposals in which the operations used to manipulate commitments (e.g. creation, fulfillment, violation, withdrawn, etc.) have always been defined as axioms or constrains on top of the commitment semantics. The advantage of this logical model is to gather the direct semantics of these operations and the semantics of social commitments (propositional and conditional) within the same framework. Furthermore, this paper proposes a new definition of assignment and delegation operations by looking at the content of the assigned and delegated commitment that could be different from the content of the original commitment in terms of deadline. Finally, to stress the soundness of the model, we prove that the proposed semantics satisfies some properties that are desirable when modeling commitment-based multiagent systems.

I. INTRODUCTION

The importance of defining suitable and formal semantics of social commitments has been broadly recognized for multiagent systems. Particulary, social commitments have been used for agent communication, coordination and artificial institutions [ 22 ]. In communication protocols, commitments can capture a high level meaning of interaction as opposed to lowlevel operational representation [ 24 ], [ 14 ], [ 9 ]. However, the meanings of messages exchanged between interacting agents can also be interpreted directly into social commitments in an operational semantics style [ 11 ], [ 6 ].

Some interesting semantic frameworks for social commitments have already been proposed using different approaches such as branching time logics (CT L¤ and CT L§) [ 2 ], [ 3 ], [ 13 ], [ 19 ], [ 25 ]. Recently, a model-theoretic semantics of social and dialogical commitments based on linear-time logic (LT L) has been introduced in [ 20 ] and the proposed postulates are reproduced in [ 7 ] to define semantics of commitment operations in distributed systems.

In general, two categories of semantic frameworks for social commitments can be distinguished. In the former category, commitment operations are formalized based on Singh’s presentation [ 18 ] as axioms or constraints on top of commitment semantics [ 6 ], [ 9 ], [ 13 ], [ 14 ], [ 24 ]. These axioms are represented either as reasoning rules, updating rules or enforcing rules to evolve the truth of commitments’ states. However, the real meanings of commitment operations themselves (e.g. Create, Fulfill, etc.) are not captured. In the later category, social commitments are formalized using object-oriented paradigm to advance the idea of commitments as data structure [ 11 ]. Thus, the main objective of defining clear, practical, and verifiable semantics of commitments and associated operations in the same framework is yet to be reached.

The objective of this paper aims to propose a new semantics not only for social commitments, but also for all the operations used to manipulate commitments. For verification issues and development methodologies of agent-oriented software engineering, the semantics of these operations should not be only captured by some enforced rules like in [ 13 ], but also integrated in the same framework [ 15 ]. In essence, this work is a continuation of our two previous publications [ 3 ], [ 15 ]. In the former one [ 3 ], we have developed a framework unifying commitments, actions on commitments and arguments that agents use to support their actions. In the second one [ 15 ], we have proposed a new logical semantics of social commitments and associated two-party operations based on Branching Space-Time (BST) logic. BST-logic provides this semantics with agent life cycle, space-like dimension and causal relation between interacting agents in the same (physical or virtual) space. Specifically, here we refine the semantics of some operations (e.g., Create, Withdraw, Fulfill) to overcome the state explosion problem that arises in [ 3 ], complete the life cycle of commitment operations introduced in [ 15 ], and define a new semantics of multi-party operations, such as Delegate and Assign using an extension of CT L¤.

The primary contribution of this paper is the unified logical model for commitments and associated operations. In fact, the paper introduces a new semantics of withdrawal, fulfilment, violation and release operations using the notions of accessible and non-accessible paths. New definitions of assignment and delegation operations are also proposed by taking into account the fact that the assigned and delegated commitment’s deadline could be different form the deadline of the original commitment. Some desirable properties such as “the same social commitment (with the same identifier) cannot be created twice” or “if it is fulfilled, the commitment cannot be fulfilled again or withdrawn in the future” are captured, which makes the model sound. The proposed logical model uses a Kripke-like computational structure where accessibility relations for commitment modalities are defined using a computational interpretation, which makes our semantics computationally grounded [ 23 ] (this idea will be detailed later). This compotional interpretation is suitable for formal verification using model checking to verify interacting agentbased systems against given properties [ 4 ], but model checking algorithm is out of scope of this paper. Furthermore, the logical model presented here is expressive because the content of commitments are CTL*-like path formulae [ 10 ] and not state formulae and their semantics is expressed in terms of accessible paths and not in terms of deadlines.

The remainder of this paper is organized as follows. Section II describes the notion of social commitment and its formal notation extended from [ 15 ]. Given this context, Section III presents the syntax and semantics of the main elements of our logical model. Subsequently, Section IV proves some logical properties based on the defined semantics. Finally, the paper ends in Section V with a discussion of related work.

II. SOCIAL COMMITMENTS

A. Formal Notation

A commitment is an engagement made by one agent, the debtor, and directed towards another agent, the creditor, so that some fact is true. The debtor must respect and behave in accordance with his commitments. These commitments are contextual, manipulable and possibly conditional [ 18 ]. Furthermore, commitments are social and observable by all the participants. Consequently, social commitments (SC) are different from the agent’s private mental states like beliefs, desires and intentions. Several approaches assume that agents will respect their commitments. However, this assumption is not always guaranteed in real-life scenarios (e.g in e-business) since violation can occur if agents are malicious, deceptive, malfunctioning or not reliable. Thus, it is natural to introduce violation operation of social commitments along with their satisfaction. We can also use a legal context of commitments to define rules that impose penalties on the debtors that violate their commitments. Below, we distinguish between two types of social commitments: propositional and conditional.

Definition 1: Propositional social commitments are related to the state of the world and denoted by SCp(id; Ag1; Ag2; Á) where id is the commitment’s identifier, Ag1 is the debtor, Ag2 is the creditor and Á is a well-formed formula (expressed in some logics) representing the commitment content.

The basic idea is that Ag1 is committed towards Ag2 that the propositional formula Á is true. We suppose that the identifier id is unique so that there is at most one commitment with a particular identifier. In several situations, agents can only commit when some conditions are satisfied. Conditional commitments are introduced to capture this issue.

Definition 2: Conditional social commitments are denoted by SCc(id; Ag1; Ag2; ¿; Á) where id; Ag1; Ag2; and Á have the same meanings as in Def.1 and ¿ is a well-formed formula representing the condition.

B. Social Commitment Life Cycle

Having explained the formal definitions of commitments, in this section we present their life cycle to specify the relationship between commitments’ states. Figure 1 describes this life cycle using UML state diagram. The life cycle proceeds as follows: ² The commitment could be conditional or unconditional (i.e. propositional). This is represented by the selection operator. The first operation an agent can perform on a commitment is creation. When created, a conditional commitment can move to the state of created unconditional commitment if the condition is true. Otherwise, the conditional commitment moves to the final state. ² When the unconditional commitment is created, then it may move to one of the following states: fulfilled, violated, withdrawn, released, delegated or assigned. ² The commitment can be withdrawn if the debtor decides to cancel it. Only the debtor is able to perform this action without any intervention from the creditor. ² The commitment is fulfilled if its content is satisfied by the debtor. ² The social commitment is violated if its content is violated by the debtor. ² The social commitment can be released by the creditor so that the debtor is no longer obliged to carry out his commitment.

Created Conditional commitment

Selection [Delegate_new _ debtor] [Assign_new_creditor] Condition [condition_ met]

Created

Uncoditional commitment [has_been_Released] [condition_ not_ met]

[has_been_Violated] [has_been_Fulfil ed] [has_been_Withdrawn] [has_been _Delegated] [has_been_ Assigned] Released

Fulfilled

Violated

Withdrawn

Delegated

Assigned

Legend Debtor's action Creditor's action ² The social commitment can be assigned by the creditor, which results in releasing this creditor from the commitment and having a new unconditional commitment with a new creditor. ² The social commitment can be delegated by the debtor, which results in withdrawing this debtor from the commitment and delegating his role to another debtor within a new commitment.

III. LOGICAL MODEL OF SOCIAL COMMITMENTS

This section introduces the syntax and semantics of the different elements of our formal language L. This propositional language uses extended Computation Tree Logic (CTL*)[ 10 ] with past operators and two additional modalities SCp for propositional and SCc for conditional commitments, and Act for actions applied to commitments. We refer to the resulted branching time logic as CT L¤sc. The time in our model is discrete and branching in future to represent all choices that agents have when they participate in conversations and linear in the past. On the other hand, the dynamic behavior of agents is captured by actions these agents perform on different commitments during conversations.

A. Syntax

Let ©p be a set of atomic propositions and ID be a set of identifiers. AGT is a set of agent names and ACT is a set of actions used to manipulate commitments (e.g. Create, Fulfill, etc.). L and Act are nonterminals corresponding to L and ACT , respectively. Furthermore, we use the following conventions: id; id0; id1, etc. are unique commitment identifiers in ID, Ag1; Ag2; Ag3, etc. are agent names in AGT , p; q, etc. are atomic propositions in ©p and Á; Ã, etc. are formulae in L. Table I gives the formal syntax of L expressed in Backus-Naur Form (BNF) grammar where “!” and “j” are meta-symbols of this grammar.

L1. L ! C j Act j p j :L j L _ L j X+L j X¡L j L U +L j

L U ¡L j AL j EL L2. C ! SCp(id; Ag1; Ag2; L) j SCc(id; Ag1; Ag2; L; L) L3. Act ! Create(Ag; C) j F ulf ill(Ag; C) j V iolate(Ag; C) j W ithdraw(Ag; C) j Release(Ag; C) j Assign(Ag1; Ag2; C) j Delegate(Ag1; Ag2; C)

The intuitive meanings of the most constructs are straightforward (from CTL* with next (X+), previous (X¡), until (U +), and since (U ¡) operators). A and E are the universal and existential path-quantifiers over the set of all paths starting from the current moment. AÁ (resp. EÁ) means that Á holds along all (some) paths starting at the current moment. Furthermore, there are some useful abbreviations based on temporal operators (X+; X¡; U +; U ¡): (sometimes in the future) F +Á , true U +Á; (sometimes in the past) F ¡Á , true U ¡Á; (globally in the future) G+Á , :F +:Á and (globally in the past) G¡Á , :F ¡:Á. We also introduce L¡ ½ L as the subset of all formulae without temporal operators.

B. Semantics of CT L¤sc

1) The formal model:

Our model M for L is based on a Kripke-like structure with seven-tuple, M = hS; T; R; V; Rscp; Rscc; Fi, where: ² S = fs0; s1; s2; : : :g is a set of states. ² T : S ! T P is a function assigning to any state the corresponding time stamp where T P is a set of time points. ² R µ S £ S is a total transition relation, that is, 8si 2 S; 9 sj 2 S : (si; sj ) 2 R, indicating branching time. If there exists a transition (si; sj ) 2 R, then we have T (si) < T (sj ). A path P is an infinite sequence of states P = hs0; s1; s2; : : :i where 8 i 2 N; (si; si+1) 2 R. We denote the set of all paths by ¾ and the set of all paths starting at si by ¾si . ² V : ©p ! 2S is a valuation function that assigns to each atomic proposition a set of states where the proposition is true. ² Rscp : S £ AGT £ AGT ! 2¾ is a function producing an accessibility modal relation for propositional commitments. ² Rscc : S £ AGT £ AGT ! 2¾ is a function producing an accessibility modal relation for conditional commitments. ² F : L ! L¡ is a function associating to each formula in

L a corresponding formula in L¡.

The function Rscp associates to a state si the set of paths starting at si along which an agent commits towards another agent. These paths are conceived as merely “possible”, and as paths where the commitments’ contents made in si are true. The computational interpretation of this accessibility relation is as follows: the paths over the model M are seen as computations, and the accessible paths from a state si are the computations satisfying (i.e. computing) the formulae representing the contents of the commitments made at that state by a given agent towards another given agent. For example, if we have: P 0 2 Rscp(si; Ag1; Ag2), then the commitments that are made in the state si by Ag1 towards Ag2 are satisfied along the path P 0 2 ¾si .

Rscc is similar to Rscp and it gives us the paths along which the resulting unconditional commitment is satisfied if the underlying condition is true. Because it is possible to decide if a path satisfies a formula (see the semantics in this section), the model presented here is computationally grounded [ 23 ]. In fact, the accessible relations map commitment content formulae into a set of paths that simulate the behavior of interacting agents. The logic of propositional and conditional commitments is KD4 modal logic and the accessibility modal relations Rscp and Rscc are serials [ 3 ]. The function F is used to remove the temporal operators from a formula in L. For example: F(X+X+p) = p and F(SCp(id; Ag1; Ag2; X+q)) = SCp(id; Ag1; Ag2; q).

2) Semantics of social commitments:

Having explained our formal model, in this section we define the semantics of the elements of L relative to a model M , state si, and path P . The notation hsi; P i refers to the path P starting at si meaning that P 2 ¾si where P = hsi; si+1; si+2; : : :i. If P is a path starting at a given state si, then prefix of P starting at a state sj (T (sj ) < T (si)) is a path denoted by P # sj and suffix of P starting at a state sk (T (si) < T (sk)) is a path denoted by P " sk. Because the past is linear, sj is simply a state in the unique past of si such that P is a part of P # sj . sk is in the future of si over the path P such that P " sk is part of P . If si is a state, then we assume that si¡1 is the previous state in the linear past ((si¡1; si) 2 R) and si+1 is the next state on a given path ((si; si+1) 2 R).

In the metalanguage, we use the following symbols: & means “and”, , means “is equivalent to” and ) means “implies that”. The logical equivalence is denoted ´. As in CT L¤, we have two types of formulae: state formulae evaluated over states and path formulae evaluated over paths [ 10 ]. M; hsii j= Á means “the model M satisfies the state formula Á at si”. M; hsi; P i j= Á means “the model M satisfies the path formula Á along the path P starting at si”. A state formula Á is satisfiable iff there are some M and si such that M; hsii j= Á. A path formula Á is satisfiable iff there are some M , P , and si such that M; hsi; P i j= Á. A state formula is valid when it is satisfied in all models M , in all states si in M . A path formula is valid when it is satisfied in all models M , in all paths P in M , in all states si. The formal semantics of CT L¤ and SCp, SCc modalities of our model is illustrated in Table II.

M1. M; hsii j= p iff si 2 V(p) where p 2 ©p M2. M; hsii j= : Á iff M; hsii 2 Á M3. M; hsii j= Á _ Ã iff M; hsii j= Á or M; hsii j= Ã M4. M; hsii j= AÁ iff 8 P 2 ¾si : M; hsi; P i j= Á M5. M; hsii j= EÁ iff 9 P 2 ¾si : M; hsi; P i j= Á M6. M; hsii j= SCp(id; Ag1; Ag2; Á) iff

8 P 2 Rscp(si; Ag1; Ag2) M; hsi; P i j= Á M7. M; hsii j= SCc(id; Ag1; Ag2; ¿; Á) iff 8 P 2 Rscc(si; Ag1; Ag2) M; hsi; P i j= ¿ ) M; hsi; P i j= SCp(id; Ag1; Ag2; Á) M8. M; hsi; P i j= Á iff M; hsii j= Á M9. M; hsi; P i j= : Á iff M; hsi; P i 2 Á M10. M; hsi; P i j= Á _ Ã iff M; hsi; P i j= Á or M; hsi; P i j= Ã M11. M; hsi; P i j= X+Á iff M; hsi+1; P " si+1i j= Á M12. M; hsi; P i j= Á U + Ã iff 9 j ¸ i : M; hsj ; P " sj i j= Ã & 8 i · k < j M; hsk; P " ski j= Á M13. M; hsi; P i j= X¡Á iff M; hsi¡1; P # si¡1i j= Á M14. M; hsi; P i j= Á U ¡ Ã iff 9 j · i : M; hsj ; P # sj i j= Ã & 8 j < k · i M; hsk; P # ski j= Á

The semantics of state formulae is given from M 1 to M 7 and that of path formulae is given from M 8 to M 14. For space limit reasons, we only explain the semantics of formulae that are not in CTL*. M 6 gives the semantics of propositional commitment operator, where the state formula is satisfied in the model M at si iff the content Á is true in all accessible paths P starting at si. Similarly, M 7 gives the semantics of conditional commitment operator, where the state formula is satisfied in the model M at si iff in all accessible paths P if the condition ¿ is true, then the underlying unconditional commitment is also true. The semantics of past operators X ¡ and U ¡ is given by considering the linear past of the current state si as prefix of the path P .

3) Semantics of actions on social commitments:

Having defined the semantics of commitments, below we define the semantics of operations used to manipulate those commitments and support flexibility. These operations are of two categorizes: two-party operations: Create, Withdraw, Fulfill, Violate and Release, and three-party operations: Assign and Delegate because Assign and Delegate need a third agent to which the new commitment is assigned or delegated. The context and detailed exposition of these operations are given in [ 13 ], [ 14 ], [ 18 ]. To simplify the notations used in the semantics, we suppose that these actions are momentary and do not need time to be performed.

Technically, this can be represented by allowing actions to be performed on states or by supposing that transitions labeled by these actions are connecting two states si and sj having the same time stamp (T (sj ) = T (si)). The first possibility is adopted in this paper. Although actions are momentary, action formulae are evaluated over paths. This is compatible with the philosophical interpretation of actions, according to which, by performing an action the agent selects a path or history among the available paths or histories at the moment of performing the action.

Creation action: the semantics of creation action of a propositional commitment (see Table III) is satisfied in the model M at state si along path P iff (i) the commitment is established in si (as a result of performing the momentary creation action); and (ii) the created commitment was not established in the past.

M15. M; hsi; P i j= Create(Ag1; SCp(id; Ag1; Ag2; Á)) iff (i) M; hsi; P i j= SCp(id; Ag1; Ag2; Á) & (ii) 8 j < i; M; hsj i j= :SCp(id; Ag1; Ag2; Á)

The semantics of creation action of a conditional commitment (see Table IV) is defined in the same way.

M16. M; hsi; P i j= Create(Ag1; SCc(id; Ag1; Ag2; ¿; Á)) iff (i) M; hsi; P i j= SCc(id; Ag1; Ag2; ¿; Á) & (ii) 8 j < i; M; hsj i j= :SCc(id; Ag1; Ag2; ¿; Á)

Example 1: Let us consider a simple and modified case of NetBill protocol to illustrate the semantics of different action formulae. A customer (Cus) requests a quote for some goods (rfq), followed by the merchant (M er) sending the quote as an offer. If the customer pays for goods, then the merchant will deliver the goods, withdraw (within a specified time), or not deliver. The customer can also release after receiving the quote (see Fig.2).

The offer message at state s2 means that M er creates a conditional commitment Create(M er; SC c(id; M er; Cus; pay; delivergoods)) meaning that if the payment is received, then M er commits to deliver the goods to Cus. hs2; s3; s4; : : : i, hs2; s3; s5; s6; : : : i and hs2; s3; s5; s8; : : : i are not accessible paths for this commitment (i.e. are not in Rscc(s2; M er; Cus). However, hs2; s3; s5; s7; : : : i is an accessible path (i.e. is in Rscc(s2; M er; Cus). As the condition is true through hs2; s3; s5; s7; : : : i (the customer pays), the conditional commitment becomes unconditional: SCp(id; M er; Cus; delivergoods) along the same accessible path. Before creating this unconditional commitment, M er checks that it has not been created before, as there is no reason to create the same commitment twice.

Withdrawal action: the semantics of withdrawal action of a propositional commitment (see Table V) is satisfied in the model M at si along path P iff (i) the commitment was created in the past at sj through the prefix P # sj ; (ii) this prefix is not one of the accessible paths via Rscp; and (iii) at the current state si, there is still a possibility of satisfying the commitment since there is a path P 0 whose the prefix P 0 # sj is still accessible using Rscp. Note that the first argument of Rscp is sj where the commitment has been created. This is because the accessible paths start from the state where the commitment is created. Intuitively, when a commitment is withdrawn along a path, the prefix of this path from the creation state does not correspond to an accessible path (condition ii).

M17. M; hsi; P i j= W ithdraw(Ag1; SCp(id1; Ag1; Ag2; Á)) iff (i) 9j < i : M; hsj ; P # sj i j= Create(Ag1; SCp(id1; Ag1; Ag2; Á))& (ii) P # sj 2= Rscp(sj ; Ag1; Ag2) & (iii) 9 P 0 2 ¾si : P 0 # sj 2 Rscp(sj ; Ag1; Ag2)

Furthermore, a commitment can be withdrawn when its satisfaction is still possible (condition iii), which is captured by the existence, starting at the current moment, of an accessible path the agent can choose (see Fig.3). In other words, the agent Ag1 has another choice at the current state, which is continuing in the direction of satisfying its commitment. We also note that withdrawing a commitment does not mean its content is false. For instance it can be accidentally true even if the current path is not amongst the accessible ones.

Withdraw and Release actions at the state si along the path P

Example 2: The merchant M er, before delivering the goods to Cus, can withdraw the offer. Thus, there is no accessible path for the commitment between M er and Cus at s6. At the same time, M er still has a possibility to satisfy its offer at state s5 through the accessible paths hs2; s3; s5; s7; : : : i.

Fulfillment action: the semantics of fulfillment action (see Table VI) is defined in the same way as withdrawal. In (ii), the prefix P # sj of the current path P (along which the commitment has been created) is accessible using Rscp; and in (iii), at the current state si, there is still a possible choice of not satisfying the commitment since a non-accessible path P 0 # sj exists. We notice that being accessible means that the content Á is true along P # sj . As for withdrawal, fulfillment action makes sense only when a non-fulfilment action is still possible.

M18. M; hsi; P i j= F ulf ill(Ag1; SCp(id; Ag1; Ag2; Á)) iff (i) 9 j < i : M; hsj ; P # sj i j= Create(Ag1; SCp(id; Ag1; Ag2; Á)) & (ii) P # sj 2 Rscp(sj ; Ag1; Ag2) & (iii) 9 P 0 2 ¾si : P 0 # sj 2= Rscp(sj ; Ag1; Ag2)

Example 3: When the customer Cus pays for the goods and the merchant M er delivers the goods (within a specified time), the merchant satisfies his commitment through the accessible path hs2; s3; s5; s7; : : : i. At the moment of satisfying the commitment, the merchant has still a possibility of not satisfying it through the non-accessible path hs2; s3; s5; s6; : : : i: Violation action: the semantics of violation action (see Table VII) is almost similar to the semantics of withdrawal. The main difference is related to the truth of the commitment’s content, which is false in the case of violation (condition ii). the previous one. Thus, we need to consider the temporal The fact that Á is false implies that P # sj is not accessible, component specifying the deadline of the first commitment. but the reverse is not always true as explained above. Here The logical relationship between Á and Á0 is as follows: (1) again, violation makes sense when a choice of satisfying the Á0 is true at the current state si through a given path P 0 commitment is still possible at the current state (condition iii). iff Á is true at sj where the original commitment has been created through the prefix P 0 # sj ; and (2) the two contents are logically equivalent when the temporal operators are removed. (Mi)199. jM<; hisi:;MP i;hj=sj;VPio#lastjei( Aj=g1C;rSeCatpe((iAd;gA1;gS1;CApg(2id;;ÁA))g1if;fAg2; Á)) & We consider the current state si in (1) because the new content (ii) M; hsj; P # sji j= :Á & Á0 should be true starting from the moment where the new (iii) 9 P 0 2 ¾si : P 0 # sj 2 Rscp(sj ; Ag1; Ag2) commitment is established (see Fig.4).

Example 4: When Cus pays for the goods, but M er does not deliver them within a specified time, then M er violates his commitment. Through the path hs2; s3; s5; s8; : : : i the content delivergoods is false.

Release action: the semantics of release action (see Table VIII) is similar to the semantics of withdrawal. The only difference is that the release action is performed by the creditor while withdrawal is performed by the debtor (see Fig. 3).

M20. M; hsi; P i j= Release(Ag2; SCp(id1; Ag1; Ag2; Á)) iff (i) 9j < i : M; hsj; P # sji j= Create(Ag1; SCp(id1; Ag1; Ag2; Á))& (ii) P # sj 2= Rscp(sj; Ag1; Ag2) & (iii) 9 P 0 2 ¾si : P 0 # sj 2 Rscp(sj ; Ag1; Ag2)

Example 5: The customer Cus, before paying for the goods, can release the offer. Thus, no accessible path exists between Cus and M er from s4. However, an accessible path still exists from s3.

Assignment action: the semantics of assignment action of a propositional commitment (see Table IX) is satisfied in the model M at si along path P iff (i) the creditor Ag2 releases the current commitment at si through P ; and (ii) a new commitment with the same debtor and a new creditor appears at si, so that the formula SCp(id1; Ag1; Ag3; Á0) is true at

M; hsii.

M21. M; hsi; P i j= Assign(Ag2; Ag3; SCp(id0; Ag1; Ag2; Á)) iff (i) M; hsi; P i j= Release(Ag2; SCp(id0; Ag1; Ag2; Á)) & (ii) 9 j < i : M; hsji j= SCp(id0; Ag1; Ag2; Á) &

M; hsii j= SCp(id1; Ag1; Ag3; Á0) such that: (1) 8 P 0 2 ¾si ; M; hsj; P 0 # sji j= Á , M; hsi; P 0i j= Á0 & (2) F(Á) ´ F(Á0)

The most important issue in this semantics is that the content Á0 of the new commitment is not necessarily the same as for the assigned one (Á), but there is a logical relationship between them. This is because the second commitment appears after

To clarify this issue, let us suppose that the content of the assigned commitment is Á = X+X+p where p is an atomic proposition and the assignment action takes place at the next moment after the creation action. The content of the resulting commitment should be then Á0 = X+p, which is the content we obtain by satisfying the conditions (1) and (2). By (1) we have X+p is true at a state si through a path P 0 iff X+X+p is true at the state sj (sj = si¡1) through P 0 # sj ; and by (2) we have F(X+X+p) ´ F(X+p). The second condition is added to guarantee that the relationship between the contents is not arbitrary.

Example 6: Suppose Cus commits to pay $200 to M er in two days. After one day, M er, for some reasons, assigns this commitment to M er1 (we suppose that there is an agreement between Cus and M er1 about this commitment). Thus, M er releases the commitment with Cus and a new commitment between Cus and M er1 is established to pay the $200 after only one day.

In the semantics proposed in previous frameworks (for example in [ 13 ], [ 14 ] and [ 20 ]), the two commitments have the same content, which implicitly suppose that the creation of the commitment and its assignment take place at the same moment. The previous example cannot be managed using this assumption.

Delegation action: the semantics of delegation action (see Table X) is similar to the semantics of assignment. The only difference is that delegation is performed by the debtor while assignment is performed by the creditor. Therefore, instead of release, the semantics is defined in terms of withdraw.

Example 7: Suppose Cus commits to pay $200 to M er in two days. After one day, Cus, for some reasons, delegates this commitment to a financial company (Bank) to pay the $200 to M er on his behalf. Thus, Cus withdraws his commitment and a new commitment between Bank and M er is established to pay the $200 after only one day.

M22. M; hsi; P i j= Delegate(Ag1; Ag3; SCp(id0; Ag1; Ag2; Á)) iff (i) M; hsi; P i j= W ithdraw(Ag1; SCp(id0; Ag1; Ag2; Á)) & (ii) 9 j < i : M; hsj i j= SCp(id0; Ag1; Ag2; Á) &

M; hsii j= SCp(id1; Ag3; Ag2; Á0) such that: (1) 8 P 0 2 ¾si ; M; hsj; P 0#sji j= Á , M; hsi; P 0i j= Á0 & (2) F(Á) ´ F(Á0)

The aim of this section is to prove that the model aforementioned in the previous section presents a satisfactory “logic of commitment”. We show some of desirable properties related to the semantics of actions on social commitments that are fundamental for soundness considerations where alignment [ 7 ] among interacting agents in distributed systems is satisfied. In the rest of this paper, the set of all models is denoted M.

X¡G¡:Create(Ag1; SCp(id; Ag1; Ag2; Á))¤

Proposition 1: If a commitment is created, then it has been never created before.

AG+£Create(Ag1; SCp(id; Ag1; Ag2; Á)) )

Proof: Let M be a model in M, si be a state in S, and P be a path in ¾. Also, suppose that: M; hsi; P i j= Create(Ag1; SCp(id; Ag1; Ag2; Á)) (Semantics of creation action) ) 8j < i M; hsj ; P i j= :SCp(id; Ag1; Ag2; Á) (Semantic calculus) ) M; hsi; P i j= X¡G¡:SCp(id; Ag1; Ag2; Á) (1) Let us now suppose that: M; hsi; P i j= X¡F ¡ Create(Ag1; SCp(id; Ag1; Ag2; Á)) (Semantics of creation action) ) M; hsi; P i j= X¡F ¡ SCp(id; Ag1; Ag2; Á) There is then contradiction with (1). Consequently: M; hsi; P i j= X¡G¡:Create(Ag1; SCp(id; Ag1; Ag2; Á))

As a direct consequence of this proposition, we have the following lemma: X+AG+:Create(Ag1; SCp(id; Ag1; Ag2; Á))¤

Lemma 1: Once created, a commitment cannot be created again in the future.

AG+£Create(Ag1; SCp(id; Ag1; Ag2; Á)) )

Proof: Let us suppose that the negation is true. Therefore: EF +£Create(Ag1; SCp(id; Ag1; Ag2; Á)) ^ :(X+AG+:Create(Ag1; SCp(id; Ag1; Ag2; Á)))¤ (Semantic calculus) ) EF +£Create(Ag1; SCp(id; Ag1; Ag2; Á)) ^

X+EF +Create(Ag1; SCp(id; Ag1; Ag2; Á))¤

Consequently, there is a contradiction with Proposition 1 as the second creation cannot take place since there is a creation in its past. Thus, we are done.

Proposition 2: Once withdrawn, a commitment cannot be withdrawn again in the future.

AG+£W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) X+AG+:W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á))¤

Proof: Let M be a model in M, si be a state in S, and P be a path in ¾. Also, suppose that: M; hsi; P i j= W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) (Semantics of withdrawal and creation actions) ) 9j < i : M; hsj ; P # sj i j= SCp(id; Ag1; Ag2; Á) &

P # sj 2= Rscp(sj ; Ag1; Ag2) (2) Let us now suppose that: M; hsi; P i j= X+EF + W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) (Semantics of withdrawal action, X+ and EF +) )9k > i & 9P 0 2 ¾sk:P 0#sj 2 Rscp(sj ; Ag1; Ag2) There is then contradiction with (2) because P 0 is a suffix of P . Consequently: M; hsi; P i j= :X+EF +W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) M; hsi; P i j= X+AG+:W ithdraw(Ag1; SCp(id; Ag1;Ag2;Á))

In the same way, we can prove the following three propositions (3,4 and 5) using the semantics of withdraw, fulfillment, violation and release actions, X+ and EF +.

Proposition 3: Once withdrawn, a commitment cannot be fulfilled in the future.

AG+£W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) X+AG+:F ulf ill(Ag1; SCp(id; Ag1; Ag2; Á))¤

Proposition 4: Once withdrawn, a commitment cannot be violated in the future.

AG+£W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) X+AG+:V iolate(Ag1; SCp(id; Ag1; Ag2; Á))¤

Proposition 5: Once withdrawn, a commitment cannot be released in the future.

AG+£W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) X+AG+:Release(Ag2; SCp(id; Ag1; Ag2; Á))¤

Proposition 6: Once withdrawn, a commitment cannot be assigned in the future.

AG+£W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) 8Ag 2 AGT

X+AG+:Assign(Ag1; Ag; SCp(id; Ag1; Ag2; Á))¤

Proof: Let M be a model in M, si be a state in S, and P be a path in ¾. Also, suppose that: M; hsi; P i j= W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) (Proposition 5) ) M;hsi; P i j= X+AG+:Release(Ag2; SCp(id; Ag1; Ag2; Á)) (Semantics of assignment action) ) 8Ag 2 AGT communicating agents. Also, in [ 20 ] Singh has delineated M;hsi; P i j= X+AG+:Assign(Ag2; Ag; SCp(id; Ag1; Ag2; Á)) the model-theoretic semantics of commitments by postulating some rules as ways of using and reasoning with commitments.

Using Proposition 2 and the semantics of delegation action, This model combines two commitments (practical and diawe can prove the following proposition: logical), in the sense that when a commitment arises within

Proposition 7: Once withdrawn, a commitment cannot be an argument and the content is satisfied with the same argudelegated in the future. ment, then practical commitment would be satisfied. However, AG+£W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) ) 8Ag 2 AGT this model does not include the semantics of commitment operations. Chopra and Singh [ 7 ] have used the theoretical X+AG+:Delegate(Ag1; Ag; SCp(id; Ag1; Ag2; Á))¤ model proposed in [ 20 ] to study the semantics of commitment operations with message patterns that implement commitment

As for previous propositions for withdrawal action, we can operations with some constraints on agents’ behaviors to also prove the following proposition for fulfillment action: tackle the problem of autonomy in distributed systems. This semantics is expressed in terms of the set of propositions that

Proposition 8: Once fulfilled, a commitment cannot be can be inferred from the observation sequence that agents sent fulfilled again, withdrawn, violated, released, assigned or or received. Moreover, this semantics must correspond to the delegated in the future. postulates introduced in [ 20 ]. However, the formal language AG+£F ulf ill(Ag1; SCp(id; Ag1; Ag2; Á)) ) 8Ag 2 AGT of those postulates is based on enhancing LT L (linear-time X+AG+:£F ulf ill(Ag1; SCp(id; Ag1; Ag2; Á)) logic) with two commitment modalities. Thus, this language _ W ithdraw(Ag1; SCp(id; Ag1; Ag2; Á)) is less expressive than the formal language introduced here, _ V iolate(Ag1; SCp(id; Ag1; Ag2; Á)) which is more compatible with agent choices. Furthermore, _ Release(Ag2; SCp(id; Ag1; Ag2; Á)) our semantics is based on Kripke structure with accessibility _ Assign(Ag2; Ag; SCp(id; Ag1; Ag2; Á)) relations, which enables us to prove that the proposed model _ Delegate(Ag1; Ag; SCp(id; Ag1; Ag2; Á))¤¤ is computationally grounded [ 23 ] and to verify this semantics. Finally, in [ 5 ], the propositional commitment is fulfilled when the creditor does not believe that the commitment’s

V. DISCUSSION AND RELATED WORK content is false and he cannot challenge it anymore. However, A. Discussion this semantics uses mental states which cannot be verified.

Our logical model is useful when developing agent com- The semantics defined here for conditional commitments is munication languages (ACL) thanks to its foundation based different from the semantics defined in [ 17 ] and [ 20 ]. In on social semantics. Unlike mentalistic semantics that specifies [ 17 ], conditional commitments are considered as intentions, the semantics of communicative acts in terms of pre- and post- while commitments as social notion are different from private conditions contingent on so-called agent’s mental states (e.g. intentions. In [ 20 ], Singh models conditional commitments as beliefs, desires and intentions), this social semantics can be fundamental and unconditional commitments as special cases verified [ 4 ], [ 21 ], [ 22 ]. This is because our semantics allows where the antecedent is true. In our semantics, the conditional for tracing the status of existing commitments at any point commitments are transformed into propositional commitments in time given observed actions. In commitment protocols, in all accessible paths where the underlying condition is true. social commitments capture a high meaning of interactions and provide a useful level of abstraction. In this sense, Yolum B. Related Work and Singh [ 24 ] have used commitment operations to show Let us now focus on comparing the proposed semantics for how to build and execute commitment protocols and how to commitment operations with the related ones. The semantics reason about them using event calculus. In the same way, proposed here is close to the semantics introduced in [ 3 ], Mallya and Singh [ 14 ] have showed how to reason about but does not suffer from the “recursion” problem, which is subsumption among commitment protocols and how to refine the main problem in [ 3 ]. Recursion means the semantics of and aggregate protocols based on commitment semantics and one operation depends on the semantics of one or more other operations. Also, Desai and Singh [ 9 ] have studied a com- operations. For example, in [ 3 ], a propositional commitment position of commitment protocols and concurrent operations. is satisfied along a path P at a state si iff it is active Our proposal belongs to the same line of research and can be in this state along this path, and it was already created used to specify commitment protocols in terms of creation and at a state sj , and along this path from the state sj the manipulation commitments using accessibility relation and the commitment content is true. Also, a commitment is active iff principle properties of commitment. this commitment was already created and until the current

In fact, our framework provides a unified semantics of moment the commitment was not withdrawn. Consequently, social commitments and associated operations that can be the model checking technique for this logic is very complex used to enhance, e.g., Tropos methodology [ 16 ], where Tropos and probably suffers from the state explosion problem in the is an agent-oriented software methodology, via capturing the early phases. On the contrary, the semantics we presented meaning of interactions in terms of task dependencies among here is independent, for each operation, of the semantics of other operations. Furthermore, our semantics of commitment operations is different from the ones given in [ 6 ], [ 8 ], [ 13 ] and [ 14 ]. Particularly (as discussed in Section III-B3), assignment and delegation operations should consider that the content of the new resulting commitment could be different from, and has a logical relationship with the content of the assigned and delegated commitment. This issue is not captured in previous frameworks. In addition, unlike our semantics, the violation operation has been disregarded.

C. Directions: Theoretical and Practical

Here, we outline two promising directions of future work.

Theoretically. We plan to improve our proposed semantics by removing the simplification based on the supposition that actions are only momentary and considering time frames between the execution of actions. We also plan to study the commitment operations needed to handle meta-commitments, that is commitments about commitments, that often arise in reallife scenarios. The proposed semantics would be augmented with argumentation to enhance the Tropos methodology, which we plan to apply for modeling and establishing communities of web services introduced in [ 12 ].

Practically. We intend to integrate our logical model with the logic of agent programs developed in [ 1 ] for the implementation of agents. Furthermore, a rigorous semantics opens up the way for improving the verification of logic-based protocols that govern a set of autonomous interacting agents against given properties. The mainstream step in this regard would be to map the commitment semantics introduced here to conventional verification technologies. Our semantics is based on Kripke structures (like interpreted systems). Currently model checking techniques work best for logics whose semantics is given via accessibility relations with the extension of CT L¤ as proposed in [ 4 ]. Two complementary software tools are suggested to implement model checking algorithms to verify whether or not the model M satisfies the proposed commitments’ properties (i.e., M j= Á). Model checking algorithm for our logic can be implemented via N uSM V tool, which is the best-known for CT L¤. On the other hand, the proposed logic and associated properties, which need to be checked, can be specified as tableau-based rules. Such rules provide a simple decision procedure for the logic and overcome model checking algorithm from state explosion problem. As proposed in [ 4 ], the verification method could be based on the translation of formulae into a variant of alternating tree automata called B u¨chi tableau automata (ABTA).

ACKNOWLEDGEMENTS

We would like to thank NSERC (Canada), NATEQ and FQRSC (Que´bec) for their financial support.

References

[1] N. Alechina , M. Dastani , B.S. Logan and J.-J. Ch . Meyer. A Logic of Agent Programs . In Proc. of the Twenty-Second AAAI Conf. on Artificial Intelligence (AAAI) , pp. 795 - 800 , 2007 .

[2] J. Bentahar , B. Moulin , J.-J. Ch . Meyer and B. Chaib-draa. A Logical Model for Commitment and Argument Network for Agent Communication . In Proc. of the Int. Joint Conf. on AAMAS , pp. 792 - 799 , 2004 .

[3] J. Bentahar , B. Moulin , J.-J. Ch . Meyer and Y. Lespe ´rance. A New Logical Semantics for Agent Communication . K. Inoue , K. Satoh , F. Toni (eds.), Computational Logic in Multi-Agent Systems. LNAI 4371 , pp. 151 - 170 , 2007 .

[4] J. Bentahar , J.-J. Ch . Meyer and W. Wan . Model Checking Communicative Agent-based Systems . In Knowledge-Based Systems, Special Issue on Intelligent Software Design , vol. 22 ( 3 ), Elsevier, pp. 142 - 159 , 2008 .

[5] G. Boella , R. Damiano , J. Hulstijn and L. Torre . Distinguishing Propositional and Action Commitment in Agent Communication . In Proc. of the Workshop on Comput. Modles of Natural Argument (CMNA'07).

[6] A.K. Chopra and M.P. Singh . Constitutive Interoperability . In Proc. of the Int. Joint Conf. on AAMAS , pp. 797 - 804 , 2008 .

[7] A.K. Chopra and M.P. Singh . Multiagent Commitment Alignment . In Proc. of the 8th Int. Joint Conf. on Autonomous Agents and MultiAgent Sys . (AAMAS). May 2009 .

[8] A.K. Chopra and M.P. Singh . Nonmonotonic Commitment Machines . In Dignum F. (eds) Advances in Agent Communication . LNAI 2922 , pp. 183 - 200 , 2004 .

[9] N. Desai , A.K. Chopra and M.P. Singh . Representing and Reasoning About Commitments in Business Processes . In Proc. of the 22nd Conf. AAAI , pp. 1328 - 1333 , 2007 .

[10] E.A. Emerson and J.Y. Halpern . Sometimes and not never, Revisited: on Branching versus Linear time Temporal Logic . Journal ACM (JACM) vol. 33 ( 1 ), pp. 151178 , 1986 .

[11] N. Fornara and M. Colombetti . Operational Specification of a Commitment-based Agent Communication Language . In Proc. of the Int. Joint Conf. on AAMAS , pp. 535 - 542 , 2002 .

[12] Z. Maamar , S. Subramanian , J. Bentahar , P. Thiran P and D. Benslimane . An Approach to Engineer Communities of Web Services Concepts, Architecture, Operation and Deployment . In the Int. Journal of E-Business Research , vol. 5 ( 4 ), IGI Global.

[13] A.U. Mallya , P. Yolum and M.P. Singh . Resolving Commitments among Autonomous Agents. F. Dignum (eds.), Advances in Agent Communication. LNAI 2922 , pp. 166 - 182 , 2004 .

[14] A.U. Mallya and M.P. Singh . An Algebra for Commitment Protocols . Autonomous Agents and Multi-Agent Systems , vol. 14 ( 2 ), pp. 143 - 163 , 2007 .

[15] M. El-Menshawy , J. Bentahar and R. Dssouli . A New Semantics of Social Commitments using Branching Space-Time Logic . In Proc. of the IEEE/WIC/ACM Inter. Conf. on Inte. Agent Technology (IAT'09) , Logics for Inte. Agents and Multi-Agent Systems , Milano, Italy, September 15- 18 , 2009 .

[16] P. Bresciani , A. Perini , P. Giorgini , F. Giunchiglia and J. Mylopoulos . Tropos: An Agent-Oriented Software Development Methodology . Autonomous Agents and Multi-Agent Systems , vol. 8 ( 3 ), pp. 203 - 236 , 2004 .

[17] M.K. Shakil and L. Yves . On the Semantics of Conditional Commitment . In Proc. of the Int. joint Conf. on AAMAS , pp. 1337 - 1344 , 2006 .

[18] M.P. Singh . An Ontology for Commitments in Multiagent Systems: toward a Unification of Normative Concepts . AI and Law , vol. 7 , pp. 97113 , 1999 .

[19] M.P. Singh . A Social Semantics for Agent Communication Languages . Issues in Agent Communication, Dignum , F. and Greaves , M. (eds.), LNAI 1916 , pp. 31 - 45 , 2000 .

[20] M.P. Singh . Semantical Considerations on Dialectical and Pratical Commitments . In Proc. of the 23rd Conf. AAAI , pp. 176 - 181 , 2008 .

[21] M.P. Singh. Agent Communication Languages: Rethinking the Principles . IEEE Computer , vol. 31 ( 12 ), pp. 40 - 47 , 1998 .

[22] P. Torroni , F. Chesani , P. Yolum , M. Gavanelli , M.P. Singh , E. Lamma , M. Alberti and P. Mello . Modelling Interactions via Commitments and Expectations . In Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models, ch.11 , V. Dignum (eds.), pp. 263 - 284 , 2009 .

[23] M. Wooldridge . Computationally Grounded Theories of Agency . In E. Durfee, editor, In Proc. of the 4th Int. Conf. on Multi-Agent Sys. (ICMAS 2000 ). IEEE Press, 2000 .

[24] P. Yolum and M.P. Singh . Flexible Protocol Specification and Execution: Applying Event Calculus Planning using Commitments . In Proc. of the Int. Joint Conf. on AAMAS , pp. 527 - 534 , 2002 .

[25] M. Verdicchio and M. Colombetti . A Logical Model of Social Commitment for Agent Communication . In Proc. of the Int. Joint Conf. on AAMAS , pp. 528 - 535 , 2003 .