Formal verification of multi-agent systems behaviour emerging from cognitive task analysis

The main goal of this paper is to present a novel formal approach to the verification of cognitive task analysis (CTA), an analytic tool that has been successfully used in the design of reactive behaviours, on multi-agent architectures. To achieve this, a formal logical system is developed, whose pu...

Full description

Saved in:
Bibliographic Details
Published in:Journal of experimental & theoretical artificial intelligence 2003-10, Vol.15 (4), p.407-431
Main Authors: Laureano-Cruces, Ana Lilia, Barceló-Aspeitia, Axel Arturo
Format: Article
Language:English
Subjects:
artificial intelligence
behaviour-based agents
cognitive task analysis
formal language
modal logic
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The main goal of this paper is to present a novel formal approach to the verification of cognitive task analysis (CTA), an analytic tool that has been successfully used in the design of reactive behaviours, on multi-agent architectures. To achieve this, a formal logical system is developed, whose purpose is to formally check the possible success or failure of the resulting implementation. This logic's focus is on modelling an agent's behaviour based on her goals, perceptions and actions. The article starts by giving a brief introduction to current research in reactive systems and cognitive task analysis. Simple definitions are offered of the basic concepts in these fields: agent, object, reactive behaviour, control, etc. As illustration, the paper offers the results of applying CTA to a simple model of postal delivery. Then, the syntax and semantics of the proposed logic are defined. Finally, the logic is applied to the verification of some of the behaviours resulting of the previous CTA analysis.
ISSN:0952-813X
1362-3079
DOI:10.1080/0952813031000119719