Login | Register

Analyzing the Interaction between Knowledge and Social Commitments in Multi-Agent Systems


Analyzing the Interaction between Knowledge and Social Commitments in Multi-Agent Systems

AL-Saqqar, Faisal (2015) Analyzing the Interaction between Knowledge and Social Commitments in Multi-Agent Systems. PhD thesis, Concordia University.

[thumbnail of Faisal_Thesis_Final.pdf]
Text (application/pdf)
Faisal_Thesis_Final.pdf - Accepted Version


Both knowledge and social commitments in Multi-Agent Systems (MASs) have long been under research independently, especially for agent communication. Plenty of work has been carried out to define their semantics. However, in concrete applications such as business settings and web-based applications, agents should reason about their knowledge and their social commitments at the same time, particularly when they are engaged in conversations. In fact, studying the interaction between knowledge and social commitments is still in its beginnings. Therefore, in this thesis, we aim to provide a practical and formal framework that analyzes the interaction between knowledge and communicative social commitments in MASs from the semantics, model checking, complexity, soundness and completeness perspectives.

To investigate such an interaction, we, first, combine CTLK (an extension of computation Tree Logic (CTL) with modality for reasoning about knowledge) and CTLC (an extension of CTL with modalities for reasoning about commitments and their fulfillments) in one new logic named CTLKC. By so doing, we identify some paradoxes in the new logic showing that simply combining current versions of commitment and knowledge logics results in a language of logic that violates some fundamental intuitions. Consequently, we propose CTLKC+, a new consistent logic of knowledge and commitments that fixes the identified paradoxes and allows us to reason about social commitments and knowledge simultaneously in a consistent manner. Second, we use correspondence theory for modal logics to prove the soundness and completeness of CTLKC+. To do so, we develop a set of reasoning postulates in CTLKC+ and correspond them to certain classes of frames. The existence of such correspondence allows us to prove that the logic generated by any subset of these postulates is sound and complete, with respect to the models that are based on the corresponding frames. Third, we address the problem of model checking CTLKC+ by transforming it to the problem of model checking GCTL∗ (a generalized version of Extended Computation Tree Logic (CTL∗) with action formulas) and ARCTL (the combination of CTL with action formulas) in order to respectively use the CWB-NC automata-based model checker and the extended NuSMV symbolic model checker. Moreover, we prove that the transformation techniques are sound. Fourth, we analyze the complexity of the proposed model checking techniques. The results of this analysis reveal that the complexity of our transformation procedures is PSPACE-complete for local concurrent programs with respect to the size of these programs and the length of the formula being checked. From the time perspective, we prove that the complexity of the proposed approaches is P-complete with regard to the size of the model and length of the formula. Finally, we implement our model checking approaches and report some experimental results by verifying the well-known NetBell payment protocol against some desirable properties.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (PhD)
Authors:AL-Saqqar, Faisal
Institution:Concordia University
Degree Name:Ph. D.
Program:Computer Science
Date:14 December 2015
Thesis Supervisor(s):Bentahar, Jamal
ID Code:980772
Deposited By: Faisal Suleiman Al-Saqqar
Deposited On:16 Jun 2016 15:30
Last Modified:18 Jan 2018 17:51
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top