CTL AgentSpeak(L): A specification language for agent programs

This work introduces CTL AgentSpeak(L), a logic to specify and verify expected properties of rational agents implemented in the well-known agent oriented programming language AgentSpeak(L). Our approach is closely related to the BDI CTL multi-modal logic, used to reason about agents in terms of thei...

Full description

Saved in:
Bibliographic Details
Published in:Journal of algorithms 2009, Vol.64 (1), p.31-40
Main Authors: Guerra-Hernández, Alejandro, Castro-Manzano, José Martín, El Fallah Seghrouchni, Amal
Format: Article
Language:English
Subjects:
AgentSpeak(L)
Commitment
Computer Science
Reconsideration
Specification
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:This work introduces CTL AgentSpeak(L), a logic to specify and verify expected properties of rational agents implemented in the well-known agent oriented programming language AgentSpeak(L). Our approach is closely related to the BDI CTL multi-modal logic, used to reason about agents in terms of their beliefs ( B), desires ( D), intentions ( I), and the temporal logic CTL. A new interpretation for the temporal operators, grounded in the transition system induced by the operational semantics of AgentSpeak(L), is proposed. The main contribution of the approach is a better understanding of the relation between the programming language and its logical specification, enabling us to prove expected or desired properties for any agent programmed in the language, e.g., commitment strategies. The results, as well as the specification language proposed, are very useful to reconcile computational and philosophical aspects of practical reasoning, e.g., approaching single-minded commitment as a policy-based reconsideration case.
ISSN:0196-6774
1090-2678
DOI:10.1016/j.jalgor.2009.02.003