A Logic of Agent Programs

Natasha Alechina, Mehdi Dastani, Brian Logan, John-Jules Ch. Meyer

We present a sound and complete logic for reasoning about SimpleAPL programs. SimpleAPL is a fragment of the agent programming language 3APL designed for the implementation of cognitive agents with beliefs, goals and plans. Our logic is a variant of PDL, and allows the specification of safety and liveness properties of agent programs. We prove a correspondence between the operational semantics of SimpleAPL and the models of the logic for two example program execution strategies. We show how to translate agent programs written in SimpleAPL into expressions of the logic, and give an example in which we show how to verify correctness properties for a simple agent program.

Subjects: 7.1 Multi-Agent Systems; 9.3 Mathematical Foundations

Submitted: Apr 23, 2007

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.