Formal Specification Language for Agent Oriented Systems

Background

This section describes related work that exists in applying formal methods to specify software systems in specific agent oriented software systems. The state of the art with respect to the agent oriented software specification is also described in this section.

de Vries et al. (de Vries et al., 2001) introduced a new operational model of agents that describes the interaction of agents with each other and with the environment. An agent is viewed as a program that has a state. An agent’s state has two parts: a sense buffer that is used to store the observed and communicated information, and the mental state that consists of a set of mental formulas. Kinny (Kinny, 2001) introduced an algebraic approach that describes the operational semantics of agent computation. Kinny defined agents as a strong encapsulation of beliefs, intentions, and plans. The agent interacts with the environment using two interfaces namely: sensors and effectors. The framework defined by Kinny follows an algebraic approach. The computation specified in the algebraic approach is kept separate from the agent’s program. Bosse et al. (Bosse et al., 2006) proposed the predicate logic Temporal Trace Language (TTL) for formally specifying multi-agent systems. Both quantitative and qualitative aspects of agent systems were specified using the Temporal Trace Language.