Validation and Verification of Joint-Actions in Multi-agent Planning

In multi-agent planning problem, multiple agents are involved in doing some task to achieve a common goal. At present, major approaches to multi-agent planning are decomposition, heuristic improvement, and joint-action planning. Joint-action is a special case of concurrent actions where, two or more agents perform the same action simultaneously. Joint-action executes if preconditions hold true, but it contains so many dynamic elements with it that make it so complex to be true. The aim of the study is to make an attempt to formalize the precondition of joint-action so that it can be ensured that joint-action going to be executed would execute correctly. In joint-action, two or more agents must be ready to perform a single action. In the literature, it is assumed that two or more agents become available at the same place and then are ready to execute the action, but in the real world this is not true. Naturally, there are different situations i.e. 1: both of the agents are not at same location, 2: agents may or may not be obliged to do the task, 3: agents may be busy in doing some other task and deadlock may happen, so this process involves agent´s synchronization, message passing and process synchronization. Because of this, the formalization of precondition becomes necessary and it ensure the correctness of action to be executed. This study made an attempt to formalize the precondition through BPMN and verifying it with a formal method i.e. Petri net. This work has a novelty as no one has made an attempt to formalize the precondition till today.