Home // COMPUTATION TOOLS 2011, The Second International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

Formal Verification of Parameterized Multi-agent Systems Using Predicate Diagrams*

Authors:
Cecilia E. Nugraheni

Keywords: multi-agent systems; parameterized systems; verification; predicate diagrams*; TLA*; TLA+

Abstract:
This paper presents a formal diagram-based verification technique for multi-agent systems. A multi-agent system is a collection of intelligent agents that interact with each others and work together to achieve a goal.We view multi-agent systems as parameterized systems which are systems that consist of several similar processes whose number is determined by an input parameter. The motivation of this work is that by treating multi-agent systems as parameterized systems, the specification and verification processes can be done in the same way regardless of the number of agents involved in the multi-agent systems. In this paper, we show how predicate diagrams* can be used to represent the abstractions of parameterized multi-agent systems described by specifications written in TLA*. The verification process is done by integrating deduction verification and algorithmic techniques. The correspondence between the original specification and the diagram is established by non-temporal proof obligations; whereas model checker SPIN is used to verify properties over finite-state abstractions.

Pages: 19 to 24

Copyright: Copyright (c) IARIA, 2011

Publication date: September 25, 2011

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-159-5

Location: Rome, Italy

Dates: from September 25, 2011 to September 30, 2011