PaperlayerView exact revision on arXiv

Source-linked AI summary

Multi-agent Motion Planning from Signal Temporal Logic Specifications

Dawei Sun, Jingkai Chen, Sayan Mitra, Chuchu Fan

arXiv:2201.05247v1cs.ROcs.MAcs.SYeess.SY

TL;DR

Multi-agent planning from complex temporal specifications is difficult to scale, particularly with discrete abstractions and fixed-step MPC. This paper uses timed waypoints to encode robust STL constraints as a MILP, and reports better benchmark performance than abstraction-based and MPC-based methods.

Abstract

from arXiv · show

We tackle the challenging problem of multi-agent cooperative motion planning for complex tasks described using signal temporal logic (STL), where robots can have nonlinear and nonholonomic dynamics. Existing methods in multi-agent motion planning, especially those based on discrete abstractions and model predictive control (MPC), suffer from limited scalability with respect to the complexity of the task, the size of the workspace, and the planning horizon. We present a method based on {\em timed waypoints\/} to address this issue. We show that timed waypoints can help abstract nonlinear behaviors of the system as safety envelopes around the reference path defined by those waypoints. Then the search for waypoints satisfying the STL specifications can be inductively encoded as a mixed-integer linear program. The agents following the synthesized timed waypoints have their tasks automatically allocated, and are guaranteed to satisfy the STL specifications while avoiding collisions. We evaluate the algorithm on a wide variety of benchmarks. Results show that it supports multi-agent planning from complex specification over long planning horizons, and significantly outperforms state-of-the-art abstraction-based and MPC-based motion planning methods. The implementation is available at https://github.com/sundw2014/STLPlanning.

I. INTRODUCTION

The paper addresses the scalability challenges of planning cooperative multi-agent tasks from temporal specifications by synthesizing timed-waypoint paths and encoding their constraints for MILP solving. It also introduces MA-STL to express multi-agent tasks, including implicit task assignment.

A. STL for multi-agent specifications

  • STL provides time-explicit rules over continuous signals, and formal task descriptions can support automatic control-action synthesis.The paper focuses on predicates that characterize whether a point lies in a polytope.Source: §I · p. 1, A. STL for multi-agent specifications · p. 2

A. Related work

  • Abstraction-based planning requires domain expertise and can scale poorly as state-space dimensionality grows, while MPC may require too many time steps for long horizons.The related-work discussion also contrasts timed waypoints with fixed-step MPC and describes sampling-based approaches for temporal-logic planning.Source: §I · p. 1, A. Related work · p. 2

I. INTRODUCTION

  • Timed waypoints define piece-wise linear reference paths whose STL constraints are encoded recursively, yielding linear constraints and MILP solutions.The approach accounts for tracking error and automatically assigns subtasks while avoiding collisions.Source: §I · p. 1
  • The method outperforms other state-of-the-art methods in runtime and planned-path quality across eight benchmark problems, and is an order of magnitude faster than stlcg.The MPC-based method in failed in some cases due to its number of decision variables, while the proposed method found solutions.Source: §I · p. 2

A. STL for multi-agent specifications

  • MA-STL extends STL to multiple trajectories, allowing tasks to be assigned implicitly while restricting temporal operators to a single agent at a time.The specification is a subset of STL formulas over the joint state space of the agents.Source: A. STL for multi-agent specifications · p. 3

B. Tracking controllers for the agents

A tracking controller separates planning from nonlinear robot dynamics by following a reference path within a known error bound. The planner can use this bound to ensure robust specification satisfaction.

B. Tracking controllers for the agents

  • The method assumes each agent has a tracking controller that follows any reference path under bounded disturbances with known error ϵ.The bound holds when reference paths meet controller requirements, such as bounded velocity.Source: B. Tracking controllers for the agents · p. 3
  • Because the actual trajectory stays within a tube around the reference path, ensuring the specification for every trajectory in that tube guarantees satisfaction under bounded disturbances.The paper calls this property ϵ-robustness.Source: B. Tracking controllers for the agents · p. 3

C. The MA-STL motion planning problem

The planning problem is to find reference paths for multiple agents that satisfy an MA-STL specification robustly while respecting initial positions and avoiding collisions. The search is restricted to piece-wise linear paths built from time-stamped waypoints.

C. The MA-STL motion planning problem

  • A valid solution starts each agent at its specified initial position, avoids inter-agent collisions throughout [0,T], and is ϵ-robust with respect to the MA-STL formula.Collision constraints enlarge each agent's radius by the tracking-error bound ϵ.Source: C. The MA-STL motion planning problem · p. 3
  • The reference paths are restricted to piece-wise linear trajectories formed from time-stamped waypoints.Each waypoint pairs a time instant with a position, and consecutive waypoints define path segments.Source: C. The MA-STL motion planning problem · p. 3

III. SOLVING THE PLANNING PROBLEMS USING MILP

The planner represents timed waypoints and task constraints as a MILP, with STL satisfaction and collision avoidance encoded as linear constraint formulas. Inductive rules make the STL encoding sound for trajectories within the tracking-error bound.

III. SOLVING THE PLANNING PROBLEMS USING MILP

  • The optimization variables are waypoint times and positions, and the linear objective can minimize total travel time or makespan subject to the planning conditions.The encoding introduces binary variables to represent logical relations.Source: §III · p. 4

A. Encoding MA-STL satisfactions with LCFs

  • STL satisfaction is encoded inductively as linear constraint formulas over path segments, so truth of the resulting formula guarantees robust satisfaction for trajectories within tracking error ϵ.The rules are stronger than necessary because they require satisfaction over an entire segment, but this is needed for the induction argument.Source: A. Encoding MA-STL satisfactions with… · pp. 4–5
  • Atomic predicates are encoded using endpoint constraints on shrunken or bloated polytopes, which suffice to ensure that each linear path segment remains inside or outside the relevant region.The endpoint conditions support the soundness of the segment-level encoding.Source: A. Encoding MA-STL satisfactions with… · p. 4

III. SOLVING THE PLANNING PROBLEMS USING MILP

  • The algorithm recursively resolves dependencies among STL subformulas to construct the final constraint formula, then eliminates disjunctions using the big-M method and binary variables.The full proof of soundness proceeds by induction over the STL operators.Source: §III · p. 4, A. Encoding MA-STL satisfactions with… · p. 5

B. Encoding inter-agent collision avoidance with LCFs

The section encodes inter-agent collision avoidance as linear constraint formulas (LCFs) over time-stamped path segments. The encoding treats segments as safe when they are separated in time or sufficiently separated in space.

B. Encoding inter-agent collision avoidance with LCFs

  • A segment-pair LCF is true when the segments are disjoint in time or their centers are separated beyond their half-lengths plus margin ϵ.The section uses this condition as the building block for inter-agent collision avoidance.Source: B. Encoding inter-agent collision… · p. 5
  • Combining the segment-pair conditions encodes that all agents avoid collisions throughout their paths.The resulting formula is an LCF over the waypoint decision variables.Source: B. Encoding inter-agent collision… · p. 5
  • The encoding uses the 1-norm instead of the 2-norm to keep the expression linear or piece-wise linear; soundness is proved in the Appendix.Source: B. Encoding inter-agent collision… · p. 5

C. Overall algorithm

The algorithm combines STL-satisfaction and collision-avoidance constraints in an AND-OR tree, converts its disjunctions into MILP constraints, and solves for timed waypoints. Its encoding complexity is O(K^2 · |ϕ|), which can be advantageous over MPC when the horizon is long but few path segments suffice.

C. Overall algorithm

  • The algorithm merges STL-satisfaction and collision-avoidance LCFs into an AND-OR tree whose leaves are linear expressions.AND nodes represent conjunctions and OR nodes represent disjunctions.Source: C. Overall algorithm · p. 5
  • Each path's waypoint times are ordered within the user-specified horizon, and the algorithm constrains maximum velocity and the initial position.The initial-position constraint appears in the continuation of the section.Source: C. Overall algorithm · p. 5
  • Big-M constraints and binary variables eliminate tree disjunctions, converting the formula into linear constraints for the MILP optimizer.At least one child constraint of each OR node must be enabled.Source: C. Overall algorithm · p. 5
  • The encoding has complexity O(K^2 · |ϕ|), versus O(N · |ϕ|) for MPC; it can be advantageous when long horizons require few path segments, while MPC may suit short horizons with many segments.The algorithm returns feasible waypoint values as piece-wise linear paths.Source: C. Overall algorithm · p. 6

IV. EXPERIMENTAL EVALUATION

The evaluation uses benchmark scenarios to compare the proposed approach with other methods, with experiments implemented using Python and Gurobi. The robot dynamics are modeled as Dubins vehicles.

IV. EXPERIMENTAL EVALUATION

  • The evaluation compares the proposed approach with other methods across benchmark scenarios.Source: §IV · p. 6
  • Experiments use Dubins vehicle dynamics and solve MILP problems with Gurobi from a Python implementation.Source: §IV · p. 6
  • The experiments ran on a Linux workstation with two Intel Xeon Silver 4110 CPUs and 32 GB RAM.Source: §IV · p. 6

A. Benchmarks

The benchmarks span single-robot STL tasks, multi-agent collision avoidance, and complex rover specifications. Some scenarios come from prior motion-planning work, while others were designed to test complicated multi-agent STL tasks.

A. Benchmarks

  • The benchmark suite combines scenarios from prior motion-planning work with new benchmarks designed to test complicated multi-agent STL specifications.Source: A. Benchmarks · p. 6
  • The stlcg-1 benchmark asks a robot to reach an upright corner while visiting and avoiding specified regions; stlcg-2 uses the same environment with a different STL specification.The original circular region B is replaced by its circumscribed square in these benchmarks.Source: A. Benchmarks · p. 6
  • The doorpuzzle benchmarks require visiting a goal while navigating walls and doors, with a corresponding key region visited before each door can be opened.doorpuzzle-2 extends the similar scenario to six doors.Source: A. Benchmarks · p. 6
  • The rover tasks combine goal visits with periodic charging, timely data transmission, wall avoidance, and inter-agent collision avoidance.The passage describes rover-1 and rover-2 as tests of complicated multi-agent STL specifications.Source: A. Benchmarks · p. 6
  • The wall-1 and wall-2 scenarios test multi-agent collision avoidance: agents visit goals through a narrow door and must determine an order for passage.Source: A. Benchmarks · p. 6

B. Comparison with other methods

The paper compares its planner with MPC- and abstraction-based methods on benchmark problems, reporting broader STL task coverage and generally faster runtime. It also reports safe task completion on selected benchmarks using Robotarium robots.

B. Comparison with other methods

  • The comparison could not include the closest prior approach or doorpuzzle results from, because implementations or reported runtimes were unavailable.The implemented abstraction-based method supports wall-1 and wall-2, but not general STL specifications.Source: B. Comparison with other methods · pp. 6–7
  • Figure 1 contrasts dashed PWL reference paths with solid tracked trajectories, while Figure 2 adds four timed snapshots per benchmark with agent locations and colors.Figure 1 marks starts with circles and endpoints with stars.Source: Figure 1 · p. 7, Figure 2 · p. 7
  • For MPC, the comparison used an integrator model with Δt = 0.1 and set its horizon to the proposed method’s optimized-path makespan.Preprocessing time to determine path length or horizon was excluded from Table I.Source: B. Comparison with other methods · p. 7

C. Observations

  • The method solved complex multi-agent STL problems with up to four agents while comparison methods failed in some cases, and it ran faster in almost all cases.For stlcg-1 and stlcg-2, stlcg took minutes while the proposed method took less than one second.Source: C. Observations · pp. 7–8, Table I · p. 7
  • Robotarium experiments on doorpuzzle-1, doorpuzzle-2, wall-1, and wall-2 showed that the robots safely completed the tasks with the proposed approach and tracking controller.Tracking error for the real robots was estimated from simulations using the official simulator.Source: C. Observations · p. 8

V. CONCLUSION

  • The conclusion identifies combinatorial use of PWL reference paths and guaranteed tracking controllers as the basis for long-horizon synthesis, with larger-scale planning left for future work.The authors also plan to reduce encoding complexity.Source: §V · p. 8

A. Soundness of the STL encoding

The STL encoding is sound under bounded tracking error: truth of the waypoint constraints guarantees the temporal formula for trajectories within the tracking-error bound.

A. Soundness of the STL encoding

  • Lemma 1 uses endpoint half-space margins to keep the entire ϵ-neighborhood of a segment outside the polytope.The segment lies in a half-space whose margin exceeds ϵ, so its ϵ-ball cannot intersect the polytope.Source: A. Soundness of the STL encoding · p. 9
  • Lemma 2 ensures the segment’s ϵ-neighborhood lies inside the original polytope when both endpoints lie in the polytope shrunk by ϵ.The proof uses convexity of the shrunken polytope to contain the whole segment.Source: A. Soundness of the STL encoding · p. 9
  • If the encoded STL constraints are true, every trajectory staying within tracking error ϵ of the piecewise-linear path satisfies the formula over the stated intervals.The proof proceeds by induction from atomic predicates to the full formula.Source: A. Soundness of the STL encoding · pp. 9–10
  • The inductive proof establishes soundness for the always operator and for conjunctions and disjunctions.For always, it checks intersecting waypoint intervals; Boolean cases follow from the encoded subformulas.Source: A. Soundness of the STL encoding · p. 9
  • The encoding proves eventuality and until by selecting an intersecting waypoint interval that witnesses the required subformula.For until, the proof also checks that the preceding subformula holds throughout the interval up to the witness.Source: A. Soundness of the STL encoding · p. 9
  • Release is sound when each relevant interval satisfies the second subformula or has an earlier interval satisfying the first.This completes the operator-by-operator inductive argument for arbitrary STL formulas.Source: A. Soundness of the STL encoding · p. 10

B. Soundness of the inter-agent collision avoidance encoding

The collision-avoidance encoding guarantees separation of the agents’ tracking-error tubes over overlapping segment times, and extends this guarantee to their actual trajectories under the stated tracking assumption.

B. Soundness of the inter-agent collision avoidance encoding

  • When the encoded safety condition holds, the agents’ radius- and tracking-error-inflated segment tubes are disjoint throughout their overlapping time interval.Theorem 2 states the separation condition using 2ϵ plus the two agent radii.Source: B. Soundness of the inter-agent… · p. 10
  • The geometric proof uses a lower bound on segment separation to show the inflated balls cannot intersect.The bound is obtained using the triangle inequality.Source: B. Soundness of the inter-agent… · p. 10
  • If each actual trajectory stays within tracking error ϵ of its reference path, the encoded inter-agent condition prevents collisions even with disturbances.The guarantee follows by applying Theorem 2 to the tracking-error tubes.Source: B. Soundness of the inter-agent… · p. 10
Loading 2201.05247v1…