Automated verification of multi-agent programs

Berndt Muller, M. Fisher, R.H. Bordini, L.A. Dennis

Allbwn ymchwil: Pennod mewn Llyfr/Adroddiad/Trafodion CynhadleddCyfraniad i gynhadleddadolygiad gan gymheiriaid

Crynodeb

In this paper, we show that the flexible model-checking of multi-agent systems, implemented using agent-oriented programming languages, is viable thus paving the way for the construction of verifiably correct applications of autonomous agents and multi-agent systems. Model checking experiments were carried out on AJPF (agent JPF), our extension of Java PathFinder that incorporates the agent infrastructure layer, our unifying framework for agent programming languages. In our approach, properties are specified in a temporal language extended with (shallow) agent-related modalities. The framework then allows the verification of programs written in a variety of agent programming languages, thus removing the need for individual languages to implement their own verification framework. It even allows the verification of multi-agent systems comprised of agents developed in a variety of different (agent) programming languages. As an example, we also provide model checking results for the verification of a multi-agent system implementing a well-known task sharing protocol.
Iaith wreiddiolSaesneg
TeitlN/A
Tudalennau69-78
Dynodwyr Gwrthrych Digidol (DOIs)
StatwsCyhoeddwyd - 1 Hyd 2008
Digwyddiad 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008) - Italy
Hyd: 15 Medi 200819 Medi 2008

Cynhadledd

Cynhadledd 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008)
Cyfnod15/09/0819/09/08

Ôl bys

Gweld gwybodaeth am bynciau ymchwil 'Automated verification of multi-agent programs'. Gyda’i gilydd, maen nhw’n ffurfio ôl bys unigryw.

Dyfynnu hyn