AgentSpeak中意图生成过程的可靠性与完整性研究

摘要

意图生成是BDI型Agent为实现目标而产生动作序列的过程.验证软件Agent中意图生成的正确性是A-gent编程语言中一个重要的研究问题.针时软件Agent中意图执行的正确性,以当前最流行的BDI型Agent编程语言AgentSpeak为例,证明了软件Agent意图执行的有效性.首先根据AgentSpeak的语法构造了一个解释系统,并给出了该解释系统的满足关系.从而得出了AgentSpeak的模型论语叉.在该模型论语叉的基础上,结合由Moreira和Bordini所给出的操作语义,i～-gB了AgentSpeak的意图生成等价定理:AgentSpeak语言中模型论语义的意图等价于AgentSpeak程序操作语义的意图.由此可得出结论--AgentSpeak中的意图执行是可靠而完整的,从而验证了AgentSpeak中软件Agent意图完成目标的正确性.%Intention production is the procedure that BDI Agent drafts an action sequence to realize a goal. However, it is also a big obstacle to verify the validity of Agent intention produced by the specification of Agent Programming Language(APL). In this paper, to prove the validity of intention execution in AgentSpeak, we constructed a model-theoretic semantics and a formal interpretation of Agent program’s intention. Then,on the bases of the model-theoretic semantics and the operational semantics presented by Moreira and Bordini, we proved the equivalence theorem: the intention in model-theoretic semantics of AgentSpeak language is equivalent with the one in operational semantics of AgentSpeak program. According to the equivalence theorem, we can get the conclusion that intention execution of AgentSpeak is sound and complete.