Tech Reports

ULCS-05-012

A Formal Semantics for Gaia Liveness Rules and Expressions

Tim Miller and Peter McBurney

Abstract

The Gaia methodology is a development methodology for multi-agent systems that uses the concept of roles to define behaviour. Gaia uses liveness expressions, which are expressions written in a formal syntax that are used to define the ongoing behaviour of a role; and liveness rules, which are expressions specifying the behaviour of roles relative to each other in a system. However, while the syntax is formal, a formal semantics has not been defined, and there is no theory for how to reason about and manipulate these expressions. In this paper, we present a formal semantics for liveness rules and expressions, and discuss our work in developing axioms about them. We also discuss the introduction of a new operator for defining the complement of expressions; that is, the behaviour that falls outside of the liveness expression. This provides more flexibility when reasoning about and manipulating these expressions.

Keywords: multi-agent systems, agent-oriented development methodologies, Gaia design methodology, liveness expressions, Kleene algebra.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.