Using process calculi for plan verification in multiagent planning

Abstract

Multiagent planning is a coordination technique used for deliberative acting of a team of agents. One of vital planning techniques uses declarative description of agents’ plans based on Finite State Machines and their later coordination by intersection of such machines with successive verification of the resulting joint plans. In this work, we firstly introduce a method of multiagent planning which makes use of projections of other agent actions in order to iteratively search for a skeleton of a multiagent plan. Secondly, we describe integration of the static analysis provided by process calculi type systems for approximate verification of exchanged local plans. Furthermore, we introduce an alternative method to accomplish the above verification by a classical planner. Finally, we compare our approach with current state-of-the-art planner on an extensive benchmark set.