A logic of agent programs
Natasha Alechina, Mehdi M. Dastani, Brian S. Logan, John-Jules Meyer · 2007
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 implementa-tion 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 Sim-pleAPL and the models of the logic for two example program execution strategies. We show how to translate agent pro-grams written in SimpleAPL into expressions of the logic, and give an example in which we show how to verify correct-ness properties for a simple agent program.