Abstract
This paper has two purposes. First, it defines a formal language, for specifying agent-based applications, that integrates linear temporal logic to the Z notation. This integration offers a language that is expressive enough to cover both individual agent aspects (e.g., knowledge, goals and roles) as well as collective aspects (e.g., cooperation strategy, organization structure and collective behaviour). Second, it proposes a formal methodology for designing agent-based applications using stepwise refinements. The main contribution of our design process consists of a set of methodological principles and hints that help the user to build, in a systematic and incremental way, a verified design starting from abstract requirements. This approach will be illustrated by developing an agent-based solution for the air traffic control problem.
Get full access to this article
View all access options for this article.