IRUS Total

Abstraction in Model Checking Multi-Agent Systems

File Description SizeFormat 
Russo-F-2012-PhD-Thesis.pdf1.25 MBAdobe PDFView/Open
Title: Abstraction in Model Checking Multi-Agent Systems
Authors: Russo, Francesco
Item Type: Thesis or dissertation
Abstract: This thesis presents existential abstraction techniques for multi-agent systems preserving temporal-epistemic specifications. Multi-agent systems, defined in the interpreted system frameworks, are abstracted by collapsing the local states and actions of each agent. The goal of abstraction is to reduce the state space of the system under investigation in order to cope with the state explosion problem that impedes the verification of very large state space systems. Theoretical results show that the resulting abstract system simulates the concrete one. Preservation and correctness theorems are proved in this thesis. These theorems assure that if a temporal-epistemic formula holds on the abstract system, then the formula also holds on the concrete one. These results permit to verify temporal-epistemic formulas in abstract systems instead of the concrete ones, therefore saving time and space in the verification process. In order to test the applicability, usefulness, suitability, power and effectiveness of the abstraction method presented, two different implementations are presented: a tool for data-abstraction and one for variable-abstraction. The first technique achieves a state space reduction by collapsing the values of the domains of the system variables. The second technique performs a reduction on the size of the model by collapsing groups of two or more variables. Therefore, the abstract system has a reduced number of variables. Each new variable in the abstract system takes values belonging to a new domain built automatically by the tool. Both implementations perform abstraction in a fully automatic way. They operate on multi agents models specified in a formal language, called ISPL (Interpreted System Programming Language). This is the input language for MCMAS, a model checker for multi-agent systems. The output is an ISPL file as well (with a reduced state space). This thesis also presents several suitable temporal-epistemic examples to evaluate both techniques. The experiments show good results and point to the attractiveness of the temporal-epistemic abstraction techniques developed in this thesis. In particular, the contributions of the thesis are the following ones: • We produced correctness and preservation theoretical results for existential abstraction. • We introduced two algorithms to perform data-abstraction and variable-abstraction on multi-agent systems. • We developed two software toolkits for automatic abstraction on multi-agent scenarios: one tool performing data-abstraction and the second performing variable-abstraction. • We evaluated the methodologies introduced in this thesis by running experiments on several multi-agent system examples.
Issue Date: May-2011
Date Awarded: Feb-2012
URI: http://hdl.handle.net/10044/1/9294
DOI: https://doi.org/10.25560/9294
Supervisor: Lomuscio, Alessio
Author: Russo, Francesco
Department: Computing
Publisher: Imperial College London
Qualification Level: Doctoral
Qualification Name: Doctor of Philosophy (PhD)
Appears in Collections:Computing PhD theses

Unless otherwise indicated, items in Spiral are protected by copyright and are licensed under a Creative Commons Attribution NonCommercial NoDerivatives License.

Creative Commons