A formal semantics for Gaia liveness rules and expressions. (14th December 2007)

• Record Type: Journal Article
• Authors: Miller, Tim; McBurney, Peter
• Is Part Of: International journal of agent-oriented software engineering. Volume 1:Number 3/4(2007)
• Page Start: 435
• Page End: 476
• Publication Date: 2007-12-14
• Subjects: multi-agent systems -- MAS -- agent-oriented development methodologies -- Gaia design methodology -- liveness expressions -- Kleene algebra -- semantics; Intelligent agents (Computer software) -- Periodicals; Software engineering -- Periodicals; Systems software -- Periodicals; 005.12
• Languages: English
• ISSNs: 1746-1375

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.