Synthesis method of strategy for multi-robot systems from local automatons under probabilistic model checking

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

1 Introduction

In recent years, more and more attention has been paid to the research of strategy synthesis for robots to complete the complex tasks (such as coverage, search, rescue, etc.). Model checking [1], as a formal mathematical tool and technique that successfully applied in a variety of engineering fields, provides a brand-new solution for the problem of robot strategy synthesis [2]. The strategy synthesis method that takes linear temporal logic as the task description language is one of the main research in this direction, because the linear temporal logic has ability to formalize the complex task requirements of robots in a rich time-related language and its close relevance to natural language. There have been many advances in using model checking to synthesize strategies for robots to satisfy task specifications. Ding et al. [3] proposed a method to synthesize strategy for a robot to complete a task with maximum probability, which not only considered the uncertainty of the robot motion, but also the uncertainty of the robot’s observation of properties in the environment. Guo et al. [4] proposed a novel framework combining motion planning based on model checking with action planning using action description languages. And an optimal controller was designed to generate discrete motion to satisfy LTL specifications. Ulusoy et al. [5] proposed an efficient computational incremental algorithm to automatically synthesize the optimal strategy for a robot interacting with a set of independent uncontrollable agents in a graph-like environment. The control goal is to maximize the probability that the robot satisfies the syntactically co-safe LTL specifications. Lacerda et al. [6] proposed a method to synthesize the cost-optimal strategy for a stochastic system to satisfy the co-safe LTL specifications. In order to address scenarios in which the task specification may not be satisfied with probability 1, the multi-objective probabilistic model checking is used to synthesize strategy with formal guarantee, that is, when the task becomes no longer fully satisfied during the execution, the strategy can still satisfy the task specification as much as possible.

At present, the research of strategies synthesis for robots from temporal logic is gradually expanding from single-robot to multi-robot systems. In this paper, the focus is on the latter one. The first step of collaboration strategy synthesis for multi-robot systems under model checking is to accurately describe the tasks by temporal logic language such as signal temporal logic etc. Then realizing the mapping of system control from continuous domain to discrete domain [7 –9]. At last the task specifications of the multi-robot systems are analyzed and the strategies whose correctness can be verified are synthesized. In recent work, strategy synthesis for multi-robot systems from temporal logic specifications has been explored and developed. Ulusoy et al. [10] presented a method to generate the optimal paths for robot team to satisfy LTL specifications, which depended on describing the movement of the robot as a timed automata to satisfy task specifications while minimizing transfer time between optimization proposition. But this method has not considered the collaboration among robots. Yushan et al. [11] proposed a top-down LTL planning method for multi-robot systems. The multi-robot systems are given a global task specification and attempt to decompose the LTL specification into local specifications that each robot could deal with independently. However, this method also has not considered the collaboration among robots. Guo et al. [12] proposed a bottom-up partially distributed planning method, which divided individual robots with task dependency into a group and only considered the groups rather than the whole team during strategy synthesis. As a result of it, the calculation burden was reduced. Although model checking has been successfully applied, the problem of state explosion and computational complexity limit its further development, especially in the multi-robot systems with large state space and complex task specifications. Therefore, some receding horizon strategy synthesis methods under model checking appeared [13 –16].

The receding horizon method optimizes an objective function of the current state over a finite horizon at each time instant, but only applies the first element of the optimal finite sequence of controls. The whole process is repeated for the new evaluated state at the next time instant. At present, the research of receding horizon strategy synthesis under model checking mainly focuses on single-robot. Ding et al. [13] proposed a receding horizon method to generate trajectories for a single agent, maximizing the collected time-varying rewards related to the state while ensuring that the task specifications are met. An energy equation similar to the Lyapunov equation was defined to ensure that the trajectory satisfied the acceptance conditions of the automaton and optimized a predetermined finite trajectory. Ulusoy et al. [14] proposed a receding horizon strategy synthesis method for single agent to ensure that the LTL specifications including static tasks with known locations and dynamic tasks sensed locally were satisfied. But the complexity of this method scales with the size of the local sensing range and the number of static tasks, so the state space can be potentially very large, and some low-priority dynamic tasks may be not serviced if it gets out of the sensing range when the agent moves towards a higher-priority dynamic task. Mingyu et al. [15] proposed a receding horizon strategy synthesis method from the LTL specification for a single agent according to the priority of tasks. The task specification consists of soft constraints and hard constraints, in which the hard constraints need to be satisfied and the soft constraints can be partially satisfied, while maximizing the collected rewards. Until now, there are only a few studies on receding horizon strategy synthesis for multi-robot systems under model checking [16]. In [16], Tumova et al. proposed a method to synthesize strategies for multi-agent system that each agent satisfies local task specifications, which considering the collaboration among agents. Through dynamic building of the local interaction automatons and the local product systems, the problem of state explosion brought by model checking is greatly reduced and the calculation efficiency is improved. As can be seen from above, the receding horizon strategy synthesis for multi-robot systems under model checking needs further research.

According to our knowledge, in the current research field of receding horizon strategy synthesis for robots under the model checking, either for single-robot [13 –15] or multi-robot systems [6] are aimed at the deterministic system model. Up to now, there has been no relevant research under the probabilistic model checking framework for the probabilistic system model. The main contribution of this paper is the first one to introduce the receding horizon into strategy synthesis under probabilistic model checking such that dynamically modeling the multi-robot systems and iteratively synthesizing collaboration strategies that satisfy the task specifications with maximum probability. Firstly, considering that in a multi-robot system, each robot is modeled as a global MDP, different from the deterministic transition system (TS) model used in [13 –16], which is a widely used formalism for modeling systems that exhibit both probabilistic and nondeterministic behaviour. Probability is a valuable tool for the modeling and analysis of multi-robot systems which contain uncertain factors, for example there is delay in sending messages among robots or deviation in executing the strategy due to dynamic changes in the environment and failures of robots. Secondly, each robot is assigned a LTL specification. For some tasks that a robot cannot complete by itself, the collaboration of other robots takes the form of atomic proposition into the robots’ LTL specifications. And the LTL specification of each robot is transformed into a deterministic rabin automaton (DRA). Compared with the buchi automaton used in [13 –16], the rabin automaton has stronger power of representation [17]. Unlike [16], where the task progression metric is defined on the local product automaton, a task progression metric is defined over rabin automatons transformed by the LTL specifications of each robot. Thus, the task progression rewards for each state of each rabin automaton are obtained to determine the corresponding local goal states in the finite-horizon product systems. As the experimental results show, the proposed method can correctly determine the local goal states in the finite-horizon product systems and loose the assumptions in [16] that the product automaton must contain at least an accepting state within the horizons. Also, the proposed method has no restrictions on the LTL operators. Thirdly, by setting two horizons to determine the steps of running in automatons and MDPs, the local finite-horizon product systems are dynamically built at each iteration according to the task dependency among robots, and the strategies of multi-robot system within the horizon are synthesized online based on the value iteration algorithm. And then, the strategies are synthesized iteratively until the global task specifications of the multi-robot system are satisfied. Finally, to verify the correctness of the proposed method, experiments are made in an indoor environment to synthesize collaboration strategies for a multi-robot system. The results show that the proposed method can be used for the online strategies synthesis for multi-robot systems of which the state space is large with the maximum probability to satisfy the task specifications, while it is difficult for global computation.

The rest of this paper is structured as follows. In Section 2, the preliminaries are introduced. Section 3 introduces the formulation of the problem and framework. In Section 4 the details of the strategy synthesis method are provided. In Section 5 the experimental results are presented, and a conclusion is made in Section 6.

2 Preliminaries

Given a set X, 2^X is defined as the set of all subsets of X. A finite or infinite sequence of elements of X is called a finite or infinite word over X, respectively. $ℕ$ and $ℝ_{0}^{+}$ represent natural numbers and non-negative real numbers, respectively.

2.1 Markov decision process

Each robot is modeled as a Markov decision process of which states are labeled with atomic proposition.

Definition 1 (Markov decision process): A Markov decision process (MDP) is a tuple $M = 〈 S, s_{0}, A, δ_{M}, A P, L a b 〉$ , where: S is a finite set of states; s₀ ∈ S is the initial state; A is a finite set of actions; $δ_{M} : S \times A \times S \to [0, 1]$ is a probabilistic transition function, where $\sum_{s^{'} \in S} δ_{M} (s, a, s^{'}) \in {0, 1}$ for all s ∈ S, a ∈ A; AP is a set of atomic propositions; Lab : S → 2^AP is a labelling function, such that p ∈ Lab (s) iff p is true in s ∈ S.

The set of enabled actions in s ∈ S is defined as $A_{s} = {a \in A ∣ δ_{M} (s, a, s^{'}) > 0$ for some s′∈ S }. A state-action mapping function μ : S → A is defined. And a policy is an infinite sequence of state-action mapping functions π ={ μ₀, μ₁, … }. An infinite sequence $σ = s_{0} \overset{a_{0}}{\to} s_{1} \overset{a_{1}}{\to} \dots$ on $M$ generated under a policy π ={ μ₀, μ₁, … } is a path if $δ_{M} (s_{i}, a_{i}, s_{i + 1}) > 0$ for all $i \in ℕ$ . A finite path $ρ = s_{0} \overset{a_{0}}{\to} s_{1} \overset{a_{1}}{\to} \dots \overset{s_{n - 1}}{\to} s_{n}$ is a prefix of an infinite path. The sets of all finite and infinite paths of $M$ starting from state s are denoted as ${FPath}_{M, s}$ and ${IPath}_{M, s}$ . A detailed introduction of MDP can be found in [17].

2.2 Linear temporal logic

Linear temporal logic (LTL) is an extension of propositional logic [17], first proposed by Pnueli in the late 1970s. LTL is a logical language used to describe the linear temporal relation of propositional changes. It provides a convenient and powerful method to formalize various qualitative attributes. As a task description language, temporal logic can describe complex tasks accurately. In this paper, the task specifications are expressed as LTL formulas. Same as ordinary predicate logic, the basic unit of linear temporal logic is the atomic proposition, which is the assertion of the state variables in the process being described. The LTL formula φ based on the set of atomic propositions AP is defined by the following syntax: $φ : : = true | p | \neg p | φ \land φ | X φ ∣ φ U φ$ where p ∈ AP. The operator X is read “next”, meaning that the formula after it will be true in the next state. The operator U is read “until”, meaning that its second argument will eventually become true in some state, and that the first argument will remain true until this point. Other operators include □, read “always”, to mean that the formula after it is always true, and ◊, read “eventually”, to mean that the formula is always true after a certain point. The Boolean operators include ¬ (negation), ∨ (disjunction) and ∧ (conjunction).

Given an infinite path σ of an MDP $M$ , the path σ satisfies the LTL formula φ is denoted as σ ⊨ φ. Detailed information about LTL semantics and syntax can be found in [17].

2.3 Deterministic rabin automaton

For any LTL formula φ over AP, a deterministic rabin automaton (DRA) can be built [17].

Definition 2 (Deterministic Rabin Automaton): A deterministic rabin automaton is a tuple $R = 〈 Q, q_{0}, δ, Σ, F 〉$ , where Q is a finite set of states; q₀ ∈ Q is the initial state; δ : Q × Σ → Q is a transition function; Σ is an input set (alphabet); F = {(L₁, K₁) , …, (L_M, K_M)} is a set of state pairs, where M is a positive integer and L_i, K_i ⊆ Q for all i ∈ {1, …, M}.

A run of a DRA $R$ is an infinite sequence of states in $R$ , denoted by $r_{R} = q_{0} q_{1} \dots$ , such that for each i ≥ 0, q_i+1 ∈ δ (q_i, α) for some α ∈ Σ. A run $r_{R}$ is accepted if there are some state pairs (L, K) ∈ F such that 1) there is n ≥ 0, q_m ∉ L for all m ≥ n; 2) there are infinite indexes k such that q_k ∈ K. This acceptance condition means that a run $r_{R}$ is accepting if a state pair (L, K) ∈ F and $r_{R}$ intersects with L only finitely many times and K infinitely many times. Note that for a given state pair (L, K), L may be null, but K will not be.

For any LTL formula φ over AP, a DRA with input alphabet Σ = 2^AP can be built and only accepts words over φ that satisfy φ [18, 19].

3 Problem formulation and framework

3.1 Problem description

A system containing robots $B$ in a collaborative environment is considered. Each robot $i \in B$ ,where robots $B = {1, \dots, N}$ has the ability to perform actions and communicate with each other, thus can synchronize with each other. Each robot will go to complete the task after obtaining its own LTL task specification. In the process of task completion, a robot may not be able to complete the task by itself, and the collaboration of other robots is included in their own LTL specification in the form of atomic proposition. The goal is to synthesize a strategy for each robot that satisfies the LTL specification with maximum probability. Each robot is modeled as an MDP, and the transitions between states correspond to the ability of the robot to perform actions.

When completing the tasks that need collaboration of multiple robots, synchronization among robots is required. For example, a robot will send a message to the other robots that responsible for the collaboration to remind them that it has reached the synchronization point as soon as it arrives the location of the task. Then, it must wait to receive a message from each of the collaborating robots before performing any action, that is, until all robots reach the synchronization point. In this paper, robots synchronize by sending messages to each other, but introducing the details of the synchronization mechanism is beyond the scope of this paper. Each robot is required to send synchronization messages only when it performs a task that needs collaboration, and there is no idle time in the system model.

Example 1: As shown in Fig. 1, there is a multi-robot system in a grid workspace, including three robots robot1, robot2 and robot3. The task of robot1 is to load the goods (lG) and move them to the elevator (elevator). However, due to the large volume of the goods, robot2 is needed to help load the goods (hG). Whether robot1 or robot2 arrives at the state of goods first, they need to wait for each other to synchronize until both robots reach the state of goods, and then execute the next action simultaneously. During transportation, the door (door) needs to be opened by robot1 before going to the elevator (elevator). The task of robot2 is to get water from the tearoom (tearoom) and deliver it to desk one (desk1) and then to desk two (desk2). The task of robot3 is to collect the garbage in garbage can one (can1) and garbage can two (can2) and transport it to the garbage station (dump). The security constraint on the robot is that robot1 cannot open the door (door) until it has finished loading the goods (lG).

Fig. 1

The example of workspace.

3.2 Framework

The overall framework of online receding horizon strategy synthesis for multi-robot system is shown in Fig. 2. The collaboration requirements between robots $i \in B$ have been included in the LTL specification of each robot. According to the task collaboration relationship among robots i, they are divided into groups $D_{n}$ , for $n \in ℕ$ . Each robot i is modeled as an MDP $M_{i}$ , and the LTL specification φ_i of each robot i is transformed into a DRA $R_{i}$ . The product automaton $A_{n}^{h}$ is built for the DRA $R_{i, n}$ of robots that are in the same group $i \in D_{n}$ within the horizon h, then the product system $M_{p, n}^{H}$ is built for the product automaton $A_{n}^{h}$ and the MDP $M_{i}$ of the robot $i \in D_{n}$ within the horizon H. In the product system $M_{p, n}^{H}$ , the local goal states are determined according to the task progression rewards of the states and the strategy from the current state to the goal states is synthesized by value iteration algorithm. The finite-horizon product automaton $A_{n}^{h}$ and the finite-horizon product system $M_{p, n}^{H}$ are dynamically built at each iteration. Then the strategies are synthesized iteratively in the finite-horizon product systems until the global task specifications are satisfied.

Fig. 2

The overall framework.

4 Cooperative strategy synthesis of LTL task specifications for multiple robots

In this paper, a receding horizon method with two horizons $h, H \in ℕ$ is used for each robot to online synthesize strategy, where the horizon h is used to set the steps of running in each DRA and the horizon H is used to set the steps of running in each MDP.

4.1 Task progression metric

In order to reduce the huge computational burden brought by model checking, an online iterative strategy synthesis method based on local automatons is proposed in this paper. To indicate a progress towards the satisfaction of the task specifications and be subsequently used to determine the goal states within the horizon, different from [16] defining a task progression metric over the product automaton, refer to [6], a task progression metric is defined over the DRA $R_{i}$ transformed by the LTL specification φ_i of each robot $i \in B$ . This metric is related to the distance between states in the DRA. Firstly calculate the distance from each state in DRA $R_{i}$ to a state in K_i ∈ F_i, and map each state to a value based on the distance $Dis : Q_{i} \to ℝ_{0}^{+}$ . Suc_{q
_i} ⊆ Q_i is denoted as the set of successors of state q_i and denoting $q_{i} \to q_{i}^{'}$ if there is a sequence of transitions in DRA $R_{i}$ that leads it from state q_i to state $q_{i}^{'}$ . The distance metric is defined as follows:

$\begin{matrix} Dis (q_{i}) = {\begin{matrix} 0 & if q_{i} \in K_{i} \\ Dis (q_{i}^{'}) + 1 & if q_{i} \notin K_{i}, q_{i}^{'} \in {Suc}_{q_{i}}, \\ \exists q_{i}^{F} \in K_{i} s . t . q_{i} \to q_{i}^{F} \\ + \infty & otherwise \end{matrix} \end{matrix}$ (1)

If a state in K_i can be reached from state q_i, then Dis (q_i) ≤ |Q_i|-1, where |Q_i| represents the number of states in DRA $R_{i}$ . And if a state in K_i cannot be reached from state q_i, Dis (q_i) is set as a huge value. The values Dis (q_i) can be calculated recursively by the following fixed-point calculation: $\begin{matrix} {Dis}^{0} (q_{i}) = {\begin{matrix} 0 & if q_{i} \in K_{i} \\ + \infty & if q_{i} \notin K_{i} \end{matrix} \end{matrix}$ (2)

$\begin{matrix} {Dis}^{k + 1} (q_{i}) = min {{Dis}^{k} (q_{i}), min_{q_{i}^{'} \in {Suc}_{q_{i}}} {{Dis}^{k} (q_{i}^{'}) + 1}} \end{matrix}$ (3) And then based on the distance metric, each state of DRA $R_{i}$ is mapped with a reward $R : Q_{i} \to ℝ_{0}^{+}$ representing the progress towards the satisfaction of the task specification after reaching that state: $\begin{matrix} R (q_{i}) = {\begin{matrix} | Q_{i} | & if q_{i} \in K_{i} \\ \frac{1}{Dis (q_{i})} & if q_{i} \notin K_{i} \end{matrix} \end{matrix}$ (4) The reward mapping function indicates that if a state q_i of DRA $R_{i}$ can reach the state in K_i and the closer the distance to the state, the greater the reward will be obtained. If a state q_i cannot reach a state in K_i, the reward for q_i is 0. The larger the reward of state is, the closer it is to satisfying the task specification. Finally if there are many state pairs (L_i, K_i) in F_i, the task progression rewards are calculated for each of the state pairs (L_i, K_i), and then the multiple task progression rewards are averaged for each state in $R_{i}$ as the final task progression reward.

4.2 Receding horizon model building

The method of [16] to build local product automaton and local product system is referenced in this paper.

4.2.1 Product automaton

For robots i with task collaboration relationships, they are divided into the same group $D_{n}, n \in N$ . For all robots $i \in D_{n}$ , a product automaton within the horizon h is built to represent the interaction between DRAs $R_{i, n}$ . Since the horizon limits the number of running steps in the product automaton so that it is expressed based on finite words, the product automaton obtained is not a DRA and can be viewed as a directed graph.

Suppose that $D_{n}$ contains k robots, the product automaton of DRAs $R_{1, n}, \dots, R_{k, n}$ within the horizon h is $A_{n}^{h} = 〈 Q_{A}, q_{0, A}, δ_{A}, Σ_{A}, F_{A} 〉$ , where $Q_{A} \subset Q_{1} \times \dots \times Q_{k}$ is a finite set of states; $q_{0, A} = (q_{0, 1}, \dots, q_{0, k})$ is the initial state; $Q_{A}^{0} = q_{0, A}$ ; $Σ_{A} = {⋃_{i \in D_{n}} ω_{z} ∣ ω_{z} \in 2^{{AP}_{i}}}$ . For all 1 ≤ j ≤ h, $(q_{1}^{'}, \dots, q_{k}^{'}) \in Q_{A}^{j}$ and $((q_{1}, \dots, q_{k}), ω_{A},$ $(q_{1}^{'}, \dots, q_{k}^{'})) \in δ_{A}^{j}$ are defined iff (1) $(q_{1}, \dots, q_{k}) \in Q_{A}^{j - 1}$ ; (2) for all $i \in D_{n}$ , either $(q_{i}, ω_{i}, q_{i}^{'}) \in δ_{i}, ω_{i} \in {AP}_{i}$ or $q_{i} = q_{i}^{'}$ , where $ω_{A} = ⋃_{i \in D_{n}} ω_{i}$ . Then $Q_{A} = ⋃_{0 \leq j \leq h} Q_{A}^{j}$ and $δ_{A} = ⋃_{1 \leq j \leq h} δ_{A}^{j}$ . $F_{A}$ is a set of state pairs and it is no longer needed for the further computations because the local goal states can be determined by the task progression rewards. There is a one-to-one correspondence between the transition path in the product automaton $A_{n}^{h}$ and the transition path in the DRAs $R_{1, n}, \dots, R_{k, n}$ [13]. A transition path from initial state (q_0,1, …, q_0,k) of the product automaton $A_{n}^{h}$ to a state (q₁, …, q_k) corresponds to a path in each DRA $R_{1, n}, \dots, R_{k, n}$ from their respective initial state q_0,i to a state q_i, for $i \in D_{n}$ .

In the product automaton $A_{n}^{h}$ , the task progression rewards of the states $q_{A}$ are inherited from the DRAs $R_{i, n}, i \in D_{n}$ . If $q_{A} = (q_{1}, \dots, q_{k})$ , $R_{A} (q_{A}) = \sum_{i \in D_{n}} R (q_{i})$ . Since there is a one-to-one correspondence between the paths of the product automaton $A_{n}^{h}$ and the DRAs $R_{i, n}, i \in D_{n}$ , the greater the reward $R_{A} (q_{A})$ of the state $q_{A}$ in the product automaton $A_{n}^{h}$ is, the closer the state $q_{i} \in Q_{A}$ of each DRA $R_{i, n}$ is to satisfying the individual task specification of the robot $i \in D_{n}$ .

4.2.2 Product system

Building the product automaton and task progression metric allow to evaluate which tasks should be completed to maximize the progress towards the satisfaction of the task specifications, and then planning the transitions of each robot $i \in D_{n}$ to reach the states of those tasks are needed. So building a product system $M_{p, n}^{H}$ is necessary to capture the allowable behavior of the robots within the horizon H (a finite mapping of state-action pairs). Each robot $i \in D_{n}$ is modeled as an MDP $M_{i} = 〈 S_{i}, s_{0,} i, A_{i}, L a b_{i} 〉$ . The product of the MDPs $M_{i}, i \in D_{n}$ with the product automaton $A_{n}^{h}$ within the horizon H is $M_{p, n}^{H} = 〈 S_{p}, s_{0, p}, A_{p}, δ_{M, p}, L a b_{p} 〉$ , where $S_{p} = S_{1} \times \dots \times S_{k} \times Q_{A}$ is a finite set of states; $s_{0, p} = (s_{0, 1}, \dots, s_{0, k}, q_{0, A})$ is the initial state; $S_{p}^{0} = s_{0, p}$ ; $A_{p} = A_{1} \times \dots \times A_{k} \times Σ_{A}$ is a finite set of actions; ${AP}_{p} = ⋃_{i \in D_{n}} {AP}_{i}$ is a set of atomic propositions; Lab_p : S_p → 2^{AP
_p} is a labelling function, such that p ∈ Lab_p (s_p) iff p is true in s_p ∈ S_p. For all 1 ≤ j ≤ H, $s_{p} = (s_{1}, \dots, s_{k}, q_{A})$ , $a_{p} = (a_{1}, \dots, a_{k}, ω_{A})$ , $s_{p}^{'} = (s_{1}^{'}, \dots, s_{k}^{'}, q_{A}^{'})$ , $s_{p}^{'} \in S_{p}^{j}$ and $(s_{p}, a_{p}, s_{p}^{'}) \in δ_{M, p}^{j}$ are defined iff (1) $s_{p} \in S_{p}^{j - 1}$ ; (2) for all $i \in D_{n}$ , $δ_{i} (s_{i}, a_{i}) = s_{i}^{'}$ and $ω_{A} \cap {AP}_{i} = {Lab}_{i} (s_{i})$ ; (3) $(q_{A}, ω_{A}, q_{A}^{'}) \in δ_{A}$ . Then $S_{p} = ⋃_{0 \leq j \leq H} S_{p}^{j}$ and $δ_{M, p} = ⋃_{1 \leq j \leq H} δ_{M, p}^{j}$ . The task progression rewards of the states in the product system $M_{p, n}^{H}$ are inherited from the product automaton $A_{n}^{h}$ , $R_{M} : S_{p} \to ℝ_{0}^{+}$ . $\begin{matrix} R_{M} (s_{p}) = {\begin{matrix} R_{A} (q_{A}) & if q_{A} \in s_{p} \\ 0 & otherwise \end{matrix} \end{matrix}$ (5)

A strategy π_p ={ μ_0,p, μ_1,p, … } in the product system $M_{p, n}^{H}$ is an infinite sequence of the state-action mapping function μ_p : s_p → a_p, where $s_{p} = (s_{1}, \dots s_{k}, q_{A})$ , $a_{p} = (a_{1}, \dots a_{k}, ω_{A})$ . For all $i \in D_{n}$ , the state-action mapping function μ_i : s_i → a_i and the strategy π_i ={ μ_0,i, μ_1,i, … } on each MDP $M_{i}$ can be obtained by one-to-one correspondence.

4.3 Receding horizon strategy synthesis

4.3.1 Strategy synthesis

The goal is to synthesize a strategy for each robot $i \in B$ that satisfies the individual LTL specification with maximum probability. Under a strategy π of the MDP $M$ , all nondeterminism is resolved and the actions of $M$ are fully probabilistic. Thus a probability metric $\Pr_{M, s}^{π}$ can be defined over a finite set of paths ${FPath}_{M, s}$ to determine the probability of some events occurring under the policy π. For an event $e : {FPath}_{M, s} \to {0, 1}$ , the probability of e occurring under the policy π is denoted as $\Pr_{M, s}^{π} (e)$ . Given a measurement function $f : {FPath}_{M, s} \to ℝ_{0}^{+}$ , the maximum probability of all strategies based on the probability metric can be calculated $\Pr_{M, s}^{π}$ : $\Pr_{M, s}^{max} (e) = sup_{π} \Pr_{M, s}^{π} (e)$ . Similarly, for the product MDP $M_{p}^{H}$ a probability metric $\Pr_{M_{p}, s_{p}}^{π_{p}}$ can be similarly defined over the finite set of paths ${FPath}_{M_{p}, s_{p}}$ to determine the probability of some events occurring under strategy π_p. The probability of e occurring under the policy π_p is denoted as $\Pr_{M_{p}, s_{p}}^{π_{p}} (e)$ . Measurement function $f_{p} : {FPath}_{M_{p}, s_{p}} \to ℝ_{0}^{+}$ is defined based on probability metric $\Pr_{M_{p}, s_{p}}^{π_{p}}$ , then the maximum probability among all strategies is: $\Pr_{M_{p}, s_{p}}^{max} (e) = sup_{π_{p}} \Pr_{M_{p}, s_{p}}^{π_{p}} (e)$ . The probabilistic reachability problem is the problem of calculating $\Pr_{M, s}^{max} ({reach}_{S^{'}})$ along the corresponding optimal policy. Given S′ ⊆ S, the event of reaching a state in S′ is defined as ${reach}_{S^{'}} : {FPath}_{M, s} \to {0, 1}$ , where for some j such that s_j ∈ S′, there exists ${reach}_{S^{'}} (s_{0} \overset{a_{0}}{\to} s_{1} \overset{a_{1}}{\to} \dots s_{j - 1} \overset{a_{j - 1}}{\to} s_{j}) = 1$ .

In this paper, the proposed method combines the probabilistic reachability theory with the value iteration algorithm. The probabilistic reachability theory is to calculate the maximum probability of satisfying the task specifications in the product system $M_{p}^{H}$ , which is equivalent to calculating the maximum probability of reaching a state in the set of accepting maximum end component (AMEC). More detailed information about the probabilistic reachability theory and AMEC can be found in [17]. As there may be no accepted states in the current horizon h, there may be no AMECs in the product system $M_{p}^{H}$ . Therefore, the set of goal states $S_{p}^{F}$ needs to be determined in the current product system within the horizon H, and calculating $\Pr_{M_{p}, s_{p}}^{max} (s_{p}^{'})$ for $s_{p}^{'} \in S_{p}^{F}$ . Then the strategy of the current finite-horizon product system $π^{*} = arg max_{π} \Pr_{M_{p}, s_{p}}^{max} (s_{p}^{'}), s_{p}^{'} \in S_{p}^{F}$ with the maximun probability to satisfy the task specification is obtained. The process of building local product systems and strategy synthesis are repeated until the global task specifications are satisfied.

Theorem 1. For all $i \in D_{n}$ , the state-action mapping function μ_i : s_i → a_i and the strategy π_i ={ μ_0,i, μ_1,i, … } on each MDP $M_{i}$ which are obtained by one-to-one correspondence from the $π_{p}^{*} = {μ_{0, p}, μ_{1, p}, \dots}$ and μ_p : s_p → a_p returned by Alg. 1 make the robots i satisfy their own task specifications with the maximum probability.

Proof. An one-to-one correspondence can be established between a strategy of the product system and a strategy of the MDPs. Given a state-action mapping function μ_p : s_p → a_p and a strategy π_p ={ μ_0,p, μ_1,p, … } of the product system, a state-action mapping function and a strategy of the MDP can be obtained by omitting those states and actions in μ_p : s_p → a_p that do not belong to the MDP. So the only thing that need to be verified is that the probability measures used on the paths in the MDPs and the paths in the product systems are equivalent. Due to the observation at each state is independent, the observation process is Markovian as it only depends on which state the observation is made, i.e. which states the robots get to. Note that the probability of moving from a state $s_{p} = (s_{1}, \dots s_{k}, q_{A})$ to $s_{p}^{'} = (s_{1}^{'}, \dots s_{k}^{'}, q_{A}^{'})$ in the product system under the strategy π_p ={ μ_0,p, μ_1,p, … } is exactly $δ_{M, p} (s_{p}, a_{p}, s_{p}^{'}) = Π_{i \in D_{n}} δ_{M, i} (s_{i}, a_{i}, s_{i}^{'})$ , where $s_{i} \in s_{p}, a_{i} \in a_{p}, s_{i}^{'} \in s_{p}^{'}$ . Since the strategy π_p and the μ_p can be uniquely mapped to a strategy π_i and a μ_i of each MDP $M_{i}$ . The probability of executing the strategy π_p in the product system is equivalent with the probability of satisfying the task specification through a finite path in $M_{i}$ under the strategy π_i corresponding to π_p. Thus, the maximum probability of executing the strategy $π_{p}^{*}$ returned by Alg. 1 is equivalent to that each robot i satisfies its own task specification with maximum probability.

4.3.2 Target states determination

The method of determining the set of goal states in the product system $M_{p}^{H}$ is as follows. Each state of $M_{p}^{H}$ has a task progression reward $R_{M} (s_{p})$ . The larger the task progression reward of a state is, the closer it is to the completion of the task specification. So the set of states in the current product system $M_{p}^{H}$ with the maximum task progression reward are calculated $S_{p}^{M} = ⋃_{s_{p} \in S_{p}} \underset{s_{p}}{argmax} R_{M} (s_{p})$ . However there may be some states in the current product system $M_{p}^{H}$ with the same maximum task progression reward, and because the product system is built based on local automatons, not all of these states can be viewed as goal states. In this paper, the Dijkstra algorithm [20] is used to choose the state in the $S_{p}^{M}$ which is closest to the current state of $M_{p}^{H}$ as $S_{p}^{F}$ . Then the strategy is synthesized from the initial state of $M_{p}^{H}$ to a state in the set $S_{p}^{F}$ with the maximum probability $π_{p}^{*} = arg max_{π_{p}} \Pr_{M_{p}, s_{0, p}}^{max} (s_{p}), s_{p} \in S_{p}^{F}$ . A example of goal states determination within the horizon is shown in Fig. 3.

Fig. 3

A example of goal states determination within the horizon. s_0,p is the initial state within the current horizon, and all states in the regions with the same color have the same task progression reward. The states in the red region have the smallest task progression reward, and the states in the yellow region have the largest task progression reward. So the goal states of the product system within the current horizon need to be determined in the yellow region. The Dijkstra algorithm is used to calculate the state nearest to the initial state as s_13,p, then the current goal state is s_13,p.

Theorem 2. For all $i \in D_{n}$ , the $π_{p}^{*} = {μ_{0, p}, μ_{1, p}, \dots}$ and μ_p : s_p → a_p returned by Alg. 1 yield compatible actions. With the task progression rewards, Alg. 1 terminates in a finite number of iterations and is guaranteed to return the strategy that satisfy the task specifications with maximum probability.

Proof. When each robot $i \in D_{n}$ is assigned a task specification, the needs for collaboration have been included in their own task specifications in the form of atomic propositions, which can ensure that there will be no conflict between each robot’s task specification. Therefore the strategy $π_{p}^{*} = {μ_{0, p}, μ_{1, p}, \dots}$ and μ_p : s_p → a_p returned by Alg. 1 will yield compatible actions of robots. Since the task progression reward of each state in the finite-horizon product systems are inherited from the DRAs, the larger the task progression reward of the state that the robots reach, the closer they are to satisfying the task specifications. And the last goal state in the finite-horizon product system will be the state with the maximally progression reward. With the goal states in the finite-horizon product systems, the local LTL specifications are always satisfied at line 17-19 of Alg. 1. The rest of the proof is similar to the proof of convergence for the value iteration algorithm (see [17], pp. 851-854).

Algorithm 1 Receding horizon strategy synthesis based on value iteration.

Input: a set of robots A = {1, …, N}, and their MDPs

M_{1}, \dots, M_{N}

; DRAs

R_{1}, \dots, R_{N}

transformed by the LTL specifications of the robots; the current state s_cur = (s_0,1, …, s_0,N, q_0,1, …, q_0,N); the horizons H and h;

Output: the optimal strategy from the initial state to the final goal state

π_{p}^{*} = {μ_{0, p}, μ_{1, p}, \dots}

,where μ_p : s_p → a_p is a state-action mapping function;

1: compute the task progression rewards

R_{j, i}, i \in {1, \dots, N}, j \in ℕ

for each state of the DRAs

R_{1}, \dots, R_{N}

;

2: divide the robots into teams according to the task collaboration requirements between them

G_{c} = {D_{1}, \dots, D_{n}}

;

3: for

i \in D_{k}, k \in {1, \dots, n}

4: compute the global maximun task progression

5: rewards of the teams R_max,k =

\sum_{i \in D_{k}} R (q_{i}), q_{i} \in K_{i}

;

7: for

D_{k}, k \in {1, \dots n}

8: create the list policy_k;

9: whileR_{s
_cur,k} ≠ R_max,kdo

10: build the product automaton

A_{k}^{h}

11:

R_{i}, i \in D_{k}

;

12: build the product system

M_{p, k}^{H}

13: the

A_{k}^{h}

with

M_{i}, i \in D_{k}

;

14: find a state in

M_{p, k}^{H}

with the maximun

15: task progression reward and the nearest

16: to the current state s_cur,k as s_goal;

17: compute

π_{k}^{*} =

18:

arg max_{π} \Pr_{M_{p, k}^{H}, s_{cur, k}}^{max} (s_{goal})

by the

19: value iteration algorithm (Algorithm

20: 2);

21:

{policy}_{k} . append (π_{k}^{*})

;

22: s_cur,k = s_goal;

23: end while

24: return policy_k;

25: send for

26: end for

27: the optimal strategy for robots in each group

D_{k}, k \in {1, \dots, n}

is policy_k.

Algorithm 2 value iteration algorithm

Input: the product system

M_{p, k}^{H}

, the current state s_cur,k = (s_0,1, …, s_0,N, q_0,1, …, q_0,N) and the goal state s_goal; a threshold θ = 0.00000001;

Output: the optimal strategy from the current state to the goal state

π_{k}^{*}

;

done = False;

2: While not done do

Δ ← 0;

4: for each

s_{p} \in S_{p}

v ← V (s_p);

6: V (s_p)←

max_{a_{p}} \sum_{s_{p}^{'}} δ_{M, p} (s_{p}, a_{p}, s_{p}^{'}) V (s_{p}^{'})

;

8: Δ ← max(Δ, |v - V (s_p) |);

end for

10: ifΔ < θthen

done=True;

12: end if

end while

14:

π_{k}^{*} = arg max_{π_{k}} \Pr_{M_{p, k}^{H}, s_{cur, k}}^{max} (s_{goal})

;

return

π_{k}^{*}

;

5 Experiments and analysis

5.1 Experiment settings

To verify the correctness of the method and show the high efficiency, the strategy synthesis for single robot and collaborative robots within different horizons are tested and analyzed. Before that, the local goal states of different LTL specifications within different horizons are tested and analyzed to verify the correctness of local goal states choosen by the proposed method. The proposed solution is implemented in Ubuntu18.04 based on Python2.7 using the working environment and settings as shown in the Example 1. The MDP of each robot has 34 states. By default, there are 5 actions e, s, w, n and g. The execution of each action has different probabilities to reach different states, but the robots can only move between two adjacent grids without blocking, and the execution of the action g can stay in the current grid. The ltl2dstar tool [21] is used to transform the LTL specification of each robot into a DRA. The LTL specification of the robot1 is φ₁ = ¬ door U lG ∧ (X F door ∧ (X F elevator)). The LTL specification of the robot2 is φ₂ = F hG ∧ (X F can1 ∧ (X F can2)). The LTL specification of the robot3 is φ₃ = F tearoom ∧ (X F desk1 ∧ (X F desk2)).

5.2 Testing and analysis of local goal states

To verify the correctness of local goal states choosen by the proposed method, the determinations of goal states for LTL specifications containing different types of LTL operators within different horizons are tested. For testing the different situations that the target state is within the horizon or not, the strategies are synthesized under different H and h. For robot2, firstly its LTL specification is set as φ = ¬ desk1 U hG. The strategies are synthesized under H = 5, h = 1 and H = 7, h = 1 respectively. The results of the local goal state choosen at the first iteration are shown in Figs. 5. Then its LTL specification is set as φ = G F can1 ∧ X can2. The strategies are synthesized under H = 3, h = 3 and H = 6, h = 3 respectively. The results of the local goal state choosen at the first iteration are shown in Figs. 7. Finally, its LTL specification is set as φ = G (desk2 ⟶ X ¬ desk2 U can2). The strategies are synthesized under H = 5, h = 2 and H = 9, h = 2 respectively. The results of the local goal state choosen at the first iteration are shown in Figs. 9. As can be seen from the results, the goal states within the horizons are correct for the LTL specifications containing different types of operators and for the conditions that the states of tasks exist or donot exist within the horizon, because the strategies make the robots moving towards satisfying their task specifications.

Fig. 4

H = 5, h = 1 .

Fig. 5

H = 7, h = 1 .

Fig. 6

H = 3, h = 3 .

Fig. 7

H = 6, h = 3 .

Fig. 8

H = 3, h = 3 .

Fig. 9

H = 6, h = 3 .

5.3 Testing and analysis of strategy synthesis

5.3.1 Computing task progression rewards of DRAs

According to the task collaboration relationships among the robots, the multi-robot system is divided into two groups of $D_{1} = {robot 1, robot 2}$ and $D_{2} = {robot 3}$ . The LTL specification of each robot is transformed into a DRA $R_{1}, R_{2}, R_{3}$ , and the number of states are 6, 4, 4 respectively. The task progression rewards computed of each states are shown in Fig. 10.

Fig. 10

Task progression rewards.

5.3.2 Synthesizing strategy

The strategy synthesis is tested for single robot and collaborative robots within different H and h. At the same time, the results are compared with global strategy synthesis, PRISM model checker [24] and the incremental synthesis method proposed in [25]. The strategy synthesized for each robot with the maximum probability of satisfying the task specification is shown in Fig. 11. As can be seen from the figures, the strategies synthesized are correct for they are making the robots moving towards satisfying their task specifications.

Fig. 11

Strategies synthesized for each robot.

5.3.3 Performance analysis

The performance of strategies synthesise under different horizons H and h are analyzed from three aspects of iteration number, computing time and size of state space respectively, and compared with some other methods. The results are shown in Table 1-4, and the strategy synthesized for each robot is shown in Fig. 11. As can be seen from the Table 1-2, for group $D_{1}$ , the time of constructing local product automaton, local product system and strategy synthesis is significantly less than that of the other methods, and the overall number of states in generated product automatons and product systems is significantly less than that of the other methods. Among them, the performance of H = 6, h = 1 is better than other horizons. As can be seen from the Table 3-4, for group $D_{2}$ , the time of constructing local product automaton, local product system and strategy synthesis have no great advantage compared with the other methods due to the small number of states. As shown in Fig. 11, the strategies synthesized by the proposed method make the robots move towards satisfying the task specifications. Experimental results show that the proposed method is correct and effective, which significantly alleviates the computational complexity brought by model checking and greatly improves the efficiency of strategy synthesis for models with huge state space.

Table 1
The time consumption of $D_{1}$

H h Product automaton(s) Product system(s) Policy synthesis(s)

6 1 0.00848293 25.22398184 1.68384122

6 2 0.03630995 84.08934712 2.64119195

8 1 0.01134991 65.13662291 4.22636198

8 2 0.15220567 108.85412001 3.79696393

the global computation 0.16788387 338.98028898 6.14488697

PRISM model checker 0.15960721 291.76329171 5.86153358

incremental synthesis 0.13621975 277.74904745 5.37225761

H	h	Product automaton(s)	Product system(s)	Policy synthesis(s)
6	1	0.00848293	25.22398184	1.68384122
6	2	0.03630995	84.08934712	2.64119195
8	1	0.01134991	65.13662291	4.22636198
8	2	0.15220567	108.85412001	3.79696393
the global computation	0.16788387	338.98028898	6.14488697
PRISM model checker	0.15960721	291.76329171	5.86153358
incremental synthesis	0.13621975	277.74904745	5.37225761

Table 2

The state space and iteration number of $D_{1}$

H	h	Product automaton	Product system	Iteration number
6	1	15	11067	3
6	2	17	14622	2
8	1	19	20640	3
8	2	17	18802	2
the global computation		21	24276	1
PRISM model checker		20	23093	1
incremental synthesis		19	22734	1

Table 3

The time consumption of $D_{2}$

H	h	Product automaton(s)	Product system(s)	Policy synthesis(s)
6	1	0.00081110	0.18561458	0.00701593
6	2	0.00216507	0.07428717	0.01204395
8	1	0.00078702	0.08855701	0.01499605
8	2	0.00111579	0.07062315	0.01602387
the global computation		0.00200391	0.02621388	0.01089811
PRISM model checker		0.00129631	0.02102376	0.00914733
incremental synthesis		0.00185617	0.02462909	0.01130869

Table 4

The state space and iteration number of $D_{2}$

H	h	Product automaton	Product system	Iteration number
6	1	6	158	3
6	2	5	147	2
8	1	6	204	3
8	2	5	170	2
the global computation		4	136	1
PRISM model checker		4	133	1
incremental synthesis		4	134	1

6 Conclusion

A receding horizon strategy synthesis method for collaborative multi-robot systems from local automatons is proposed. The receding horizon is first introduced into the strategy synthesis for multi-robot systems under probabilistic model checking. By setting two horizons, the running steps of automatons and Markov decision processes are limited. Based on the collaborative task relationship between robots, the local product systems within the horizons are dynamically built when the robots are running. In the product systems, the strategies that satisfy the task specifications with the maximum probability are synthesized online for each robot based on the value iteration algorithm, which greatly alleviates the computational complexity brought by the model checking.

Future research includes meeting various optimality requirements by replacing the value iteration algorithm with the linear programming algorithm or applying multi-objective probabilistic model checking techniques. Furthermore, in this paper we assume that the system models are fully known. In the case that they are not, we would like to address the formulation of the same problem. And the synchronization mechanism among robots and the theoretical guarantees need further research and verification.

References

Clarke

E.M.

, Model checking, Foundations of Software Technology and Theoretical Computer Science, Springer Berlin Heidelberg (1997), , 54–56.

Kress-Gazit

, Lahijanian

and Raman

, Synthesis for Robots:Guarantees and Feedback for Robot Behavior, Annu Rev ControlRobot Auton Syst 1 (2018), 211–236.

Ding

X.C.

, Smith

S.L.

, Belta

and Rus

, LTL Control in UncertainEnvironments with Probabilistic Satisfaction Guarantees, IFACProceedings Volumes 44 (2011), 3515–3520.

Guo

, Johansson

K.H.

and Dimarogonas

D.V.

, Motion and action planning under LTL specifications using navigation functions and action description language, IEEE/RSJ International Conference on Intelligent Robots and Systems (2013), 240–245.

Ulusoy

, Wongpiromsarn

and Belta

, Incremental controllersynthesis in probabilistic environments with temporal logicconstraints, The International Journal of Robotics Research 33 (2014), 1130–1144.

Lacerda

, Parker

and Hawes

, Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications, (2015).

Alur

, Henzinger

T.A.

, Lafferriere

and Pappas

G.J.

, Discreteabstractions of hybrid systems, Proceedings of the IEEE 88 (2000), 971–984.

Conner

D.C.

, Rizzi

A.A.

and Choset

, Composition of local potential functions for global robot control and navigation, Proceedings 2003 IEEE/RSJ International Conference on Intelligent Robots and Systems (2003), 3546–3551.

Belta

, Isler

and Pappas

G.J.

, Discrete abstractions for robotmotion planning and control in polygonal environments, IEEETransactions on Robotics 21 (2005), 864–874.

10.

Ulusoy

, Smith

S.L.

, Ding

X.C.

, Belta

and Rus

, Optimal Multi-Robot Path Planning with Temporal Logic Constraints, (2011).

11.

Chen

, Ding

X.C.

, Stefanescu

and Belta

, Formal Approach tothe Deployment of Distributed Robotic Teams, IEEE Transactionson Robotics 28 (2012), 158–171.

12.

Guo

and Dimarogonas

D.V.

, Reconfiguration in motion planning of single- and multi-agent systems under infeasible local LTL specifications, 52nd IEEE Conference on Decision and Control (2013), 2758–2763.

13.

Ding

, Lazar

and Belta

, LTL receding horizon control forfinite deterministic systems, Automatica 50 (2014), 399–408.

14.

Ulusoy

and Belta

, Receding horizon temporal logic control indynamic environments, The International Journal of RoboticsResearch 33 (2014), 1593–1607.

15.

Cai

, Peng

, Li

, Gao

and Kan

, Receding HorizonControl-Based Motion Planning With Partially Infeasible LTLConstraints, IEEE Control Syst Lett 5 (2021), 1279–1284.

16.

Tumova

and Dimarogonas

D.V.

, A Receding Horizon Approach to Multi-Agent Planning from Local LTL Specifications, (2014).

17.

Baier

and Katoen

J.P.

, Principles of Model Checking, (2008).

18.

Gradel

, Thomas

and Wilke

, Automata Logics and Infinite Games, Lecture Notes in Computer Science (2002), 265–274.

19.

Blahoudek

, Křetínský

and Strejček

, Comparison of LTL to Deterministic Rabin Automata Translators, (2013).

20.

Cormen

, Leiserson

, Rivest

and Stein

, Introduction To Algorithms, (2001).

21.

Klein

, ltl2dstar - LTL to deterministic Streett and Rabin automata, (2007).

22.

Vasile

C.I.

, Li

and Belta

, Reactive sampling-based pathplanning with temporal logic specifications, The InternationalJournal of Robotics Research 39 (2020), 1002–1028.

23.

Zhang

, Du

and Cowlagi

R.V.

, Randomized samplingbasedtrajectory optimization for UAVs to satisfy linear temporal logicspecifications, Aerospace Science and Technology 96(2020), 105591.

24.

Kwiatkowska

, Norman

and Parker

, PRISM 4.0: Verification of probabilistic real-time systems, CAV, (2011).

25.

Wongpiromsarn

, Ulusoy

, Belta

, Frazzoli

and RusIncremental

, Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications, IEEE International Conference on Robotics and Automation (2013), 5011–5018.