A Caltech Library Service

Systematic Design and Formal Verification of Multi-Agent Systems


Pilotto, Concetta (2011) Systematic Design and Formal Verification of Multi-Agent Systems. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/SCQF-VP66.


This thesis presents methodologies for verifying the correctness of multi-agent systems operating in hostile environments. Verification of these systems is challenging because of their inherent concurrency and unreliable communication medium. The problem is exacerbated if the model representing the multi-agent system includes infinite or uncountable data types.

We first consider message-passing multi-agent systems operating over an unreliable communication medium. We assume that messages in transit may be lost, delayed or received out-of-order. We present conditions on the system that reduce the design and verification of a message-passing system to the design and verification of the corresponding shared-state system operating in a friendly environment. Our conditions can be applied both to discrete and continuous agent trajectories.

We apply our results to verify a general class of multi-agent system whose goal is solving a system of linear equations. We discuss this class in detail and show that mobile robot linear pattern-formation schemes are instances of this class. In these protocols, the goal of the team of robots is to reach a given pattern formation.

We present a framework that allows verification of message-passing systems operating over an unreliable communication medium. This framework is implemented as a library of PVS theorem prover meta-theories and is built on top of the timed automata framework. We discuss the applicability of this tool. As an example, we automatically check correctness of the mobile robot linear pattern formation protocols.

We conclude with an analysis of the verification of multi-agent systems operating in hostile environments. Under these more general assumptions, we derive conditions on the agents' protocols and properties of the environment that ensure bounded steady-state system error. We apply these results to message-passing multi-agent systems that allow for lost, delayed, received out-of-order or forged messages, and to multi-agent systems whose goal is tracking time-varying quantities. We show that pattern formation schemes are robust to leaders dynamics, i.e., in these schemes, followers eventually form the pattern defined by the new positions of the leaders.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:verification, stability, convergence, PVS theorem prover
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Chandy, K. Mani
Thesis Committee:
  • Chandy, K. Mani (chair)
  • Ledyard, John O.
  • Murray, Richard M.
  • Doyle, John Comstock
  • Low, Steven H.
Defense Date:28 March 2011
Additional Information:Thesis listed in 2011 Commencement program has different title: Local-to-Global in Multi-Agent Systems.
Record Number:CaltechTHESIS:05232011-013046516
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:6418
Deposited By: Concetta Pilotto
Deposited On:06 Jun 2011 23:31
Last Modified:09 Oct 2019 17:09

Thesis Files

PDF (Thesis) - Final Version
See Usage Policy.


Repository Staff Only: item control page