Affiliations:
College of Intelligence Science and Technology, National University of Defense Technology, Kaifu District, Changsha City, HunanProvince, China
Correspondence:
[*]
Corresponding author. Li Jie, College of Intelligence Science and Technology, National University of Defense Technology, No. 109, Deya Road, Kaifu District, Changsha City, HunanProvince, China. Tel.:∖Fax: +86 181 7596 8886; E-mail: leonlee2009@163.com.
Note: [1] This work was supported by the Science and Technology Innovation 2030-Key Project of “New Generation Artificial Intelligence” under Grant 2020AAA0108200.
Abstract: Through innovatively introducing the receding horizon into probabilistic model checking, an online strategy synthesis method for multi-robot systems from local automatons is proposed to complete complex tasks that are assigned to each robot. Firstly, each robot is modeled as a Markov decision process which models both probabilistic and nondeterministic behavior. Secondly, the task specification of each robot is expressed as a linear temporal logic formula. For some tasks that robots cannot complete by themselves, the collaboration requirements take the form of atomic proposition into the LTL specifications. And the LTL specifications are transformed to deterministic rabin automatons over which a task progression metric is defined to determine the local goal states in the finite-horizon product systems. Thirdly, two horizons are set to determine the running steps in automatons and MDPs. By dynamically building local finite-horizon product systems, the collaboration strategies are synthesized iteratively for each robot to satisfy the task specifications with maximum probability. Finally, through simulation experiments in an indoor environment, the results show that the method can synthesize correct strategies online for multi-robot systems which has no restriction on the LTL operators and reduce the computational burden brought by the automaton-based approach.
Keywords: Receding horizon, linear temporal
logic, Markov decision process, probabilistic model
checking, multi-robot collaboration
