Symbolic planning

In many cases, robots will need to move in an environment in order to execute a task. How well they perform this task, however, can strongly depend on the route that they take. For example, a driverless car could take a route with the least amount of traffic in order to minimise travelling time. Or, it could choose a route with the shortest travelling distance to minimise fuel consumption. Symbolic planning investigates how robots can choose the best route based on the task and the constraint on accomplishing that task (such as least travelling time or shortest travelling distance).

Formal verification has been applied to this area, and can provide a better solution than other methods. Formal verification is a set of techniques that can automatically check the correctness of a system against its specification in a systematic way. Usually, the system is encoded as a (symbolic) mathematical model and the specification is encoded as a set of logic formulae. Specifications restricting the system’s temporal behaviour, such as “the car cannot take any motorway in the route”, can be formulated as temporal logic formulae. A verification algorithm then checks whether every behaviour of the system satisfies the logic formulae.

In order to apply formal verification to symbolic planning, we first construct a symbolic model of the environment and the robots’ behaviour and formulate the task as logic formulae. Second, we feed the model and the formulae to a verification tool, which is sometimes called Model Checker, to compute a plan for the robots to finish the task. Constraints, such as least travelling time and shortest travelling distance, can be added to the model or the formulae, depending on the modelling formalism and the planning problem.

Many applications of formal verification in planning have been developed to tackle various planning problems. The main challenge in this area is building a model that has enough accuracy and detail to ensure the verification results are useful in practice, whilst is compact enough to be processed in a timely manner by model checkers. A large complex model can either take a model checker a very long time to finish the verification process or fail to generate meaningful results. Due to diverse environmental conditions and robot behaviours, there is no universal solution to generate a proper model for symbolic planning.

Let’s look an example. A team of robots are instructed to clean each room in a building. Depending on the size of the rooms, different numbers of robots are needed to clean each room. During the cleaning process, the robots must respect two constraints; while cleaning a room, all adjacent doorways have to be blocked by robots (the number of robots blocking a doorway will depend on the size of the doorway) and the doorway separating a cleaned room and an uncleaned room has to be blocked until both rooms are cleaned.

We want to compute a cleaning plan that uses the minimum number of robots and shortest total travel distance. The complexity of this planning problem makes it challenging to directly compute a good plan efficiently. Our approach is to solve the problem in two steps: a high-level plan for the whole robot team is constructed first via formal verification and secondly a detailed plan for each individual robot is computed by Linear Programming.

The image below illustrates the layout of the building, where five rooms are separated by walls and connected by doorways.

This layout can be represented by a graph, where each room is a node and a doorway is an edge connecting two rooms. The number of robots needed to clean a room or block a doorway is labelled in the graph next to the node or the edge. For example, the biggest room v2 needs four robots to clean, and doorway e4 needs three robots, while e2 only needs one.

Finding a cleaning strategy using the minimum number of robots can be formulated as a formal verification problem and tackled by the verification tool MCMAS (Model Checker for Multi-Agent Systems). The whole cleaning process is encoded as a formal model and the cleaning requirement is encoded as a temporal logic formula.

The image below illustrates a cleaning strategy returned by MCMAS with red areas being un-cleaned and green areas being cleaned. The robots clean room v5 first, then v4, v1, v2, and finally v3. The number of robots required for cleaning each room is shown in the figure.

The strategy computed by MCMAS only shows how the robots clean the whole area as a team. It does not tell us how each robot moves from one position to the next in the cleaning process. Fortunately, this can be solved by Linear Programming (LP). We can construct a linear program, which models all possible movement of the robots in the cleaning process. The cleaning strategy is then encoded as a set of constraints in the linear program over the robots’ movement. A LP solver will compute an execution of the strategy, which includes the position of each robot at each cleaning step.

The image below illustrates such an execution for the strategy in Figure 2 with each robot labelled an index.