You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact

Verifiable Strategy Synthesis for Multiple Autonomous Agents: A Scalable Approach



Publication Type:

Journal article


International Journal on Software Tools for Technology Transfer




Path planning and task scheduling are two challenging problems in the design of multiple autonomous agents. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space explosion problem that makes it inefficient at solving the problems when the number of agents is large, which is often the case in realistic scenarios. In this paper, we propose a new version of our novel approach called MCRL that integrates model checking and reinforcement learning to alleviate this scalability limitation. We apply this new technique to synthesize path planning and task scheduling strategies for multiple autonomous agents. Our method is capable of handling a larger number of agents if compared to what is feasibly handled by the model-checking technique alone. Additionally, MCRL also guarantees the correctness of the synthesis results via post-verification. The method is implemented in UPPAAL STRATEGO and leverages our tool MALTA for model generation, such that one can use the method with less effort of model construction and a higher efficiency of learning than those of the original MCRL. We demonstrate the feasibility of our approach on an autonomous quarry industrial case study, and discuss the strengths and weaknesses of the methods.


author = {Rong Gu and Peter Jensen and Danny Poulsen and Cristina Seceleanu and Eduard Paul Enoiu and Kristina Lundqvist},
title = {Verifiable Strategy Synthesis for Multiple Autonomous Agents: A Scalable Approach},
volume = {1},
number = {1},
pages = {1--2},
month = {February},
year = {2022},
journal = { International Journal on Software Tools for Technology Transfer},
publisher = {Springer},
url = {}