1.1 Mental approaches

A promising method in fact to model agent communication was widely inspired by John Searle’s speech act theory (Searle, Reference Searle1969). This theory is also named communicative act theory (Wooldridge, Reference Wooldridge2009) due to the philosopher of language, John Austin, where linguistic communication is a special type of actions, which interacting agents can perform in an attempt to appropriately influence other agents (Weiss, Reference Weiss1999; Wooldridge, Reference Wooldridge2009). In this theory, as agents are autonomous, there is no choice for an agent, except in principle to affect another agent or similarly be influenced by another agent by carrying out an action. The following is a famous example in agent communication literature.

The communicative act theory particularly pertained to identify actions—denoted by performative verbs and also mapped into agents messages—performed by agents to satisfy a rational balance between their mental states (also named cognitive notions) such as beliefs, goals, desires, and intentions. This is particularly named mental approach. For instance, a mental approach specifies how the agent’s beliefs update as a consequence of the occurrence of a definite action. Mental approaches were exploited and being utilized to define the semantics of agent communication languages (ACL) messages employed in the most popular and standard ACLs, such as Knowledge Query and Manipulation Language (KQML) (Labrou & Finin, Reference Labrou and Finin1998) and ACLs of the foundation for intelligent physical agents (FIPA-ACL)Footnote ¹. Technically, the formal semantics of FIPA-ACL messages were given with respect to a well-defined formal language called Semantic Language (SL). FIPA-SLFootnote ² is a quantified multi-modal logic with several referential operators (e.g. any, all) and actions (e.g. feasible, done). The idea of SL semantics is to map each FIPA-ACL message into a formula of SL, which in turn defines a constraint that the sender of the message must achieve before uttering the message’s performative. Such a constraint is so-called the feasibility precondition. The SL semantics also map the postcondition of the message into the rational effect of the action: What an agent will be attempting to satisfy by performing the message’s performative.

While cognitive notions are desirable abstractions for designing individual agents, an ACL should also support the interoperability of two or more participating agents (Singh, Reference Singh1998, Reference Singh2000). As known, the interoperability is the capability of heterogeneous agents to work with each other to build effective and feasible systems. To satisfy the interoperability aspect, an agent should be in principle able to compute and infer an abstraction of the mental (or internal) state of another agent. Such a principle is not provided in the mental semantics (Singh, Reference Singh1998; Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013). Furthermore, it became apparent that a purely mental semantics for ACL messages in terms of pre- and post-conditions could inevitably impose substantial restrictions on the functional behaviors of agents.

When the shipment basically fails to deliver on Monday, then there is no way for the customer to verify whether or not the merchant sincerely believes that the shipment should be delivered on Monday, delineated by the inform’s precondition (Singh, Reference Singh1998, Reference Singh2000). Initially, the merchant could be particularly deceiving. On the other hand, the customer would never know whether or not the merchant would conform to ship goods without an external observer that can access the merchant’s database (it is like reading the merchant’s mind). Such an observer can be developed and implemented in specific situations, but the notion in principle is far from the standard in real business domains, because participating agents will not be willing to reveal their internal functionalities (Singh, Reference Singh1998; Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013). This problem is known as the semantics verification problem (Wooldridge, Reference Wooldridge2000, Reference Wooldridge2009). Accordingly, such pure mental semantics would be of severely restricted value in systems of heterogeneous agents (Singh, Reference Singh2000).

When conversing, agents do not particularly exchange separated messages, but a succession of messages. The developers of FIPA-ACL, for instance, have addressed the challenge of integrating ACLs and protocols by proposing a set of conversation policies, named FIPA-ACL protocolsFootnote ³. These protocols involve messages of the standard types in FIPA and can be viewed as specific ACLs designed for particular purposes, such as Request Interaction protocol, English Auction Interaction protocol (EAI), and Contract Net protocol (CN). For examples, the CN protocol is designed from online business’s perspective to reach agreements among interacting agents, whereas the EAI protocol is designed to help auction goods acquire a higher market value. FIPA-ACL protocols have succeeded and exploited in practice to specify the rules governing interactions and coordinating dialogues among participating agents by: (1) curbing the range of permitted follow-up messages at any phase during a dialogue; and (2) describing the possible ordering and occurrence constraints on messages that FIPA compliant agents can exchange for particular applications. Such protocols, however, are too rigid to be utilized by autonomous agents. This is because they are specified so that agents should enact them without being able to handle exceptions that emerge at run time. This restricts obviously the protocols’ flexibility (El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2011b; Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013).

We do not intend to in fact supply a comprehensive review of all current approaches introduced to address the limitations of mental approaches and FIPA-ACL protocols as this would be beyond the scope of this article. Therefore, we refer interested readers, for example, to: (1) the survey introduced by Maudet and Chaib-Draa (Reference Maudet and Chaib-Draa2002), which in turn focuses on how dialogue games can be exploited to improve the flexibility of FIPA-ACL protocols; (2) the book Issues in Agent Communication edited by Dignum and Greaves (Reference Dignum and Greaves2000), which documents two workshops on communication in MAS held in 1999: one on ‘Specifying and Implementing Conversation Policies’ and the other on ‘ACLs’; and (3) the recent manifesto presented by agent communication researchers (Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013), which in turn aims at identifying consensus and substantial differences among current approaches and interesting directions of future work in the field of agent communication. In the following, we only focus on social commitments and commitment-based protocols.

1.2 Social approaches

To overcome the shortcomings and inconveniences incorporated with mental approaches, the MAS community witnessed a shift from individual agent representations to social interaction approaches (Singh, Reference Singh1998, Reference Singh2000) by particularly abstracting away from agents’ mental states and by providing a social meaning to agent message exchanges. From Example 1, the judge might sign and then affix his seal on a marriage certificate (Wooldridge, Reference Wooldridge2000) or might simply talk in public, because what specifically induces the truth communication is the agreed convention within a given business domain. Informally, we would think of the judge’s proclamation as saying ‘I declare this couple husband and wife’. Parallel with this thinking, Austin argued that all communications could be articulated in the declarative form by making use of appropriate performative verbs (Wooldridge, Reference Wooldridge2000, Reference Wooldridge2009). Thus, from Example 3, an informative verb such as ‘the shipment will deliver on Monday’ can be treated as ‘merchant informs customer that the shipment will deliver on Monday’. Furthermore, a directive verb such as ‘send the goods to customer’ can be treated as ‘customer requests that merchant sends the required goods to him’. In fact, such a shift is recently asserted by agent communication community in a study by Chopra et al. (Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013). Commitments are employed in some of these social approaches, which successfully supply a well-founded principle for representing, modeling, and reasoning upon the communication of agents. In Longman Dictionary, commitment is:

• ∙ ‘a promise to do something or to behave in a particular way’; or

• ∙ ‘something that you have promised you will do or that you have to do’.

In such a definition, commitment imposes loyalty, dedication, or devotion toward a person within a social community. In broad terms, commitments are social, objective, and help in representing the states of affairs at different instants in the course of multi-agent interactions. Informally, social commitment expresses an engagement made by an agent, named the debtor—as a result of messages exchanged, actions taken, or other types of events related to agent communication—and is directed toward another agent, named the creditor, to bring about certain fact (Singh, Reference Singh1999) or to achieve some consequence of interest. For what concerns, the notion of social commitments briefly provides the following benefits for agent communication.

• ∙ The main idea of social semantics is to solely define public aspects of ACL messages for further reference from high-level abstractions without entirely reasoning about agent’s mental states. That is, all social states of the MAS that contain social facts such as commitments are global, accessible, and shared by the pairs of agents that are concerned with these social facts so that (1) the satisfiability (soundness) (Fornara & Colombetti, Reference Fornara and Colombetti2003) of agents’ behaviors can be easily monitored and verified (Chesani et al., Reference Chesani, Mello, Montali and Torroni2013; Spoletini & Verdicchio, Reference Spoletini and Verdicchio2007, Reference Spoletini and Verdicchio2009; Torroni et al., Reference Torroni, Chesani, Mello and Montali2010); and (2) the interoperability among interacting agents operating in heterogeneous systems can be straightforwardly achieved (Chopra & Singh, Reference Chopra and Singh2008; Baldoni et al., Reference Baldoni, Baroglio and Marengo2010).

• ∙ Commitment-based approaches accommodate the autonomy and flexibility of the interacting agents. The autonomy aspect is satisfied in a natural way as each agent is in principle expected to only achieve its commitments. On the other hand, as an agent at run time can select what is best for satisfying its goals (e.g. a customer substitutes a new method to make a payment, selects to deliver first, or returns damaged goods), then the approach supports flexibility as long as the behavior is correct at the business interaction level (Yolum & Singh, Reference Yolum and Singh2004; Desai et al., Reference Desai, Mallya, Chopra and Singh2005; Winikoff et al., Reference Winikoff, Liu and Harland2005; Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013).

• ∙ Commitment-based approaches provide a robust way to characterize the degrees of autonomy and interdependency of interacting agents without considering low-level details (Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013). On the one hand, when the interacting agents are completely autonomous, we then will not have an effective system of agents. On the other hand, when there is no interdependence, the interacting agents will be approximately useless; instead autonomous agents must be able to cooperate and compete with each other.

• ∙ An important aspect of social commitments is that commitments can be modified and manipulated using a set of named commitment actions, such as Create, Discharge, and Cancel (Singh, Reference Singh1999; Venkatraman & Singh, Reference Venkatraman and Singh1999). More precisely, such actions capture the dynamic behavior of committing agents, provide a principle way to evolve the changes in the social commitment states, and define the life cycle of commitments.

• ∙ As social commitments have been introduced in agent communication research, they have become a well-acknowledged engineering tool to formally model and reason upon the interaction among agents (Yolum & Singh, Reference Yolum and Singh2002b, Reference Yolum and Singh2004). Furthermore, they have been successfully applied to other research areas such as modeling business processes (Desai et al., Reference Desai, Mallya, Chopra and Singh2005; Telang & Singh, Reference Telang and Singh2009a, Reference Telang and Singh2012), developing artificial institutions (Fornara et al., Reference Fornara, Viganò, Verdicchio and Colombetti2008), defining programming languages (Winikoff, Reference Winikoff2007; Singh & Chopra, Reference Singh and Chopra2010), modeling service-oriented computing (Singh et al., Reference Singh, Chopra and Desai2009), enhancing agent-oriented software engineering methodologies (El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2009a; Telang & Singh, Reference Telang and Singh2009b), developing Web-based MASs (Venkatraman & Singh, Reference Venkatraman and Singh1999), developing agent-based Web services and their communities (Bentahar et al., Reference Bentahar, Maamar, Wan, Benslimane, Thiran and Subramanian2008; El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2009a), specifying commitment-based protocols (Yolum & Singh, Reference Yolum and Singh2002b, Reference Yolum and Singh2004; Desai et al., Reference Desai, Cheng, Chopra and Singh2007; Mallya & Singh, Reference Mallya and Singh2007; Baldoni et al., Reference Baldoni, Baroglio and Marengo2010), specifying business protocols (Desai et al., Reference Desai, Mallya, Chopra and Singh2005; El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2010a), checking commitment conflicts (Günay &Yolum, Reference Günay and Yolum2013), and diagnosing exceptions (Kafali & Torroni, Reference Kafali and Torroni2012).

Current proposals considered defining the formal semantics of ACL messages in terms of social commitments by means of either temporal logicsFootnote ⁴ (Singh, Reference Singh2000; Bentahar et al., Reference Bentahar, Moulin and Chaib-draa2003, Reference Bentahar, Moulin, Meyer and Chaib-draa2004b, Reference Bentahar, Moulin, Meyer and Lespérance2007; Mallya & Huhns, Reference Mallya and Huhns2003; Mallya et al., 2004; El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2010b), which in turn we term ‘logics of commitments’, or logics of actions (Yolum & Singh, Reference Yolum and Singh2002b, Reference Yolum and Singh2004; Chopra & Singh, Reference Chopra and Singh2006; Desai & Singh, Reference Desai and Singh2007; Chesani et al., Reference Chesani, Mello, Montali and Torroni2009). Through this article, we call these two types of logics, computational logics of commitments. The main advantages of using computational logics can be summarized as follows:

• ∙ They have a well-understood formal semantics, which in turn lays down the foundation for a neat, concise, and unambiguous logical meaning of agent messages.

• ∙ They provide a high-level language in which notions can be expressed in a transparent and concise way through a small range of powerful constructs.

• ∙ They allow us to model not only static aspects of an agent state, but also the dynamic behavior of agents. More significantly, they can be exploited by agents for making decisions and selecting courses of action, and they provide explanations for conclusions in a human friendly way (i.e. the sequence of inference steps would be restored).

• ∙ They facilitate and improve the applicability of the proposed semantics to be exploited, for example to develop automated reasoners.

1.3 Specifying and verifying commitment-based protocols

Commitment-based protocols, specified as a set of commitments and associated actions explicitly capturing the meanings of exchanged messages and a set of agent roles, are more suitable for regulating and coordinating agent interactions than FIPA-ACL’s protocols and conventional software engineering protocols purely modeled in terms of finite state machines (FSM), statecharts, and Petri nets, which only capture legal orderings of exchanged messages without unduly considering the meanings of those messages (El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2011b; Chopra et al., Reference Chopra, Artikis, Bentahar, Colombetti, Dignum, Fornara, Jones, Singh and Yolum2013). In a point of fact, the typical function of commitments in commitment-based protocols involves introducing the syntax for the exchanged messages along with a formalization of the precise meanings (expressed in terms of commitments) of those messages. Having such a declarative principle not only simplifies the modeling of protocols, but also provides a beneficial basis for flexible and rigorous specifications (i.e. a participating agent might communicate in any way it opts as long as its created commitments are discharged), which in turn can be searched for correctness (Yolum & Singh, Reference Yolum and Singh2004; Yolum, Reference Yolum2007; Bentahar et al., Reference Bentahar, Meyer and Wan2010; El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2010b, Reference El-Menshawy, Bentahar and Dssouli2011b). Internally, in commitment-based protocols, agents will not reason about legal sequences but about concrete commitment states and possible pathsFootnote ⁵ to reach them (Yolum & Singh, Reference Yolum and Singh2002a; El-Menshawy et al., Reference El-Menshawy, Bentahar, Qu and Dssouli2011c).

The motivation of the MAS community, however, is no longer just formally representing and reasoning about social commitments and commitment actions, but becomes the application of various verification techniques, such as full-automatic model checking, semi-automatic verification, local testing, static verification, monitoring, etc. in order to (1) verify the compliance of commitment-based protocols with given specifications at design time; (2) identify the compliant and non-compliant agents at the end of the commitment-based protocol at run time; or (3) track the evolution of commitment statuses at run time, respectively. This verification process is significant because there is a possibility that an agent might fail to comply with its commitments as it is supposed to. For what concerns, it is unrealistic—in open systems (e.g. e-business, e-negotiation) or in any application wherein interacting agents are implemented in different programming languages and having competing objectives—to assume that all autonomous agents will behave (or act) according to the given protocols because they might not behave as they are committed to or at least not wantonly violate or cancel commitments. Furthermore, a formal verification technique, such as model checking, is necessary to help protocol designers either detect automatically unwanted and bad agents’ behaviors to eliminate them or enforce desirable agents’ behaviors so that such protocols comply with given specifications. Thus, ensuring that merely the suitable interactions take place is a significant aspect of analyzing and designing effective MASs (El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2010b, Reference El-Menshawy, Bentahar, Qu and Dssouli2011c).

1.4 Motivation and organization of the article

The motivation and plan of the article are to go through prominent and predominate proposals in the literature to explore the state of the art on how temporal logics can be devoted to define a formal semantics for ACL messages in terms of social commitments and related actions. In our methodology to achieve this objective, we first begin by exploring the historical development of commitments from philosophy, distributed systems, and artificial intelligence (AI) perspectives up to the time it gets landed on MASs, including as a special case agent communication (Section 2). Second, in Section 3, we present a running example to demonstrate our presentation and discussion of reviewed proposals. Third, in Sections 4–6, we explore and evaluate current proposals that advocate temporal logics: respectively, linear temporal logic (LTL) (Pnueli, Reference Pnueli1977), computation tree logic (CTL) (Clarke & Emerson, Reference Clarke and Emerson1982), and full computation tree logic (CTL*) (Emerson & Halpern, Reference Emerson and Halpern1986) not only to represent and reason about commitments and associated actions, but also to specify commitment-based protocols. We specifically explain each proposal and point out if and how it meets seven crucial criteria (presented in Section 2). We also aim at exploring and evaluating different techniques proposed to verify the correctness of commitment-based protocol specifications introduced in those proposals. The point is not to declare one proposal as a winner, but to highlight the advantages (strengths) and limitations (where they exist) of those proposals to designers and developers, so that they can make the best choice with regard to their needs. The limitations (or disadvantages) should not be considered fatal, but only a consideration that must be taken. Fourth, in Section 7, we proceed to succinctly present logical languages of actions, such as event calculus (EC), C⁺, and modular action description for protocols, which have been exploited to specify, model, and execute commitment-based protocols. In Section 8, we finally conclude by summarizing current limitations and suggesting the directions for future work from our perspective. It is worth noticing that our methodology would help designers and developers with their choices throughout:

1. 1. Indicating that CTL*-based approaches are more expressive than those using LTL and CTL, which are in turn incomparable, expressiveness-wise (Emerson, Reference Emerson1990). This will help designers, who are non-expert in logic, make their choices if expressiveness is an issue.

2. 2. Presenting the syntax and semantics of commitments and their fulfillments to be able to express them in the desirable properties.

3. 3. Discussing the way of defining the formal models introduced in the reviewed proposals and the way of expressing desirable protocol properties using LTL, CTL, and CTL*.

4. 4. Categorizing current proposals into run-time proposals and design time proposals with respect to the employed verification methods.

5. 5. Comparing different verification techniques in terms of their efficiency: The number of interacting agents, number of reachable states, and execution time.

6. 6. Presenting our conclusions about each section in the form of remarks.

We finally present a running example, which we use in our presentation and discussion of reviewed proposals through the whole manuscript.

4.1 Giordano and colleagues

Giordano et al. (Reference Giordano, Martelli and Schwind2003, Reference Giordano, Martelli and Schwind2007) developed a logical framework based on Dynamic Linear Time Temporal Logic (DLTL), an extension of LTL with propositional dynamic logic, to specifically specify and verify commitment-based protocols. In this framework, the protocol describes the meaning of communicative actions in terms of their effects on the system’s social state, including commitments and some facts related to the protocol’s execution. These effects are expressed by means of ‘action laws’. The protocol specifies a set of ‘precondition laws’, which, in principle, define the execution of actions, a set of ‘causal laws’ capturing the dependencies among social states, and a set of temporal constraints, which provide restrictions on the possible correct behaviors of the protocol.

In this approach, commitments are modeled as fluents, basic components of EC (Shanahan, Reference Shanahan2000). In principle, every fluent is either true (hence commitment holds) or false (hence commitment does not hold), and no fluent is both true and false. A fluent might also exchange its truth value with the performance of communicative actions. For instance, the fluent C(NB, Mer, Cus, deliverGoods) means that Mer is committed to Cus to execute the action deliverGoods in NB (cf. Figure 2). However, the approach does not explicitly introduce commitment actions. Instead, the authors introduced a causal law to define the operational semantics of discharge action.

It is worth mentioning that Singh (Reference Singh2008) removed the temporal operators □ and ○ in the postulate that defines the operational semantics of discharging commitments in order to make it reasonable and intuitive. In the verification part, the authors discussed different types of verification problems depending on whether the verification process is carried out at design time such as verifying protocol properties or at run time such as verifying agents compliance with a protocol. However, they informally reduced DLTL formulae into standard LTL formulae, and commitment-based protocol into PROMELA (the input language of the SPIN model checker (Holzmann, Reference Holzmann1997)) wherein commitments are represented as PROMELA processes and protocol actions are represented as PROMELA message channels, which are communicating interleaved processes. By informally, we mean that the reduction (transformation) rules are not delineated by a systematic and formal way; so the soundness of the mapping from DLTL formulae into LTL formulae can be proved. The semantics of this approach is formal, declarative, meaningful, and verifiable using model checking. Model checking is a full, formal, and automatic verification technique during the design time. By modeling commitments as fluents, we will have the issue discussed in the following remark.

In fact, the problem in Remark 1 is not about the expressiveness of fluent representation, but it is in the fluent modeling itself. Specifically, by modeling commitment C (i, j, φ) as a fluent, the truth value of this fluent after substituting i and j and then evaluating the truth value of φ is either true (i.e. commitment holds) or false (i.e. commitment does not hold) (the solution of this problem is introduced after Remark 3). Furthermore, the use of the SPIN model checker has a limitation discussed in Remark 2.

4.2 Pham and colleagues

Pham and Harland (Reference Pham and Harland2007) introduced an approach that extends LTL with linear operators that model resources, actions, and capabilities of interacting agents, the resulting logical language is named TLL. This language is in turn exploited to flexibly generate commitment-based protocols from the internal view of participating agents in terms of a set of agents’ capabilities, resources, and pre-commitments. Those pre-commitments can be negotiated among each other using inference rules and upon being accepted, will form conditional commitments. The authors exploited negative formulae, which can be regarded as formulae in demand and linear implication expressing the causal relationship in the form of reasoning rules to represent and reason about unconditional and conditional commitments, respectively. When the antecedents are satisfied, the linear implication will assure that unconditional commitments turn effective. An unconditional commitment is fulfilled whenever the agent successfully performs the actions required by its commitment. This specifically means that the corresponding positive formula—which can be regarded as formula in supply—in TLL is derived.

However, the way of generating the token Cond is not considered. Constructing protocols from the view of participating agents by making use of proof search and putting the specification of commitments locally at the respective agents according to their roles has an interesting advantage toward avoiding the mapping ‘from protocol actions to commitment operations’. However, some issues are missing in this approach. The first one is syntactic: the realm of commitment has only the debtor, which is not an effective representation as the two main features of commitment representation are social and directive. The second one is in modeling commitments as propositions, which in turn waive formal semantics (cf. Remark 1). The third one is of adopting the linear implication to obtain an unconditional commitment from the conditional one when its antecedent is true. The linear implication ‘ $${\raster="rg7"}$$ ’ represents capabilities of agents in producing and consuming resources. Let p and q be agents’ resources, so p $$p\,{\raster="rg7" }\,q$$ q ensures that the antecedent before p will be transformed into the antecedent after q in which p is removed after producing q. We can think of the linear implication as the one Canadian dollar p is ‘gone after using it to buy a chocolate bar’ q. From our perspective, a linear implication might function as the material implication (p⊃q), which is true when p is false, so we could have an unconditional commitment without satisfying its antecedent. To evaluate the semantics of this approach, it meets the formal (in terms of introducing logic-based approach to define the meaning of protocol actions via commitments) and meaningful criteria, but it does not consider the verifiability issue. However, as protocols are specified in terms of what is to be achieved rather than how the agents should act, the proposed semantics meets the declarative criterion.

4.3 Singh and colleagues

Desai et al. (Reference Desai, Cheng, Chopra and Singh2007) proposed an interesting way to model business protocols in terms of social commitments and their actions, which in turn reduce the emphasis on the rigid sequence of actions that participating agents must take and facilitate loose coupling among these agents. They also exploited a particular language named OWL-P introduced in Desai et al. (Reference Desai, Mallya, Chopra and Singh2005) to model business protocols. OWL-P supports the specification and composition constructs to build standard business protocols and incorporates the standard web ontology language (OWL) for modeling well-defined business processes. The authors argued that the correct composition of business processes can be expressed via individual protocols and their composition constraints and thereby enabling the verification of a wide range of composed processes. To verify properties geared toward the composition of protocols, the authors informally reduced protocols into the PROMELA language, which in principle allows them to model the composition of protocols in terms of a set of processes and analyzing the resulting model with the SPIN model checker. In this technique, as in Giordano et al. (Reference Giordano, Martelli and Schwind2007), commitments and their actions are modeled in terms of OWL-P rules, which are mapped, respectively, into PROMELA processes without capturing all features of commitments such as evaluating the consequence of commitment at the proper time, and into PROMELA messages. The checked properties are classified into general properties such as deadlock and livelock freedom and protocol-specific properties that check a specific behavior of participating agents. An example of protocol-specific property is as follows.

It is clear that this semantics is formal, declarative, meaningful, and verifiable. Although the authors focused on modeling commitments as simple processes in the PROMELA language to address the lack of communication aspect raised in fluent modeling, no formal semantics is given to commitments. Recall that a formal LTL-based framework is in fact proposed to solely express protocol properties. To this end, three missing points in this approach are as follows: (1) a formal model for protocols; (2) a formal translation procedure; and (3) a formal semantics for commitment actions themselves.

Singh (Reference Singh2008) introduced the model-theoretic semantics for social commitments by postulating some rules (axioms) that can be utilized as methods to reason about commitments and solely detach and discharge actions. A commitment becomes detached when its antecedent is true. A commitment that is detached but fails to be discharged indicates a violation. This model particularly extends LTL with modalities for two kinds of commitments: practical commitments, which are about what is to be made, whereas dialectical commitments, which are about what holds. In this model, the semantics is interpreted using Segerberg’s idea, which in turn maps ‘each world into a set of set of worlds’. For instance, to define the semantics of dialectical commitments, Singh introduced a function:

$${\Bbb D}:{\Bbb T}{\times}{\cal A}{\times}{\cal A}{\times}{\scr P}({\Bbb T})\to{\scr P}({\scr P}({\Bbb T}))$$

that produces a set of propositions for each moment, an ordered pair of two agents and proposition where $${\Bbb T}$$ is a set of moments, $${\cal A}$$ is a set of agents, and $${\scr P}({\Bbb T})$$ is the powerset of $${\Bbb T}$$ . Each proposition is a set of moments. This function yields a set where each member is a consequent proposition, which in turn captures what the debtor would be committed to if the antecedent is met. Thus, the commitment semantics is delineated by computing the set of moments where the consequence holds $$\raster="rg2"$$ and testing if those moments are among the moments $\raster="rg3"$ computed by $$ {\Bbb D}$$ on the commitment antecedent $\tau $ :

$$M,s\, \models CC\,(i,\,k,\,\tau ,\,\varphi )\;iff\,\raster="rg2" \in {\Bbb D}\left( {s,\,\raster="rg3"} \right)$$

Notably, the author focused on identifying the logical terms between the antecedent and consequence of commitment to avoid the problem of both the linear implication exploited in Pham and Harland (Reference Pham and Harland2007) and the ‘strict implication’ advocated in Singh (Reference Singh2000) to define the semantics of conditional commitments (cf. Section 5 for the problem of strict implication).

• ∙ CC (Mer, Cus, sendPayment, sendReceipt)∧Payment⊃C (Mer, Cus, sendReceipt);

• ∙ Receipt⊃¬CC (Mer, Cus, sendPayment, sendReceipt).

It is obvious that this semantics is formal, declarative, and meaningful. However, the computation of the function $${\Bbb D}$$ is not specified, which feasibly makes the possibility of implementing and applying such an approach unclear as discussed in Bentahar et al.(Reference Bentahar, El-Menshawy, Qu and Dssoulia2012). As the semantics is not based on Kripke structures, verifying such a semantics using model checking needs either defining an equivalent semantics using Kripke structures or interpreted systems, or defining a completely new model checking approach for the extended logic from scratch. The semantics of discharge action focuses upon checking whether the truth condition of the commitment consequence is true or not, but we believe this should be a part of the semantics of the commitment modality not the discharge one. Throughout the article, we refer to this problem as over-specification. Simply put, such a problem occurs when some specifications are repeated in the semantics of different operators. In our case, this problem happens because the truth condition of the commitment consequence is part of not only the commitment operator, but also its discharge.

4.4 Baldoni and colleagues

Baldoni et al. (Reference Baldoni, Baroglio and Marengo2010, Reference Baldoni, Baroglio and Marengo2011, Reference Baldoni, Baroglio, Marengo and Patti2013) observed that current specifications of commitment-based protocols do not account for the regulative specifications and focus only on the constitutive specifications. The constitutive specification defines the semantics of all agents’ actions in terms of how these actions affect the social state, whereas the regulative specification constraints the evolution of the social state. They forcefully argued that the two specifications together define the meaning of the interaction (because the only constraint by which we can say that an interaction governed by protocol is successful is that all commitments are discharged), but it is well suited to distinguish between them. The authors then introduced a framework to model commitment-based protocols that separates the constitutive and regulative specifications. They also showed that the regulative specifications should be based on commitments holding in social states not on the execution of actions in order to address the limitations raised in previous proposals (Giordano et al., Reference Giordano, Martelli and Schwind2003, Reference Giordano, Martelli and Schwind2007) regarding the openness, interoperability, and modularity of designing MASs, which in fact complicate the re-use of software agents’ actions. Furthermore, the authors defined a first-class and declarative language, named, 2CL, to represent the constraints among commitments (i.e. only the regulative specifications). 2CL provides seven kinds of constraint rules, such as correlation, co-existence, cause, response, and before. Such constraint rules are delineated by making use of equivalent LTL temporal modalities.

Notice that the commitment of the merchant is modeled as an LTL atomic proposition.

The proposed semantics is declarative and meaningful. When the protocol specification is exploited to define the meaning of ACL messages, the semantics of this approach satisfies the formal criterion. However, the approach waives the formal semantics for commitments as commitments are simply modeled by propositions, which in principle suffer from the same problem discussed in Remark 1. Although the constraint rules can be expressed directly by LTL modalities, which in turn opens the way to utilize different model checkers to check, for example, whether or not agent behaviors comply with the protocol, the authors do not consider the verification issues. To this end, separating the regulative rules from commitments has been criticized recently by Marengo et al. (Reference Marengo, Baldoni, Baroglio, Chopra, Patti and Singh2011). In particular, Marengo et al. placed regulative rules in the antecedents and consequences of commitments to identify the ‘duties and rights’ of the debtor and creditor.

4.5 Verdicchio and colleagues

Spoletini and Verdicchio (Reference Spoletini and Verdicchio2007) developed an ‘automata-based monitoring module’ to keep the interactions of a single agent safe by checking whether the evolution of its commitment states with regard to certain events is compatible with some desirable properties defined in agent’s specifications and expressed in LTL^± (an extension of LTL with past and future modalities). A commitment is modeled as a predicate with four components: an event e that has created the commitment, a debtor i, a creditor j, and a consequence φ: Comm (e, i, j, φ). The consequence φ of a commitment is represented by a first-order term and written ⌊φ⌋ in order to refer to the relevant LTL^± formula in which ⌊φ⌋ is named a ‘truth-preserving translation’ of φ. The commitment is fulfilled (resp. violated) when its consequence is true (resp. false):

$$\eqalignno{ & Fulf\,(e,\,i,\,j,\,\varphi )\,{\triangleq}\,Comm\,(e,\,i,\,j,\,\varphi )\wedge{\lfloor}\varphi {\rfloor} \cr & Viol\,(e,\,i,\,j,\,\varphi )\,{\triangleq}\,Comm\,(e,\,i,\,j,\,\varphi )\wedge\neg {\lfloor}\varphi {\rfloor} $$

In the verification part, the monitoring module comprises of two components (Spoletini & Verdicchio, Reference Spoletini and Verdicchio2009): (1) ‘Word Composer’ responsible for collecting all data resulting from agent communication, preserving track of the relevant information, and in turn elaborating them to assess and evaluate present and past time-stamped words selected from these data; and (2) ‘Word Analyzer’ that translates such words into Alternating Modulo Counting Automata (Spoletini, Reference Spoletini2005) functioning as a ‘language acceptor’. Unaccepted word in this approach means that the state of the system does not satisfy the property expressed by the monitored formula, and such violation is notified to the agent. This semantics meets formal (using LTL^±-based framework to define the semantics for agent communication), declarative (wherein every communicative action can be viewed as the modification of commitments attaching agents to others), meaningful, and verifiable criteria. However, this approach lacks formal semantics for commitments because commitments are modeled as predicates, which are reduced into propositions as stated by the authors as ‘to be able to write the properties to be monitored in the form of LTL^± formulae, we need to translate the first-order logic sentences into propositions’. Furthermore, the semantics of fulfillment and violation actions suffer from the over-specification problem. It is worth noticing that whereas modeling commitments as predicates by making use of a pure predicate logic (or first-order logic) (Huth & Ryan, Reference Huth and Ryan2004) allows one to model real-life business scenarios, not only they cannot distinguish among various ‘modes’ of truth, such as inevitably true, □, and true in the future, ◊, but also suffer from the problem reported in the following remark.

Indeed, the problem in Remark 3 is not about the flexibility of protocol (e.g. to say that the protocol should consist of several ways of the payment), but it is about the possibility of considering equivalent commitments as different commitments. To solve the problems in Remarks 1 and 3, the ‘sense’ of the formula having opaque context is needed along with its truth value. A similar solution was introduced by Wooldridge (Reference Wooldridge2009), who models agent’s belief as a temporal modality. In principle, the sense of commitment C (i, j, φ) is to qualify the truth value of φ, that is C (i, j, φ) is satisfied at a state s iff φ is not only true in a certain state but true in all accessible states s′ from s defined by certain accessibility relation. This accessibility relation is defined by considering the local states of interacting agents as well as other conditions to generate a computationally grounded semantics, which is entirely missing in fluent (or predicate) modeling and this is why EC-based approaches do not have formal models. The main advantage of computationally grounded semantics is to directly interpret formulae into concrete models and vice versa.

In the literature of agent communication semantics, there are few proposals that have been introduced to address the limitation of the pure predicate logic and the lack of communication aspect emerged from fluent and proposition modelings. For instance, Colombetti (Reference Colombetti2000) proposed an extended first-order modal language (EFOM) to represent and reason about commitments. In particular, the author introduced a new set of basic speech-act-based ACL, which is named Albatross (agent language based on a treatment of social semantics). This ACL is based on the social notion of commitments. The semantics of the main elements of Albatross is based on the EFOM language. Concretely, the semantics of commitment modality is delineated by using a certain type of accessibility relation: $$f_{c} :D_{{{\rm action}}} {\times}D_{{{\rm agent}}} {\times}D_{{{\rm agent}}} {\times}S\to2^{{2^{S} }} $$ , which in turn produces a family set of states for each state, and a typed domain of individual sorts of action and a pair of two agents. The semantics is defined by computing the set ||φ|| of states satisfying the commitment consequence and testing if this set is among the set of states computed by f _c. This would be formally defined as follows:

$$M,s\, \models C\,(e,\,i,\,j,\,\varphi ) \,iff\, \,\mid\mid\,\varphi \,\mid\mid\,\in f_{c} (\delta \,(e,\,s),\,\delta (i,\,s),\,\delta (j,\,s),\,s)$$

where C (e, i, j, φ) is named a modal predicate and means that the performance of action e commits i relative to j to bring about φ, δ (e, s) and δ (x, s), where x∈{i, j} define, respectively, the denotation of action e and agent x at s. The author showed that the commitment is violated when its consequence is false. A violation of the commitment C (e, i, j, φ) is delineated by the following semantic rule:

$$V(e,\,i,\,j)\,{\triangleq}\,C\,(e,\,i,\,j,\,\varphi )\wedge\neg \varphi $$

As claimed by the author, the logic of commitment is ‘indeed very weak’ and there is no ‘counterpart of the D axiom’. Consequently, an agent can make conflicting commitments. The author also contended that inferential capacities are ‘sufficient to derive that at least one of two conflicting commitments is going to be violated’. He in turn showed that reasoning upon violations provides a way to deal with conditional commitments in question. This semantics is formal, declarative, and meaningful, but verifiability has not been addressed. As in Singh (Reference Singh2008), the approach does not describe how in practice the accessibility relation f _c can be computed. The approach also does not define (1) axioms of commitment logic; and (2) the semantics of other commitment actions to automatically reason about the developed language.

We conclude this section with Table 1, which in principle summarizes the results of evaluating the contributed proposals that advocate LTL (or an extension of LTL) to define the semantics for ACL messages. In the table, we use For., Dec., Mea., and Ver., to, respectively, refer to formal, declarative, meaningful, and verifiable Singh’s criteria. We also indicate how the commitments are modeled (Mod.) and if a formal semantics (Sem.) is defined for them. Although all reported proposals satisfy the first three criteria (formal, declarative, and meaningful), there is no formal semantics for social commitments, except Singh’s (Reference Singh2008) proposal. The declarative specification of commitment-based protocols will permit agents to realize in advance whether or not the protocol supplies them enough assures of attaining their objectives to take part.

Table 1

Summary of linear temporal logic and commitment-based agent communication

We claim that our new criteria would help designers and developers decide which proposal will satisfy their choices or will meet their needs. To support this claim, we consider Desai et al.’s (Reference Desai, Cheng, Chopra and Singh2007) approach and Spoletini and Verdicchio’s (Reference Spoletini and Verdicchio2007, Reference Spoletini and Verdicchio2009) proposals as illustrative examples. Although Desai et al.’s approach and Spoletini and Verdicchio’s proposals satisfy all agent communication semantics criteria, their evaluations with respect to commitment-oriented criteria and verification method criterion are entirely different. If designers need to verify the correctness of the developed semantics before proceeding to implement it in order to detect design errors, they will select Desai et al.’s proposal, which adopts a model checking technique, applied at design time, and they know the semantics of commitments will be transformed into PROMELA processes to be able to use SPIN. On the other hand, if designers plan to monitor the behaviors of interacting agents at run time, they will use monitoring tool developed by Spoletini et al. that represent commitments as predicates. Moreover, as there are no experimental results reported in all reviewed proposals in Table 1, we could not discuss the performance of the used verification methods. When we classify a particular semantics of a proposal as being not verifiable, we mean that the verifiability issue is not considered, but still there might be a possibility to use a technique to verify that proposal.

5.1 Singh and colleagues

Venkatraman and Singh (Reference Venkatraman and Singh1999) introduced an approach for locally testing whether the behavior of an agent in Web-based MASs complies with a commitment-based protocol specified in CTL with the idea of ‘potential causality’. Their verification process centers on the conditions under which an individual agent (named an observer, who participates in the protocol) can check the satisfaction or violation of commitments made by each agent toward each other by making use of a model checking-like technique. This technique is similar to model checking, but it uses a different procedure and performs at run time. Technically, a model checking-like approach can ‘only falsify (but not verify) the correctness of the construction of the agents’ in the MAS. That is, when the observer agent discovers an inappropriate execution, this entails that the system does not satisfy the protocol. Each commitment in this approach is a meta-commitment. The consequence of commitment is expressed as a CTL formula and commitment itself is modeled as a variable c of type T, which is an abstract data type (ADT). Operations that can be performed on commitments are modeled as methods having c as an argument.

This ADT can be implemented as a module where the module’s interface declares the methods corresponding to the type’s operations. In this modeling, there is no formal semantics for commitments. However, when it comes to agent communication, the semantics of this approach is formal (as the protocol is specified in CTL, the formal semantics of ACL messages is well defined), declarative, meaningful (as the meaning of every message is expressed in terms of commitments), and verifiable. Their verification technique is an effective one provided that the system under consideration has a small state space. The semantics of commitment actions, on the other hand, is not considered in this work.

Based on Jürgen Habermas’s theory of communicative acts (Habermas, Reference Habermas1984), Singh (Reference Singh2000) proposed three-level meanings for ACLs such that each communicative act is associated with three validity claims: (1) objective claim meaning that the debtor is committed to send something that is true; (2) subjective claim stating that the debtor is committed to sincerity, that is the debtor believes or intends what is communicated; and (3) practical claim regarding to the debtor’s claim that it is justified in making the communication. Recall that defining the meaning of communicative acts is not different from the meaning of the messages specified in the protocols as argued in the approach proposed in Venkatraman and Singh (Reference Venkatraman and Singh1999). To avoid the shortcoming of Venkatraman and Singh (Reference Venkatraman and Singh1999) regarding the representation of commitments as simple variables, the author extended CTL modalities with three modalities for commitments, beliefs, and intentions to model interactions among agents. He particularly presented three accessibility relations to define the semantics of those modalities. For instance, the semantics of the commitment modality is satisfied at s in a model M iff the consequence is true along every accessible path π delineated by using an accessible relation $${\Bbb C}\,(i,\,j,\,G,\,s)$$ and emanating from the commitment state s, this would be expressed as:

$$M,s\, \models C\,(i,\,j,\,G,\,p)\, iff\, (\forall \pi :\pi \in {\Bbb C}\,(i,\,j,\,G,\,s)\,\supset\,M,\pi (s)\, \models p)$$

where the accessibility relation $${\Bbb C}:{\cal A}{\times}{\cal A}{\times}{\cal A}{\times}S\to2^{\Pi } $$ , where $${\cal A}$$ is a set of agents and Π is a set of paths, produces the set of accessible paths along which the commitments made by the debtor i toward the creditor j in the social context G hold at a state s∈S. The author exploited the defined modalities to give the formal semantics of the ACL messages.

The strict implication is indeed introduced to define the semantics of conditional commitment. Its semantics is given as follows:

$$M,s\, \models p{\,\raster="rg6"\,}q\,iff\,M,s\, \models p\,and\,(\forall s':M,s'\, \models p\,\supset\,(\forall s'':s'\,\approx\,s''\,\supset\,M,s''\, \models q))$$

The formula p $$p{\,\raster="rg6"\,}q$$ q is satisfied at s in a model M iff p holds in the current state s and for all states s′ in M, if p holds, then we have that q holds in all states s′′ similar to s′, that is s′≈s′′. Given a commitment-based semantics for ACL primitives, the author exploited it to derive a specification language of commitment-based protocols. The new specification helps analyze the protocol by determining, for example, the compliance of an agent with respect to a given protocol.

Although Singh’s approach satisfies formal, declarative and meaningful criteria, it does not clarify the intuition that the accessibility relation $${\Bbb C}$$ captures and how accessible paths are computed. More precisely, there is a lack of intuition, due to the meaning behind the fact that a state or a path is accessible from the state where the commitment holds is not delineated. Particularly, an accessibility relation should specify the intuitive relation between a social commitment and accessible paths or states. Furthermore, an accessibility relation should clarify how in a computational model one can determine if a state or a path is accessible. The author then suggested different levels of verifiability in order to verify the correctness of the proposed semantics. Two verifiability levels are as follows: (1) ‘every commitment to a putative fact can be verified or falsified by challenging that putative fact’; and (2) ‘every commitment to a mental state can be similarly verified or falsified, but only through the more arduous route of eliciting the agent’s beliefs and intentions’. As created and manipulated (or modified) commitments can be publicly recorded, the observer agent—as in Venkatraman and Singh (Reference Venkatraman and Singh1999)—can be in turn exploited to test the compliance of other agents with a given protocol. However, when the semantics is given in terms of mental states, Wooldridge (Reference Wooldridge2000) pointed out that it is very difficult to carry out the verification of this property as we do not understand how such states can be systematically attributed to agents’ programs. Such a problem stems from the subjective semantics, which, in principle, refers to a mental component by arguing that interaction among agents should be sincere.

The first application of Singh’s descriptive ontology of commitments (Singh, Reference Singh1999) to design coordinated MAS was introduced by Xing and Singh (Reference Xing and Singh2001). They particularly proposed a set of commitment patterns inspired by design patterns to composedly model agent interactions. In this approach, each pattern captures an important scenario and can be specialized and applied to commitment actions. Different combinations of patterns can yield different kinds of agent interactions. In this approach, each pattern is expressed as a CTL formula. The commitments are simply modeled as ADTs where the consequence is a predicate with a vector of domain arguments $\vec {v}$ to pass data values.

Commitment actions are modeled as predicates (cf. Remark 3 to know why predicates are not suitable to represent commitments). The following formula expresses the relationship between the communication proposition Inform and action predicate Create:

$$\forall i,\,j,\,Pred\,,\vec {v}: A{□}\,[Inform(i,\,j,\,Pred(\vec {v}))\,\supset\,A\diamondsuit [Create\,(i,\,C\,(i,\,j,\,G,\,Pred(\vec {v})))]]$$

This formula means that along all paths in all states when agent i informs agent j about a predicate Pred ( $\vec {v}$ ), then along all paths there is a possibility that i creates a commitment to bring about Pred ( $\vec {v}$ ) toward j in the context G. The authors exploited a statechart to specify the behavior model of each agent. Indeed, the operational semantics provided by statecharts are exploited as a rigorous basis for coordinating the interactions of agents. To relate such operational semantics with temporal logic specifications, a CTL model is produced from agent’s statechart. The soundness of this transformation is proved. The authors continued their approach in Xing and Singh (Reference Xing and Singh2003) by developing (1) an algorithm to transform the statechart of behavior model of agent into CTL model; (2) a library of commitment patterns; and (3) a library of behavior models of agents along with theorem proving which behavior models comply with which patterns. Notably, the agent communication semantics of this approach is formal, declarative, meaningful, and verifiable (using theorem proving). In theorem proving, the proof construction is in general difficult and requires a good deal of human ingenuity (Emerson, Reference Emerson1990). However, manual proof construction does not scale up well to large programs and fails ‘to be of much help due to the inherent complexity of testing validity for even the simplest logics’ (Clarke et al., Reference Clarke, Emerson and Sistla1986). When commitments are considered as basic components in ACLs, no formal semantics is given because they are simply modeled as ADTs and treated as propositions in CTL model. Recall that a formal CTL-based framework is proposed to give only semantics for agent communication using commitments.

Mallya and Huhns (Reference Mallya and Huhns2003) and Mallya et al. (Reference Mallya, Yolum and Singh2004) developed an extension of CTL with (1) predicates to represent and reason upon commitments and related actions; and (2) two temporal quantifiers (existential and universal) to describe temporal deadlines in the form of time points and Allen’s intervals. This extension provides a richer temporal aspect for the commitment consequences in order to capture real-life scenarios.

To define the semantics of violation and fulfillment of the commitment c in question, the authors, respectively, introduced two predicates (Breached (c) and Satisfied (c)). For instance:

$$\eqalignno{ M,s\, \models Satisfied(c) \ iff &\ \Big( \exists s_{3} :s_{3} \leq s\,and\,M,s_{3} \, \models Discharge(i,c) \ and, \cr & (\exists s_{1} :s_{1} \,\lt \,s_{3} \,and\,M,s_{1} \, \models Create(i,c), and \cr & (\forall s_{2} :s_{1} \leq\, s_{2} \,\lt\, s_{3} \,\supset\,M,s_{2} \, \models Active(c))\Big) } \right)$$

The semantics of the Satisfied (c) predicate at s in a model M is defined in terms of whether or not the Discharge (i, c) of the commitment c that has been created in the past and still active holds. A commitment is active if it is not canceled, delegated, assigned, released, and discharged yet. The authors assumed that the discharge action ‘brings about p, and conversely, if p occurs, the discharge action is assumed to have happened’. As a result, the discharge action’s performance is in principle equivalent to the satisfaction of p. In fact, this assumption raises many issues. More specifically, Verdicchio and Colombetti (Reference Verdicchio and Colombetti2004), in the same proceedings, criticized such an assumption by showing that the above semantics of the Satisfied (c) predicate appears ‘bypassing the problem instead of solving it’. As the scope of the discharge action focuses on checking whether or not the truth condition of the commitment consequence holds, it in turn suffers from the over-specification problem discussed in Singh (Reference Singh2008). To conclude, such a semantics straightforwardly supports formal, declarative, and meaningful criteria for agent communication but not the verifiable criterion. The authors also model commitments and associated actions as predicates, which in turn suffer from the problem discussed in Remark 3.

To enable a rich modeling of temporal deadlines for commitments, Torroni et al., (Reference Torroni, Chesani, Mello and Montali2010) extended Mallya et al.’s (Reference Mallya, Yolum and Singh2004) proposal by using ‘variables with domains’ inside commitments. The authors showed that without such an extension, Mallya et al.’s representation of commitments does not cover some practical situations. For example, a commitment of Cus toward Mer to send the payment p is going to hold at a given moment in the interval beginning at t ₁ and ending at t ₂ would be represented in Mallya et al.’s model as: C (Cus, Mer, [t ₁, t ₂]p). This modeling enables reasoning about the temporal deadline without considering the p’s meaning and specifying the time at which the commitment is satisfied. In Torroni et al.’s model, p is defined as a variable, which is bound to a domain interval: [T]p, T∈[t ₁, t ₂]. Thus, the commitment above can be written as:

$$C\,(Cus{\rm ,}\,Mer{\rm ,}\,[T]p),\,t_{1} \leq T\leq t_{2} $$

When there exists a possible value of T in the range [t ₁, t ₂], the commitment is satisfied and this value can be used for further inferences. This commitment is violated at time t (viol (C (Cus, Mer, [T]p, t))) ‘due to the elapsing at time t of a time interval in which p was supposed to be verified’. The authors proposed a specification language called commitment modeling language (CML), which consists of a set of domain variables, constraints and rules. They used EC axioms not only for reasoning about the effects of commitment actions, but also for a static verification of properties and compliance checking, which tracks the evolution of commitment statuses at run time by making use of reactive event calculus (REC), which is implemented in SCIFF, an abductive proof procedure (Alberti et al., Reference Alberti, Chesani, Gavanelli, Lamma, Mello and Torroni2008). In this approach, commitments are modeled as fluents and then there is no formal semantics for commitments (cf. Remark 1 for more information about the limitations of fluents). The proposed semantics for agent communication perspective is formal (where EC axioms are used to model commitment actions capturing the meaning of ACL messages), declarative, meaningful, and verifiable.

Gerard and Singh (Reference Gerard and Singh2013) developed an analysis tool named ‘Proton’ to specify business protocols having social semantics and their refinement. In particular, Proton specifies a protocol declaratively in terms of (1) its agent roles; (2) guarded messages, which must be true before the messages can be sent by the roles; and (3) the meaning of each message as a set of actions applied to the roles’ social states, holding atomic propositions that specify the states of commitments. Proton also describes the syntax for a refinement mapping. To verify refinement of protocols, they exploited model checking to compute whether a protocol refines correctly another one under a given mapping that contains the essential elements for refining any two protocols. Internally, their verification technique uses the Proton preprocessor that first reads the two protocols and mapping specifications and then generates both the ISPL model accepted by the MCMAS model checker (Lomuscio et al., Reference Lomuscio, Qu and Raimondi2009) and CTL formulae expressing certain conditions. All generated CTL formulae must be satisfied in the generated model by MCMAS for the protocol refinement to hold. The proposed agent communication semantics is formal, declarative, meaningful, and verifiable. The formal semantics of commitments is entirely missing because the authors modeled commitments as objects with seven instances that are mapped into domain variables in the ISPL language. These variables cannot represent the real and concrete meaning of commitments. However, commitment actions are simply modeled as atomic propositions, not as effective actions. Technically, the operational semantics of discharge action—‘which occurs implicitly when the consequent becomes true’—suffers from the over-specification problem.

Using the approach of Xing and Singh (Reference Xing and Singh2001, Reference Xing and Singh2003), Telang and Singh (Reference Telang and Singh2009a, Reference Telang and Singh2012) introduced an interesting business model that uses social commitments and agent-oriented concepts such as goals and tasks inspired by Tropos software engineering methodology (Bresciani et al., Reference Bresciani, Perini, Giorgini, Giunchiglia and Mylopoulos2004) to capture complex, long-lived business scenarios among business partners involved in service engagements (Telang & Singh, Reference Telang and Singh2009a) or cross-organizational business processes that are the norms in today’s MAS applications (Telang & Singh, Reference Telang and Singh2012). As in Xing and Singh (Reference Xing and Singh2003), the authors developed a library of business patterns that in turn model recurring business scenarios wherein each pattern is delineated by a highly abstract-level based upon the notion of commitments with some attributes: name, intent, motivation, implementation, and consequence inspired by classical object-oriented design patterns. In order to verify agent interactions, Telang and Singh proposed two different methods to implement this process. In the former one (Telang & Singh, Reference Telang and Singh2009a), they introduced a reasoning algorithm, which in turn takes a business model populated by a set of business patterns and business interactions formalized using the UML sequence diagrams and returns a set of violated commitments. In the latter one (Telang & Singh, Reference Telang and Singh2012), they exploited the NuSMV model checker (Cimatti et al., Reference Cimatti, Clarke, Giunchiglia, Giunchiglia, Pistore, Roveri, Sebastiani and Tacchella2002) to verify whether an operational model (a set of business interactions) correctly confirms the defined business model. Technically, a business model pattern is formalized as a set of CTL formulae. The following is an example of a business pattern and its CTL formalization.

A commitment is simply modeled as an SMV module, which can be initiated as a domain variable in the main module. To evaluate this semantics for agent communication against our criteria, it is formal (where a CTL-based framework is introduced to express business model patterns), declarative, meaningful, and verifiable. However, there is no formal semantics for commitments as they are modeled simply as SMV modules. In addition, formal semantics for commitment actions themselves are not considered. With respect to the flexibility of classical commitment machines (Yolum & Singh, Reference Yolum and Singh2002a), adopting the UML sequence diagram to model the behavior of interacting agents forces the temporal ordering of action executions, which in principle looses the flexibility supported by the adoption of commitments as shown in Baldoni et al. (Reference Baldoni, Baroglio and Marengo2010, Reference Baldoni, Baroglio and Marengo2011).

5.2 Bentahar and colleagues

El-Menshawy et al. (Reference El-Menshawy, Bentahar and Dssouli2011b) presented a framework that comprises of three parts aiming at excluding spurious aspects that plague some of the above proposals (e.g. lacking intuition and computation, modeling commitments as fluents, propositions and predicates, and reducing commitments into domain variables). In the first part, they introduced a new temporal logic, named CTLC, an extension of CTL with modality for commitments. They defined a social accessibility relation R _sc to interpret the semantics of the commitment modality. This is the first approach that associates the formalism of interpreted systems introduced in Fagin et al. (Reference Fagin, Halpern, Moses and Vardi1995) to model MASs with the Kripke model in order to compute the accessibility relation and define an intuitive semantics of social commitments, which is missing in existing proposals of agent communication models. In the formalism of interpreted systems, each agent $$i\in {\cal A}$$ is characterized by a set of local states L _i, a set of local actions, a local protocol, and a local evaluation function. The set of all global states S is a subset of the Cartesian product of all local states of n agents at a given time: S⊆L ₁×L ₂× … ×L _n. The standard CTL model M=(S, R _t, V, I) is extended to M′=(S, R _t, R _sc, V, I), where $$R_{{sc}} :S{\times}{\cal A}{\times}{\cal A}\to2^{S} $$ is the social accessibility relation for commitments. It is defined as follows:

$$s'\in R_{{sc}} (s,\,i,\,j)\,iff\;\exists \bar{s}\in S:l_{i} (s)=l_{i} (\bar{s})\,and\,l_{j} (\bar{s})=l_{j} (s')$$

where l _i (s) denotes the local state of agent i in the global state s. Intuitively, s′ is accessible from s, that is s′∈R _sc (s, i, j) iff there is an intermediate state $\bar{s}$ , so that there is no difference for the debtor i between being in s and $\bar{s}$ ; but for the creditor j there is no difference between being in the intermediate state $\bar{s}$ and accessible state s′. In the second part, the semantics of commitments is formally defined as follows:

$$M',s\ \left| {=C(i,\,j,\,\varphi )\,iff\,\forall s'\in S,\,if\,s'\in R_{{sc}} \,(s,\,i,\,j),\,then\,s'} \ \right|=\varphi $$

which means that the consequence φ is true in every accessible state from the current state computed using R _sc (s, i, j). In the last part, the authors show how the problem of model checking CTLC can be formally reduced, using a transformation function $${\scr F}$$ , into the problems of model checking CTLK (an extension of CTL with knowledge modality (Penczek & Lomuscio, Reference Penczek and Lomuscio2003)) and ARCTL (an extension of CTL with action formulae (Pecheur & Raimondi, Reference Pecheur and Raimondi2007)) in order to be able to, respectively, use the MCMAS and extended NuSMV (Lomuscio et al., Reference Lomuscio, Pecheur and Raimondi2007). The more interesting point in this approach is that the commitment modality is reduced into the knowledge modality, not into domain variables, as follows:

$${\scr F}\,(C\,(i,\,j,\,\varphi ))=\mathord{\buildrel{\lower3pt\hbox{$\scriptscriptstyle\frown$}}\over K} _{i} {\scr F}(\varphi ) \wedge {\rm E}\!\bigcirc\! \mathord{\buildrel{\lower3pt\hbox{$\scriptscriptstyle\frown$}}\over K} _{j} {\scr F}(\varphi )$$

where $$\mathord{\buildrel{\lower3pt\hbox{$\scriptscriptstyle\frown$}}\over K} _{i} \varphi $$ read as ‘possible knowledge’ of agent i (Fagin et al., Reference Fagin, Halpern, Moses and Vardi1995), is the dual of agent knowledge K _iφ (i.e. $$\mathord{\buildrel{\lower3pt\hbox{$\scriptscriptstyle\frown$}}\over K} _{i} \varphi \,{\triangleq}\,\neg K_{i} \neg \varphi $$ ) and $$E\!\bigcirc\! \mathord{\buildrel{\lower3pt\hbox{$\scriptscriptstyle\frown$}}\over K} _{j} $$ is read as there is a path such that in the next state agent j possibly knows φ. The authors also implemented the reduction technique on top of the MCMAS and extended NuSMV to automatically verify a business protocol against some desirable properties, such as reachability, liveness, and safety.

It is clear that our seven criteria for agent communication semantics using commitments are successfully met. However, the authors do not consider the semantics of commitment actions and their verification.

To address the identified limitations, El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c) extended CTLC introduced in El-Menshawy et al. (Reference El-Menshawy, Bentahar and Dssouli2011b) with two modalities to represent and reason about fulfillment (Fu) and violation (Vi) of commitments. Given that, the authors proceed to develop a new symbolic algorithm to perform the model checking of the proposed logic and fully implemented such an algorithm on top of the MCMAS model checker developed for MASs (Lomuscio et al., Reference Lomuscio, Qu and Raimondi2009). An example of fulfillment is as follows.

Bentahar et al. (Reference Bentahar, El-Menshawy, Qu and Dssoulia2012) and El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b) redefined both the social accessibility relation introduced in El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c) to account for the intuition that social commitments are conveyed through communication between agents and the semantics of commitments and their fulfillments. They also removed the violation modality presented in El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c); instead the violations of commitments are expressed as properties to simplify the proposed semantics.

This refinement is extremely important as far as time complexity and space complexity are concerned. The refined logic is called CTLC⁺. As in El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c), Bentahar et al. (Reference Bentahar, El-Menshawy, Qu and Dssoulia2012) adopted the direct verification technique that develops symbolic algorithms needed for the new modalities. The verification technique introduced by El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b), on the other hand, is based on formally reducing the problem of model checking CTLC⁺ into the problem of model checking ARCTL and the problem of model checking GCTL* (Bhat et al., Reference Bhat, Cleaveland and Groce2001) (a generalized version of CTL* with action formulae) so that the extended NuSMV symbolic model checker and the CWB-NC automata-based model checkerFootnote ⁷ as a benchmark are usable. The authors tested the satisfiability of a set of desirable properties, such as safety and reachability.

El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b) also showed that their formal reduction technique is easy to implement and allows one to compare different verification methods and techniques with respect to the same logic. To come into the evaluation of Bentahar et al. (2012) and El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b), the semantics introduced in these proposals evidently meets our seven criteria. However, there is no semantics for other commitment actions and conditional commitments. Another issue is that the semantics of fulfillment implies that the commitment is active at the moment of its fulfillment, that is Fu(C(i, j, φ))⊃C(i, j, φ), which is not commonly accepted in the literature (cf. e.g. Yolum & Singh, Reference Yolum and Singh2004; Winikoff et al., Reference Winikoff, Liu and Harland2005; Singh, Reference Singh2008).

5.3 Yolum and colleagues

Kafali et al. (Reference Kafali, Günay and Yolum2014) developed a tool, called $${\cal P}{\scr R}{\cal O}{\cal T}{\cal O}{\cal S}{\cal S}$$ , to detect and predict possible privacy violations within online social networks (OSNs). The privacy agreements that exist among each user and the OSN operator and the relations among the users constitute the formal model. Such privacy agreements are represented as a set of commitments. The tool has a semantic reasoning component that makes use of an ontology, which is used to refine commitments. For instance, if the OSN operator commits to a user not to share her information, then via reasoning on the ontology, the system can infer that neither a person’s location nor her pictures can be shared. Moreover, undefined privacy concerns can be discovered through the ontology. The following example shows a commitment representing a privacy agreement.

The above example shows that the operator will be committed not to share Charlie’s location information with his colleagues if Charlie declares an individual as his colleague. After these agreements are specified, then the OSN operator is asked to check if there are any privacy violations in the system model. Following the above example, if a colleague ends up seeing Charlie’s location, this would yield a privacy violation.

Kafali et al. represent privacy violations as commitment violations in the system model and employ model checking to detect such violations. In general, the model checking technique is used to check that the private behavior rules—which define the operational behavior of the OSN operator—comply with privacy agreement shared between a user and the OSN operator, such that the operator would act in a way that honors its agreement with the user. Specifically, the authors use NuSMV as the underlying model checker and model a commitment as an SVM module in order to enable NuSMV to deal with commitments, in the same spirit of Telang and Singh (Reference Telang and Singh2012). The commitment module defines the statuses of a commitment, which correspond to the commitment states. As the focus is on the privacy violations, only four commitment states are implemented: conditional, active, fulfilled, and violated. The life cycle implemented there allows a commitment to be fulfilled only if both the antecedent and consequent hold, as if the consequent holds without the antecedent, there is still a privacy violation. Using the commitment module, domain variables of commitment types can be specified.

With the help of $${\cal P}{\scr R}{\cal O}{\cal T}{\cal O}{\cal S}{\cal S}$$ , which is implemented as the privacy checker for the OSN operator, privacy properties are expressed in CTL and then automatically checked. For example, the following property describes if Charlie and Linus are colleagues, the commitment introduced in Example 24 (say c1) is violated. The model checking then decides if this is true, thereby leading a privacy violation.

$$A{□}(colleague\_charlie\_linus\,\supset\,A\!\diamondsuit \,c1.status=VIOLATED)$$

The workings of the approach have been tested over privacy scenarios and their performance have been evaluated on a Facebook data set. Their results show that when the social network is small, the commitments can be verified in a reasonable time, but when the network grows, the model needs to be pruned to be verified efficiently. As Kafali et al.’s proposal follows the same methodology as Telang and Singh (Reference Telang and Singh2012) when it comes to the representation of commitments as SMV modules, the two proposals share the same evaluation with regard to our criteria.

Table 2 summarizes our results of evaluating current proposals that use CTL (or an extension of CTL) to define the semantics for ACL messages using commitments and related concepts.

Table 2

Summary of computation tree logic and commitment-based agent communication

We conclude this section with Table 3, which in principle presents the empirical results reported in the proposals reviewed in Table 2 in order to be able to evaluate the performance of their employed verification methods in terms of number of agents, number of reachable states, and execution time. By comparing the direct verification technique in El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c) and the reduction verification technique in El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b) when the number of agents is six agents, we found that

1. 1. The direct verification technique needs <0.01 second to execute the verification process, whereas the reduction verification technique needs 630.914 seconds (cf. Table 3). The reason why the reduction technique is slower because its execution time is the summation of the time needed to carry out the actual verification process and the time needed to carry out the reduction preprocessing step.

2. 2. The reduction verification technique is hard to scale up in order to include more agents (six agents in El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b) and 20 agents in El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c)), because this technique is based on transformation rules that require extra states (Bentahar et al., Reference Bentahar, Meyer and Wan2010) and transitions (El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2011a, Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013a) to capture the semantics of certain actions as well as additional temporal operators, which are added to find the equivalent formulae to the transformed ones.

3. 3. The number of reachable states in the reduction verification technique (238 787 states, see Table 3) is more than the corresponding one in the direct verification technique (239 states in El-Menshawy et al. (Reference El-Menshawy, Bentahar, Qu and Dssouli2011c)), because some states are added in the transformation process.

Table 3

Empirical results reported in the proposals reviewed in Table 2

6.1 Colombetti and colleagues

Verdicchio and Colombetti (Reference Verdicchio and Colombetti2003, Reference Verdicchio and Colombetti2004) introduced a logical framework for the definition of ACL semantics based on the concept of social commitments resulting from the performance of speech acts by presenting a branching-time temporal logic, named CTL^±, which in turn enriches CTL* with (1) ‘past-directed temporal operators’; and (2) meta-language predicates (or many-sorted first-order language) containing terms, which in turn denote events, actions, commitments, and commitment actions. They also introduced a number of appropriate axioms to describe the constitutive effects of the action types for commitment manipulations. In other terms, each axiom describes the state of affairs that necessarily holds once a token of a given action type is successfully carried out. There are basically two possibilities to represent the consequence of commitment: (1) it can be represented as a CTL^± formula, in which case, a commitment can be modeled as a modal operator; and (2) it can be represented as a first-order term, in which case, a commitment can be modeled as a first-order formula. The authors forcefully argued that modeling a commitment as a first-order formula rather than a modal operator has the advantage that the ‘technicalities required by a predicative representation are simpler than the ones required by a modal representation’. Such a first-order term can be viewed as the representation of a concrete Content Language (CL) statement. To achieve this goal, the syntax of CL statement can be represented as a first-order term in CTL^±. Technically, such a first-order term, say φ, is represented as a CTL^± formula using a ‘truth-persevering translation’ ⌊φ⌋. However, modeling commitments using many sorted first-order terms waives the formal semantics and the sense of formulae, which in turn makes using model checking-based verification inappropriate. Inspired by Reichenbach’s (Reference Reichenbach1947) terminology, the semantics of fulfilling commitments is defined as follows:

$$Fulf(e,\,i,\,j,\,\varphi )\,{\triangleq}\,C(e,\,i,\,j,\,\varphi ) \wedge A \diamondsuit ^{{\minus}} (Happ(e)\wedge{\lfloor}\varphi {\rfloor})$$

where ◊⁻ is read as ‘sometimes in the past’. The predicate Happ(e) states that an event e has happened and ⌊φ⌋ is a truth-preserving translation of the commitment consequence φ into a CTL^± formula. The semantics of fulfillment means that the commitment is fulfilled at s′ (Reichenbach’s point of event), when the commitment-inducing event e has been made at s (Reichenbach’s point of speech) where the truth value of Happ(e) and ⌊φ⌋ are true ‘at some state in the past of s′ on every path starting from s and going throughout s′’. Notably, this agent communication semantics meets the following criteria: formal, declarative, and meaningful. However, the semantics of fulfillment action in principle suffers from the over-specification problem as it considers the truth value of the commitment consequence, which is the main component of the semantics of commitment itself. The authors also do not consider the verification issue. From our point of view, the verification of this logic by means of model checking is very hard to perform because: (1) the proposed logical model uses superfluous translation of the commitment consequence and past operator that points to the state at which the commitment is made; and (2) the model checking of predicate logic is undecidable as we cannot write a procedure that works for all φ (the proof of this claim is introduced in Huth & Ryan (Reference Huth and Ryan2004)). Such a temporal language has been extended with two interval operators, dates, and times to express a ‘rich assortment of temporal conditions’, such as deadlines in a natural way, which is missing in the CL expressions of FIPA-ACL (Verdicchio & Colombetti, Reference Verdicchio and Colombetti2005). Here are some examples of temporal deadlines:

• ∙ The agreed payment is due before the end of November 2014: $$\langle cd(),{\it 2014}Y{\rm 11}M\rangle \,{\bullet}Done(Payment)$$ , where cd() is the constant of the current time.

• ∙ The agreed payment is due within 45 days from the time of delivery: $$\langle Done(delivery),$$ $$cd(){\plus}{\it 45}D\rangle Done(payment)$$ .

• ∙ The auction will be open for 40 hours: [Done(openAuction), cd()+40H]Open(auction).

This approach could be considered as a generalization of the work introduced in Mallya et al. (Reference Mallya, Yolum and Singh2004). Colombetti et al. (Reference Colombetti, Fornara and Verdicchio2004) and Verdicchio and Colombetti (Reference Verdicchio and Colombetti2006) showed that FIPA’s communicative act library can be effectively redefined using a commitment-based semantics instead of FIPA’s mental semantics with respect to their logical model introduced first in Verdicchio and Colombetti (Reference Verdicchio and Colombetti2003) and extended in Verdicchio and Colombetti (Reference Verdicchio and Colombetti2004). For example see the following.

6.2 Bentahar and colleagues

The first work on combing social commitments as deontic notions and arguments into the paradigm of ACL was done by Bentahar et al. (Reference Bentahar, Moulin and Chaib-draa2003). In this hybrid approach, the social and public aspects of conversational agents are captured by commitments and the reasoning aspects are delineated by means of arguments. The authors claimed that existing approaches introduced to define ACL semantics are ‘not exclusive but rather complementary’. This approach, however, waives defining formal semantics of commitments, arguments, and semantic link between them. In continuation of this work, Bentahar et al. (Reference Bentahar, Moulin and Chaib-draa2004a, Reference Bentahar, Moulin, Meyer and Chaib-draa2004b, Reference Bentahar, Moulin, Meyer and Lespérance2007) adopted a temporal logic to address such limitations. In particular, they extended CTL* with (1) modalities for commitments and two-party actions; (2) argument modality; and (3) a DL, which in turn captures the actions that agents are committed to achieve. They then introduced two accessibility relations to define the semantics of commitment and argument modalities. For instance, the accessibility relation dedicated to commitments (Bentahar et al., Reference Bentahar, Moulin, Meyer and Lespérance2007) is defined as: $$R_{{sc}} :{\cal A}{\times}{\cal A}{\times}S\to2^{\Pi } $$ , which in turn associates with a state s a set of accessible paths along which an agent commits toward another agent. Thus, the semantics of the commitment modality is given as:

$$M,s\, \models C(i,\,j,\,\varphi )\,iff\,\forall \pi :\pi \in R_{{sc}} \,(s,\,i,\,j),M,\pi \, \models \varphi $$

The commitment formula is satisfied in a model M at s iff the consequence φ is true along every accessible path started at s and computed by R _sc. The semantics of the Satisfy (discharge) action is defined in terms of whether the commitment has been created in the past and still active and its consequence holds or not. This would be expressed as:

$$\eqalignno{ M,\pi (s)\, \models Satisfy(i,\,C(i,\,j,\,p))\,iff\quad &#x0026; M,\pi (s)\, \models Active(C(i,j,p))\,and\,\exists s':T(s')\leq T(s) \cr &#x0026; and\,\,M,s'\, \models Create(i,C(i,j,p))\,and\,M,\pi (s)\, \models p $$

where T (s) gives the time point associated to the state s. A commitment is active iff this commitment was already created, and till the present moment, the commitment in question was not withdrawn:

$$M,\pi (s)\, \models Active(i,C(i,j,p))\,iff\;M,\pi (s)\, \models \neg \,Withdraw(i,C(i,j,p))\,U^{{\minus}} Create(i,C(i,j,p))$$

where U ⁻ is interpreted as ‘since in the past’. To define flexible conversations, the authors interpreted a speech act not as an action performed on a commitment as usual, but also on a commitment consequence to enable agents to defend and justify their commitment consequence and to attack and challenge the commitment consequence of other agents. This semantics for agent communication meets formal, declarative, and meaningful criteria. As we discussed in Colombetti (Reference Colombetti2000) and Singh (Reference Singh2008), the intuition of the accessibility relation and how accessible paths are practicality computed is not clear. Furthermore, this semantics is delineated by a recursive manner (i.e. the semantics of one action depends recursively on the semantics of one or more other actions), which in turn induces its model checking procedure quite hard. In addition, the semantics of satisfy action suffers from the over-specification problem as it focuses upon checking the truth condition of the commitment consequence.

El-Menshawy et al. (Reference El-Menshawy, Bentahar and Dssouli2009b, Reference El-Menshawy, Bentahar and Dssouli2010b) addressed the limitations of Bentahar et al. (Reference Bentahar, Moulin and Chaib-draa2004a, Reference Bentahar, Moulin, Meyer and Chaib-draa2004b, Reference Bentahar, Moulin, Meyer and Lespérance2007) by developing a logical model based on a new temporal logic, named CTL*^sc, which in principle extends CTL* with (1) past-directed temporal modalities; and (2) modalities for commitments and all pertained actions. The proposed logic is exploited to drive a new specification language of commitment-based protocols to particularly define the meaning of protocol messages in terms of commitments. In particular, the semantics of each action does not depend upon other actions using the notion of accessible and non-accessible paths. For instance, the semantics of fulfillment (discharge) action is satisfied in a model M along a path π _i starting at s _i iff (1) the commitment was established in the past at s _j (after performing the creation action) through the prefix of π starting from s _j denoted by π _i ↓ s _j; (2) all paths starting at state s _i+1 (the state resulting from the fulfillment action) using R _sc at state s _j (where the commitment has been established) are accessible paths; and (3) at the present state s _i, there exists a possible choice of not fulfilling the commitment as the prefix $$\pi ''_{i} \!\downarrow \!s_{j} $$ of a non-accessible path $$\pi ''_{i} $$ emanating from s _i is present. This would be expressed as:

$$\eqalignno{ (M,s_{i} ,\pi _{i} )\, \models Fulfill(i,C(i,j,\varphi ))\,iff \ (1) &#x0026; \exists j\leq i:(M,s_{j} ,\pi _{i} \downarrow s_{j} )\, \models C(i,j,\varphi )\,and \cr (2) &#x0026; (s_{i} ,Fulfill,s_{{i{\plus}1}} )\in R_{t} \,and \cr &#x0026; \forall \pi '_{{i{\plus}1}} \in \Pi ^{{s_{{i{\plus}1}} }} :\pi '_{{i{\plus}1}} \downarrow s_{j} \in R_{{sc}} (s_{j} ,i,j)\,and \cr (3) &#x0026; \exists \pi ''_{i} \in \Pi ^{{s_{i} }} :\pi ''_{i} \downarrow s_{j} \,\notin\, R_{{sc}} (s_{j} ,i,j) $$

where Π^si is the set of paths starting at s _i. Thus, the semantics of fulfillment action is cured from the over-specification problem raised in Verdicchio and Colombetti (Reference Verdicchio and Colombetti2003), Bentahar et al. (Reference Bentahar, Moulin and Chaib-draa2004a, Reference Bentahar, Moulin, Meyer and Chaib-draa2004b), Mallya et al. (Reference Mallya, Yolum and Singh2004), Verdicchio and Colombetti (Reference Verdicchio and Colombetti2004), Bentahar et al. (Reference Bentahar, Moulin, Meyer and Lespérance2007). The idea is that ‘being accessible means that the consequence φ is true along all the paths $$\pi '_{{i{\plus}1}} \downarrow s_{j} $$ and fulfillment occurs automatically when the commitment consequence holds’. They also introduced a new definition of assignment and delegation actions by considering the relationship between the original and new commitment consequences, which is missing in the current approaches. The authors expressed in CTL*^sc a set of desirable properties named ‘functional correctness’, such as liveness, reachability, safety, and fairness constraint. An example of the reachability property is given as follows.

The authors also proposed a symbolic verification technique based on informally reducing the problem of model checking CTL*^sc into the problems of model checking LTL^sc and CTL^sc inspired by the notion introduced in Clarke et al. (Reference Clarke, Grumberg and Peled1999) regarding the reduction of model checking CTL* into the problems of model checking LTL and CTL. Notice that LTL^sc and LTL^sc are the standard LTL and CTL extended with commitments and their actions. In this technique, the participating agents in the protocol are defined either as modules using SMV (the input language of NuSMV) or as sets of local states and actions along with local protocol, and local evaluation function using the ISPL language. However, modeling commitments and their actions as domain variables in the SMV and ISPL languages waives real and concrete meanings of commitments and their actions. El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013a) recently addressed this limitation by developing a reduction technique that formally transforms the problem of model checking CTL*^sc into the problem of model checking GCTL*, so as to use the CWB-NC model checker. An example of the liveness property checked in this proposal is given as follows: the liveness property means that ‘something good will eventually happen’. For example:

$$\hskip -100pt \eqalignno{ A{&#x25A1;}(EFu(&#x0026; Mer,\,C(Mer,\,Cus,\,deliverGoods))\,\supset\, \hfill \cr &#x0026; A\diamondsuit [ { EFu(Cus,\,C(Cus,\,Mer,\,sendPayment)) \hfill }\cr &#x0026; \vee EWi (Cus,\,C(Cus,\,Mer,\,sendPayment)) \hfill \cr &#x0026; \vee EVi(Cus,\,C(Cus,\,Mer,\,sendPayment)) \hfill ])\hfill \cr} )$$

However, as we discussed in El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b) and proved in Bentahar et al. (Reference Bentahar, El-Menshawy, Qu and Dssoulia2012), formal reduction techniques show very limited scalability and high memory usage. The conditional commitment semantics introduced in El-Menshawy et al. (Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013a) has a limitation resulting from using the material implication operator to define the causal relationship between conditional and unconditional commitments: $$CC(Mer,\,Cus,\,sendPyament,\,sendReceipt)\, {\triangleq}\,sendPayment\,\supset\,C(Mer,\,Cus,\,sendReceipt)$$ . This limitation means that the conditional commitment CC (Mer, Cus, sendPyament, sendReceipt) could become active without satisfying its antecedent sendPayment. This limitation also appeared in Pham and Harland (Reference Pham and Harland2007). To conclude these approaches, their semantics are formal, declarative, meaningful, and verifiable and at the same time there is a formal semantics for commitments and all associated actions (El-Menshawy et al., Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013a).

Bentahar et al. (Reference Bentahar, Meyer and Wan2009, Reference Bentahar, Meyer and Wan2010) presented a verification technique based on informally reducing ACTL* (an extension of CTL* with modalities for commitments, arguments, and commitment actions) and protocols into Alternating Büchi Tableau Automata so that they made use of the CWB-NC model checker in order to address the verifiability criterion, which is the main limitation of their approaches (Bentahar et al., Reference Bentahar, Moulin and Chaib-draa2004a, Reference Bentahar, Moulin, Meyer and Chaib-draa2004b, Reference Bentahar, Moulin, Meyer and Lespérance2007). However, this approach is still suffering from lacking formal semantics for commitments and their actions as commitments are defined as simple variables and agent actions as atomic propositions using CCS (the input language of the CWB-NC). In addition, they only considered two-party actions. Table 4 summarizes our results of investigating the proposals that adopt CTL* (or an extension of CTL*) to (1) represent and reason about commitments; (2) define the semantics for ACL messages using commitments; and (3) specify commitment-based protocols and express their properties.

Table 4

Summary of full computation tree logic and commitment-based agent communication

We conclude this section with Table 5, which introduces the empirical results reported in some of the reviewed proposals in Table 4, so as to evaluate the performance of their employed verification methods in terms of number of agents, number of reachable states, and execution time. From Table 5, the authors El-Menshawy et al. (2013) considered more interacting agents (nine agents). In fact, we could not compare between these proposals (Bentahar et al., Reference Bentahar, Meyer and Wan2010; El-Menshawy et al., Reference El-Menshawy, Bentahar and Dssouli2010b, Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013a) because they employ different (1) logical models; (2) semantics for commitments and their fulfillments; (3) temporal modalities that were used to extend CTL*; and (4) temporal properties that are being model checked. In the table, it is clear that the results of symbolic techniques (MCMAS and NuSMV) in terms of execution time are better than the corresponding ones of the automaton-based technique (CWB-NC).

Table 5

Empirical results reported in the proposals reviewed in Table 4

7.1 Action logical language: event calculus

Yolum and Singh (Reference Yolum and Singh2002b, Reference Yolum and Singh2004) specified commitment-based protocols using commitment machines with the use of a subset of Shanahan’s EC (Shanahan, Reference Shanahan1997). Roughly speaking, EC is a logical language for representing and reasoning upon actions and their effects. The basic components of EC are fluents (properties or atomic propositions holding within time intervals) and events (actions happening at certain time points) (Shanahan, Reference Shanahan1997). Fluents are initiated and terminated by occurring events (i.e. events manipulate and modify fluents). In this approach, EC is akin to ‘many-sorted first-order predicate calculus’ with eight predicates and a set of axioms to represent and in turn reason upon actions wherein commitments are modeled as predicates (cf. Remark 3 about the problem resulting from using predicates). For example, the discharge action, whose purpose is to successfully fulfill a commitment, is axiomatically defined as:

$$terminates(E(I),C(I,J,P),T) \leftarrow happens (E(I),T) \wedge discharge \,(E(I),C(I,J,P))$$

This axiom means that when an event E(I) has been carried out by I at time T and the commitment is successfully discharged, the active commitment is stopped (or terminated). Such a discharge axiom can be delineated by another way (cf. Winikoff et al. (Reference Winikoff, Liu and Harland2005) framework, fig. 7) as:

$$\eqalignno{ &#x0026; terminates{\rm (}E{\rm (}I{\rm ),}\,C{\rm (}I,J,P{\rm ),}\,T{\rm )}\leftarrow \cr holds\_at(C(I,J,P),\,T)\wedge \,&#x0026;\, happens(E(I),T) \wedge initiates(E,P',T) \wedge subsumes(P',P) $$

The new axiom focuses on checking the status of commitment in question at time T and the existence of a new fluent P′ initiated by occurring of an event E(I) at the same time and in turn subsumed the commitment consequence P, and if so, the commitment is terminated. Notice that the predicate subsumes checks implicitly whether or not P holds (for other axioms that define other commitment actions, see Winikoff et al. (Reference Winikoff, Liu and Harland2005)). Yolum and Singh’s approach (Yolum & Singh, Reference Yolum and Singh2002b, Reference Yolum and Singh2004) for defining the semantics of agent communication meets formal, declarative, and meaningful criteria. Moreover, the authors exploited an abductive EC planner (Shanahan, Reference Shanahan2000) to logically compute reasoning queries with respect to the EC axioms (in the form of reasoning rules) that specify protocols: Given the initial protocol state, final protocol state, and protocol specification, the reasoner (planner) in turn computes ‘all possible protocol runs’ (where a run is a linear arrangement of actions) that can be generated between the initial state and final (goal) one. Agents can utilize the abductive EC planner to logically calculate protocol runs leading to a desirable outcome. By keeping track of agent’s commitments, we can check whether the agent behaviors comply with its commitments. This technique can be named static verification that could be preferably carried out at run time. The technique seems promising, but computing all possible runs regarding the commitment in question is hard to apply when we check open systems having a large state space, as discussed in Artikis et al. (Reference Artikis, Sergot and Pitt2009). Yolum and Singh also pointed out that their specifications achieve flexibility by means of enabling agents to adjust their actions by taking advantages of opportunities and accommodating exceptions that arise at run time by reconstructing plans as necessary. However, the flexibility resulting from reasoning capabilities can be expensive and might increase the code of the agents (Yolum & Singh, Reference Yolum and Singh2002a; Singh, Reference Singh2007). Thus, the authors suggested that the specification of protocols can be compiled into FSMs (Yolum & Singh, Reference Yolum and Singh2002a) or Büchi automata (Singh, Reference Singh2007). To this end, the generated automata can be more complete to capture the important scenarios and in turn be too large for designers so as to specify, analyze, and verify manually.

To address the limitation of Yolum and Singh (Reference Yolum and Singh2002b, Reference Yolum and Singh2004) regarding the verification issue, Yolum (Reference Yolum2007) presented the main generic properties that can help protocol designers analyze and correct the development of commitment-based protocols by (1) signaling possible errors and inconsistencies; and (2) determining the applicability of protocols. Technically, such properties are categorized into three classes: effectiveness, consistency, and robustness. Yolum then presented algorithms that could be implemented in any ‘available software tool’ to semi-automatically verify those properties at design time. However, because there is no experimental results, then we cannot be able to evaluate the performance and efficiency of the introduced algorithms.

Based on Yolum and Singh’s representation of commitment actions (Yolum & Singh, Reference Yolum and Singh2004) in terms of the EC axioms, Chesani et al. (Reference Chesani, Mello, Montali and Torroni2009) proposed a framework composed of a logical language and verification procedure. The language defines commitments, commitment actions, deadlines, and ‘compensations actions’ that can arise when deadline is expired. Technically, they modeled commitments as EC fluents and provided an axiomatization of commitment actions in terms of EC primitives. For example:

Example 28 When a commitment C(Mer, Cus, deliverGoods) has been established and the deadline has not expired yet, a fluent waiting (C(Mer, Cus, deliverGoods)) holds:

$$\eqalignno{ &#x0026; initiates(E,\,waiting(C(Mer,\,Cus,\,deliverGoods)),\,T)\leftarrow \cr &#x0026; \quad \ \ create(E,\,Mer,\,C(Mer,\,Cus,\,deliverGoods)) $$

where E is an event and T the absolute time at which the commitment has been established.

When an event regarding the discharge of this commitment occurs, the waiting(C (Mer, Cus, deliverGoods)) fluent is terminated and a new satisfied (C (Mer, Cus, deliverGoods)) fluent is instantiated, which in principle means the commitment has been successfully discharged. This would be expressed as:

$$\eqalignno{ &#x0026; terminates(E,\,waiting(C(Mer,\,Cus,\,deliverGoods)),\,T)\leftarrow \cr &#x0026; \ \quad \qquad holds\_at(waiting(C(Mer,\,Cus,\,deliverGoods)),\,T), \cr &#x0026; \qquad \qquad \ \,discharge(E,\,Mer,\,C(Mer,\,Cus,\,deliverGoods)) \cr &#x0026; \quad initiates(E,\,Satisfied(C(Mer,\,Cus,\,deliverGoods)),\,T)\leftarrow \cr &#x0026; \qquad \quad \ holds\_at(waiting(C(Mer,\,Cus,\,deliverGoods)),\,T), \cr &#x0026; \qquad \qquad \ \,discharge(E,\,Mer,\,C(Mer,\,Cus,\,deliverGoods)) $$

A fluent d_check (C, T _D) is introduced to check whether a commitment C is satisfied at time T _D. It can be instantiated as:

$$\eqalignno{ &#x0026; initiates(E,\,d\_check(C(Mer,\,Cus,\,deliverGoods),\,When),\,T)\leftarrow \cr &#x0026; \qquad \qquad \qquad \quad \ \ \, create(E,\,Mer,\,C(Mer,\,Cus,\,deliverGoods)) \cr &#x0026; \qquad \qquad \qquad \quad deadlines(C(Mer,\,Cus,\,deliverGoods),\,Delay) \cr &#x0026; \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \ When\,is\,T{\plus}Delay. $$

deadlines (C (Mer, Cus, deliverGoods), 3) means that the commitment should be fulfilled within 3 time units from its instantiation. Their verification procedure (or monitoring tool) is developed to track the commitment statuses at run time. Specifically, they implemented the above defined language using REC. REC basically builds on top of the computational logic framework, named SCIFF (Alberti et al., Reference Alberti, Chesani, Gavanelli, Lamma, Mello and Torroni2008), which in turn extends Fung and Kowalski’s IFF proof procedure for abductive logic programming. Notice that the implementation of EC is performed using the jREC Java archive tool. The authors opted REC because it is ‘not goal-directed but event-driven’, that is the fluents’ statuses can be modified at run time when certain events occur. By defining the set of possibly observed events at certain times, the values of deadline and the corresponding fluents, the monitor tool computes a set of observed events that comply with the defined axioms encoding the set of possible events and then returns either true or the state of commitments in questions.

The authors (Chesani et al., Reference Chesani, Mello, Montali and Torroni2013) recently extended their CML Torroni et al., (2010) by considering (1) conditional commitments; (2) data, variables, and metric time to deal with temporal aspects (e.g. deadlines) that are compatible with dynamic settings, but are missing in temporal logics (e.g. LTL, CTL, and CTL*); and (3) other commitment actions, such as detach, expire, and violate. The authors also mapped each possible commitment state into a fluent state to explicitly refer to ‘the state in the domain dependent theory’; instead of setting a correspondence between ‘bringing about some property P’ and ‘initiating fluent P’ as done by Yolum and Singh (Reference Yolum and Singh2004).

Example 29 Consider the following axiom:

$$\eqalignno{ &#x0026; create(promise(Ag_{1} ,\,Ag_{2} ,\,deliverGoods),\,C(Ag_{1} ,\,Ag_{2} ,\,property(e(T_{1} ,\,T_{2} ),\,deliverGoods)),\,T) \cr &#x0026; \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \,\leftarrow T_{1} \,is\,T{\plus}1,\,T_{2} \,is\,T{\plus}3 $$

Suppose we observe the following event: promise (Mer, Cus, deliverGoods) at time 20. As this event copes with the description of create (…), then Mer becomes committed to deliver the requested goods between time 21 and time 23: C (Mer, Cus, property(e(21, 23), deliverGoods)).

From agent communication perspective, the proposed semantics for ACL messages meets the first four criteria. On the one hand, the main limitation of the proposed CML is that we cannot express commitments where antecedent and consequence ‘overlap’. This is because a conditional commitment’s consequence should be brought about strictly after the original commitment is detached, and in turn create a new one. Simply put, the consequence and antecedent of commitments should be held in different states. On the other hand, to check REC’s scalability, the authors considered up to 20 000 rental cars (reflecting the state space) and up to 200 customers. In general, for a specification to be effective, and thus to reach its aim, it is fundamental to consider the characteristics of the interacting agents (e.g. local states, local actions, local polices, etc.) and of the formal modeled systems it will be settled in. Thus, we do not know how efficient such characteristics will be, if implemented, however, we suspect scalability might be an issue. This framework also lacks formal semantics for commitments because they are modeled as fluents (cf. Remark 1). As REC is in fact a first-order logic with variables and data, it is undecidable (Emerson, Reference Emerson1990). Thus, it would be hard to verify commitment-based protocol properties (e.g. reachability, safety, liveness) typically checked using model checking techniques (Bentahar et al., Reference Bentahar, El-Menshawy, Qu and Dssoulia2012; El-Menshawy et al., Reference El-Menshawy, Bentahar, El-Kholy and Dssouli2013b). By contrast, model checking appears to be less feasible, but it is not completely impossible if a real-time formalization is required (cf. real-time CTL supported by the NuSMV tool).

7.2 Action logical language: C⁺

Chopra and Singh (Reference Chopra and Singh2006) specified commitment-based protocols using ‘non-monotonic commitment machines’ presented first in Chopra and Singh (Reference Chopra and Singh2004) with the action logical description language C⁺ developed in Giunchiglia et al. (Reference Giunchiglia, Lee, Lifschitz, McCain and Turner2004). A non-monotonic commitment machine is a modification of a commitment machine (Yolum & Singh, Reference Yolum and Singh2002a) to consider situations when agents must ‘act with incomplete information’; so they need non-monotonic or defeasible reasoning. The authors adopted C⁺ as it is easy to add or remove certain interactions to an existing specification. As in EC, fluents and actions are the basic components in the C⁺ language. In this approach, a protocol specification consists of a set of causal laws, which in turn link messages specified as actions that occur at particular time points to their effects on commitments. More precisely, description of actions specifies a transition system of a protocol, a graph with states and actions wherein commitments are modeled as ‘inertial fluents’ (cf. Remark 1 about the problem of using fluents to model commitments). The interpretation (i.e. semantic value) of such fluents persists from one state to the next state ‘unless changed by some other law’. The authors presented a set of rules in the form of axioms to represent and in turn define the intended meanings of commitment actions as follows (Chopra & Singh, Reference Chopra and Singh2004):

$$\hskip -60pt \matrix{ {(1)\,Create(i,j,p)\,causes\,C(i,j,p)} \hfill &#x0026; {(2)\,Discharge(i,j,p)\,causes\,\neg C(i,j,p)} \hfill \cr {(3)\,Cancel(i,j,p)\,causes\,\neg C(i,j,p)} \hfill &#x0026; {(4)\,Delegate(i,j,p,k)\,causes\,\neg C(i,j,p)\,\,\&#x0026;\,\,(k,j,p)} \hfill \cr {(5)\,Release(i,j,p)\,causes\,\neg C(i,j,p)} \hfill &#x0026; {(6)\,Assign(i,j,p,k)\,causes\,\neg C(i,k,p)\,\,\&#x0026;\,\,(i,j,p)} \hfill \cr } $$

For instance, the axiom of the discharge action means that when the discharge action happens, then the commitment is terminated (¬C(i, j, p)) in ‘the next state’ according to the following rule (Chopra & Singh, Reference Chopra and Singh2004): a causes f, where a is an action and f is a fluent happening in the next state. Notably, this approach meets formal, declarative, and meaningful criteria. As in Yolum and Singh (Reference Yolum and Singh2004), the authors exploited a static verification technique in the form of reasoning rules in order to verify the compliance of agent behaviors against a given protocol’s state machine. As mentioned in the evaluation of Yolum and Singh (Reference Yolum and Singh2004), this technique is inapplicable in complex systems because the verification procedure needs to record all possible protocol runs from initial and final protocol states to search for commitment states in question.

Desai and Singh (Reference Desai and Singh2007) presented a ‘modular action description’ geared toward protocols, an extension of the causal logic C⁺ (Giunchiglia et al., Reference Giunchiglia, Lee, Lifschitz, McCain and Turner2004) in order to refine and compose protocols from existing ones. This approach enhances the approach of Chopra and Singh (Reference Chopra and Singh2006) for representing individual protocols. However, as in Chopra and Singh (Reference Chopra and Singh2006), Desai et al.’s commitments are modeled as inertial fluents and the operational semantics of commitment actions is delineated by a set of axioms. Composition rules satisfying some requirements are also defined as a set of C⁺ axioms without checking the correctness specification of a protocol composition. Such a challenge is addressed in Desai et al. (Reference Desai, Cheng, Chopra and Singh2007) (cf. Section 4).

To conclude this section, the advantages and disadvantages of EC and C⁺ and the comparisons between them are discussed in Artikis et al. (Reference Artikis, Sergot and Pitt2009). Artikis and Pitt (Reference Artikis and Pitt2009) showed that the abductive EC planner and causal calculator that execute commitment-based protocols specified in EC and C⁺ can be employed, ‘in principle, for the provision of both design time services—for instance, proving protocol properties—and run-time services—for example, calculating the commitments current at each time—for the benefit of the agents or their designers. These implementations, however, can become inefficient when considering large OASs [open agent systems]’. On the other hand, model checking in principle provides a full automatic verification and is effective in large and complex systems. Furthermore, there is no formal semantics for commitments as they are modeled simply as fluents (cf. Remark 1). Table 6 summarizes our results of evaluating the proposals that advocate those logical languages of actions.

Table 6

Summary of logical languages of actions and commitment-based agent communication