Skip to main content
Thesis defences

PhD Oral Exam - Faisal Al-Saqqar, Computer Science

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


Date & time
Thursday, September 3, 2015
10 a.m. – 1 p.m.
Cost

This event is free

Organization

School of Graduate Studies

Contact

Sharon Carey
514-848-2424, ext. 3802

Wheel chair accessible

Yes

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

Abstract

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 exchange, negotiate, and reason about 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 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 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 Polynomial Space (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 Polynomial (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. The obtained results show the effectiveness of our model checking approaches when the system scales up.


Back to top

© Concordia University