Existing approaches about defining formal semantics of commitment usually consider operations as axioms or constrains on top of the commitment semantics, which fail to capture the meaning of interactions that are central to real-life business scenarios. Furthermore, existing semantic frameworks using different logics do not gather the full semantics of commitment operations and semantics of social commitments within the same framework. This paper develops a novel unified semantic model for social commitments and their operations. It proposes a logical model based on a new logic extending CTL* with commitments and operations to specify agent interactions. We also propose a new definition of assignment and delegation operations by considering the relationship between the original and new commitment contents. We prove that the proposed model satisfies some properties that are desirable when modeling agent interactions in MASs and introduce a NetBill protocol as a running example to clarify the automatic verification of this model. Finally, we present an implementation and report on experimental results of this protocol using the NuSMV and MCMAS symbolic model checkers. © 2010 Springer-Verlag.
CITATION STYLE
El-Menshawy, M., Bentahar, J., & Dssouli, R. (2010). Verifiable semantic model for agent interactions using social commitments. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6039 LNAI, pp. 128–152). https://doi.org/10.1007/978-3-642-13338-1_8
Mendeley helps you to discover research relevant for your work.