Abstract
Planning and distributed task allocation are considered challenging problems. To address them, autonomous agents called planning agents situated in a multi-agent system should cooperate to achieve planning and complete distributed tasks. We propose a solution for distributed task allocation where agents dynamically allocate the tasks while they are building the plans. We model and verify some properties using computation tree logic (CTL) with the model checker its-ctl. Lastly, simulations are performed to verify the effectiveness of our proposed solution. The result proves that it is very efficient as it requires little message exchange and computational time. A benchmark production system is used as a running example to explain our contribution.