Doctoral Thesis Defense - April 11, 2016: Formal Specification and Automatic Verification of Multi-Agent Conditional Commitments and Their Applications

Warda El Kholy

Monday, April 11, 2016 at 2:00 p.m.
Room EV003.309

You are invited to attend the following Ph.D (Information and Systems Engineering) thesis examination.

Examining Committee

Dr. A. Agarwal, Chair
Dr. R. Dssouli, Co-Supervisor
Dr. J. Bentahar, Co-Supervisor
Dr. A. Ben Hamza, CIISE Examiner
Dr. O. Ormandjieva, External Examiner (CSSE)
Dr. B. Fung, External Examiner (McGill University)
Dr. H. Boucheneb, External Examiner (Ecole Polytechnique de Montreal)

Abstract

Modeling agent communication using social commitments in the form of obligatory contracts among intelligent agents in a multi-agent system (MAS) provides a quintessential basis for capturing flexible and declarative interactions and helps in addressing the challenge of ensuring compliance with specifications.  However, on the one hand, social commitments exclusively are not able to model agent communication actions, the cornerstone of the fundamental agent communication theory, namely speech act theory.  These actions provide mechanisms for dynamic interactions and enable designers to track the evolution of active commitments.  On the other hand, the designers of the system cannot guarantee the emergence of expected behaviors, such as self-contained intelligent agent complies with its protocols and honors its activated commitments.  Moreover, the designers might still wish to develop effective and scalable algorithms to tackle the problem of model checking complex interactions modeled by conditional commitments and conditional commitment actions and regulated by commitment-based protocols at design time.  Conditional commitments are a natural and universal frame of social commitments and cope with business conditional contracts.  This dissertation is in principle about addressing two open challenging issues: 1) formally defining computationally grounded semantics for agent communication messages in terms of conditional commitments and associated actions (fulfill, cancel, release, assign, and delegate), which is yet to be studied; and 2) developing a symbolic algorithm dedicated to tackle the raised model checking problem and to ensure the development of correct systems.

In this dissertation, we start with distinguishing between two types of conditional commitments: weak and strong.  Weak conditional commitments are those that can be activated even if the antecedents will never be satisfied, while strong conditional commitments are those that can be solely activated when there is at least one possibility to satisfy their assigned antecedents.  We develop a branching-time temporal logic called CTL ^cc,α that extends computation tree logic (CTL) with new modalties for representing and reasoning about the two types of conditional commitments and their actions using the formalism of interpreted systems.  We present a set of valid properties, a set of reasoning rules, and a set of action postulates in order to explore  the capabilities of CTL^cc,α.  Furthermore, we propose a new life cycle of conditional commitments.  Having a new logic (CTL ^cc,α), we introduce a new symbolic algorithms from scratch, we extend the standard CTL model checking algorithm with symbolic algorithms needed for new modalities.  We also investigate important theoretical results (soundness and termination) of the algorithm.  Given that, we completely implement our algorithm and then assemble it on top of the symbolic model checker MCMAS, developed to automatically and directly test MAS specifications.  The resulting symbolic model checker is so-called MCMAS+.  We extend MCMAS's input modeling and encoding language called ISPL with shared and unshared variables needed for agent interactions and with the syntactic grammar of new modalities to produce a new one called ISPL+.  We also extend the MCMAS's graphical user interface to display verified models to reduce inefficient and labor-intensive processes performed by the designers.
 

To evaluate the performance of the developed algorithm, we analyze its time and space computational complexity.  The computed time and space complexity are P-complete for explicit models and PSPACE-complete for concurrent programs.  Such results are positive because model checking CTL ^cc,α has the same time and space complexity of model checking CTL although CTL ^cc,α extends CTL.  Therefore, CTL ^cc,α balances between expressive power and verification efficiency.  Regarding the feasibility aspect, we apply our processes, and web service compositions.  The MAS paradigm is successfully employed in these domains wherein a component is represented, implemented and enacted by an agent.  The proposed approach improved the employed MAS paradigm by formally modeling and automatically verifying interactions among participating agents so that the bad behaviors can be detected and then eliminated or repaired at design time and the confidence on the safety, efficiency and robustness is increased.  We conduct extensive experiments to evaluate the computational performance and scalability of MCMAS+ using very large case studies.  The obtained results strongly confirm the theoretical findings and make MCMAS+ practical.  We finally compare our approaches in terms of execution time, memory use and number of considered intelligent agents.