Formal verification of multi-agent systems behaviour emerging from cognitive task analysis
Ana Lilia Laureano‐Cruces, Axel Arturo Barceló Aspeitia · Journal of Experimental & Theoretical Artificial Intelligence · 2003
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.