Linear-Temporal-Logic Planning for Robots | Sudharsan Senthil

on

 We all likely have some idea of how a robot plans and executes a simple mission by following specific heuristics. When dealing with just one robot, the problem usually boils down to minimizing a cost function, which might depend on factors such as mission characteristics (like time constraints) or the robot's limitations (like power constraints). The challenges of task and path planning for a single robot have been well-researched. Task planning—deciding the order in which a robot performs its actions—can often be done relatively easily by using loosely defined criteria or by optimizing some cost. Recently, there have been advances in using large language models (LLMs) to assist with task planning [1].

 RRT* (Rapidly-exploring Random Tree Star)[2], introduced by Karaman, has significantly influenced modern path planning algorithms. The basic idea behind RRT* is to randomly sample points in the workspace and build a tree, with nodes that extend optimally. The root of this tree represents the robot's starting point, and once a leaf node appears near the goal, sampling stops. The parent nodes of this leaf are then traced back, forming a set of waypoints to guide the robot's path.

 Have you ever wondered how a team of robots plans, both temporally and logically, to complete a high-level mission? And what happens when some robots lose their required skills halfway through the task? While these questions may sound like solvable logistical problems, the complexity increases as the team size grows. In the rest of this blog, we’ll explore approaches to address these challenges, primarily using tools from model-checking.

 Before we go any further, there are a few key terms and definitions to familiarize yourself with:

  • High-level mission: A task that requires completing a set of temporal and logical objectives.
  • LTL(Linear Temporal Logic) formulation: This is used to represent the high-level mission in a clear and unambiguous way. For example, consider a mission: Bot-1 must surveil room A, Bot-2 must eventually arrange items in room B, and neither bot should step into room C. The LTL formula for this mission would be: <>e1 && <>e2 && [] ~e3. Here, e1, e2, and e3 are atomic propositions, where e1 denotes Bot-1 surveilling room A, e2 denotes Bot-2 arranging items in room B, and e3 denotes either bot entering room C. “[]” represents "always," “<>” stands for "eventually", "&&"means "and", and "~" stands for "negation". More formal definitions, including the usage of atomic propositions, can be found in [3].
  • Büchi Automaton: An LTL formula can be converted into a Nondeterministic Büchi Automaton (NBA). You can think of an NBA as a graph where moving from one node (or state) to another represents partial progress in fulfilling the mission. Starting from an initial node and progressing towards the final node captures the sequence of actions or logical steps required to complete the high-level mission described by the LTL formula. [4] website has the tool to convert LTL to NBA, following is the NBA for the example LTL formula.

In the graph above, state '3' is the accepted state, and as shown, there are multiple routes to reach this final state. The short formulas along the edges of the graph are called Boolean formulas, which must be satisfied to move from one node to the next. A more detailed study on using LTL formulations for mission planning can be found in the thesis [5].

 LTL Sampling: 

 Now that we have some background, let’s dive into understanding the sampling-based planner. Beware! The graph above might give the impression that finding a mission plan from the NBA is straightforward, but it’s not. The size (number of edges and nodes) of the NBA scales with the complexity of the mission—i.e., the number of logics, agents, and tasks involved. As a result, brute force methods are often impractical, so we employ sampling-based techniques, similar to the RRT* method we discussed earlier. 

 In TLRRT* [7], we sample nodes and connect them to the incomplete automaton based on specific criteria. We continue sampling and building the graph until we find an accepting node that satisfies the high-level mission. Once such a node is connected, we trace back to the root node. This sequence of nodes, starting from the initial node to the accepting node, determines the order in which robots should execute the tasks. It’s important to note that we are not building the entire NBA, so the optimality of the solution depends on the number of samples. This is a clever extension of RRT* for mission planning.

Now, it’s time to start answering the questions posed earlier. You may have already grasped the key idea: to accomplish a high-level mission with a team of robots, we first need to assign tasks to individual robots and determine the order in which they should be carried out. Task assignments should minimize the sum of costs associated with each robot performing a task using a specific skill, which may also be time-sensitive. [6]

As mentioned earlier, atomic propositions capture which tasks are assigned to which robot, and the LTL formula captures the order in which the tasks should be executed. The rest is straightforward—we use the sampling-based planner to generate the mission plan. 

Now that we’ve covered how to plan a mission, let’s explore how to reassign tasks when some robots lose their skills during the mission. In terms of Büchi Automaton, this corresponds to the robot team being in a non-accepting NBA state. 

Formally speaking, when skills fail, the Boolean formula that leads to the next closest state to the accepting state cannot be satisfied. As a result, we must repair every Boolean formula that comes up as we progress through the NBA (in this case, the incomplete NBA constructed using TLRRT*). 

In simpler terms, as we repair the Boolean formula corresponding to an edge, we can treat each edge independently. Repairing a Boolean edge involves reassigning tasks to capable robots, thereby modifying the atomic proposition itself. In [8], the reassignment problem is elegantly framed as a Breadth-First Search (BFS) over the reassignment graph. In this graph, nodes represent robots, and a directional edge connects robot-i to robot-j if and only if robot-j can replace robot-i for a given task. BFS is suitable here because we want to minimize the number of reassignments, and the search terminates when we find a robot that is not busy, hence no more reassignments needed.

We apply this same process to all failed edges. Ultimately, with the repaired part of the NBA, we choose the plan that requires the fewest hops to reach the accepting state from the current state. 

I hope this blog has helped clarify the key ideas behind applying model checking tools in robotics. If you have any questions or need further clarification on the topics discussed, please feel free to contact me. 

Acknowledgement: I would like to thank Prof. Yiannis Kantaros, and Samarth Kalluraya for helping me with the content for this blog.



Comments

Post a Comment