Towards a Verification Framework for Communicating Rational Agents.

We present an abstract framework for verifying communicative actions for rational agent programming languages. Firstly, a multi-agent verification logic based on the computational semantics is introduced; and subsequently, this multi-agent logic is embedded into a more expressive modal logic over a standard run-based semantics. We formally relate both logics, prove expressivity results, and argue why it is useful to have a (more expressive) standard modal logic and semantics at hand. [ABSTRACT FROM AUTHOR]