A realistic model of multi-agent planning must allow us to formalize notions which are absent in classical planning, such as communication and knowledge. We investigate multi-agent planning based on a simple logic of knowledge that is grounded on the visibility of propositional variables. Using such a formal logic allows us to prove the existence of a plan given the description of the individual actions. We present an encoding of multi-agent planning problems expressed in this logic into the standard planning language PDDL. The solvability of a planning task is reduced to a model checking problem in a dynamic extension of our logic, proving its complexity. Feeding the resulting problem into a PDDL planner provides a provably correct plan for the original multi-agent planning problem. We apply our method on several examples such as the gossip problem.

The gossip problem, in which information (secrets) must be shared among a certain number of agents using the minimum number of calls, is of interest in the conception of communication networks and protocols. We extend the gossip problem to arbitrary epistemic depths. For example, we may require not only that all agents know all secrets but also that all agents know that all agents know all secrets. We give optimal protocols for the generalised gossip problem, in the case of two-way communications, one-way communications and parallel communication. In the presence of negative goals testing the existence of a successful protocol is NP-complete.