Login | Register

Automatic Transformation-Based Model Checking of Multi-agent Systems


Automatic Transformation-Based Model Checking of Multi-agent Systems

Laarej, Amine (2020) Automatic Transformation-Based Model Checking of Multi-agent Systems. Masters thesis, Concordia University.

[thumbnail of Laarej_MASc_F2020.pdf]
Text (application/pdf)
Laarej_MASc_F2020.pdf - Accepted Version
Available under License Spectrum Terms of Access.


Multi-Agent Systems (MASs) are highly useful constructs in the context of real-world software applications. Built upon communication and interaction between autonomous agents, these systems are suitable to model and implement intelligent applications. Yet these desirable features are precisely what makes these systems very challenging to design, and their compliance with requirements extremely difficult to verify. This explains the need for the development of techniques and tools to model, understand, and implement interacting MASs. Among the different methods developed, the design-time verification techniques for MASs based on model checking offer the advantage of being formal and fully automated. We can distinguish between two different approaches used in model checking MASs, the direct verification approach, and the transformation-based approach. This thesis focuses on the later that relies on formal reduction techniques to transform the problem of model checking a source logic into that of an equivalent problem of model checking a target logic.
In this thesis, we propose a new transformation framework leveraging the model checking of the computation tree logic (CTL) and its NuSMV model checker to design and implement the process of transformation-based model checking for CTL-extension logics to MASs. The approach provides an integrated system with a rich set of features, designed to support the transformation process while simplifying the most challenging and error-prone tasks. The thesis presents and describes the tool built upon this framework and its different applications. A performance comparison with MCMAS, the model checker of MASs, is also discussed.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering
Item Type:Thesis (Masters)
Authors:Laarej, Amine
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Quality Systems Engineering
Date:August 2020
Thesis Supervisor(s):Bentahar, Jamal and Dssouli, Rachida
ID Code:987078
Deposited By: AMINE LAAREJ
Deposited On:25 Nov 2020 15:38
Last Modified:25 Nov 2020 15:38
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