5.11.2009

Reasoning about Code Patterns in Agent-Oriented Programming

The mainstream approach to design of agent programming languages is to choose a set of features with a particular semantics. The language designer's choices thus impose strong constraints on the architecture of the implemented agents as well as only a limited toolbox of high-level language constructs for encoding the agent program.

As an alternative, we discuss a purely syntactic approach to designing an agent programming language, based on the notion of Behavioural State Machines (BSM). To reason about the execution of agent programs, we propose to use program annotations in linear time logic LTL, and subsequently introduce DCTL*, an extension of the branching time logic CTL* with features of dynamic logic. We show how DCTL* specifications can be used to prove relevant properties of BSM code patterns. We also point out that DCTL* allows for natural verification of BSM agent program