TY - GEN
T1 - Verifiable semantic model for agent interactions using social commitments
AU - El-Menshawy, Mohamed
AU - Bentahar, Jamal
AU - Dssouli, Rachida
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
KW - accessibility relations
KW - Social commitments
KW - the NuSMV and MCMAS model checkers
KW - two and three party operations
UR - http://www.scopus.com/inward/record.url?scp=77954419682&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-13338-1_8
DO - 10.1007/978-3-642-13338-1_8
M3 - Conference contribution
AN - SCOPUS:77954419682
SN - 3642133371
SN - 9783642133374
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 128
EP - 152
BT - Languages, Methodologies, and Development Tools for Multi-Agent Systems - Second International Workshop, LADS 2009, Revised Selected Papers
T2 - 2nd International Workshop on Languages, Methodologies and Development Tools for Multi-agent Systems, LADS 2009
Y2 - 7 September 2009 through 9 September 2009
ER -