PaperlayerView exact revision on arXiv

Source-linked AI summary

A Hyper-Logical View on Multi-Agent Path Planning

Hadar Frenkel, Dor Atzmon

arXiv:2610.35964v1cs.MAcs.AI

TL;DR

MAPP variants address collision-free planning tasks with different requirements, while specialized algorithms are often developed for individual variants. This paper models many variants in HyperLTL and HyperQPTL, including cross-agent constraints and optimality, and reduces optimal-solution finding to model checking. Its contribution is a common specification and reasoning layer, not a claim that current hyperproperty tools replace mature MAPP solvers.

  • Problem

    MAPP has many variants for different planning tasks, and most have been addressed with specialized algorithms rather than a shared specification approach.

    Source: §1 · p. 1

  • Method

    The paper modularly encodes MAPP variants, cross-agent constraints, and cost functions in HyperLTL or HyperQPTL, then reduces optimal-solution finding to model checking.

    Source: §1 · p. 1, §4.3 · p. 6

  • Results

    Many MAPP variants can be modeled in HyperLTL or HyperQPTL, with optimal-solution finding reduced to hyperlogic model checking.

    Source: §1 · p. 1

  • Takeaways & Limitations

    The hyper-logical view provides a common specification language for comparing MAPP variants and formalizing their distinct requirements.

    Source: §6 · p. 7

    Current hyperproperty model checkers have high worst-case complexity, and the paper does not claim they compete with mature MAPP solvers.

    Source: §3.1 · p. 3

Abstract

from arXiv · show

Multi-Agent Path Planning (MAPP) requires collision-free paths for multiple agents. MAPP has numerous real-life applications, including the navigation of automated vehicles, and has therefore many variants considering different constraints, requirements, and objectives. For each such variant, a new algorithmic treatment is often developed. This paper takes a complementary, specification-centered view: we show that many MAPP variants can be modeled in HyperLTL, a temporal logic that reasons about multiple paths and their evolution through time, and in its omega-regular extension HyperQPTL. The contribution is not a claim that current hyperproperty model checkers replace specialized MAPP solvers. Rather, the hyper-logical view gives a unified language for comparing MAPP variants, adding cross-agent constraints, expressing optimality, and connecting MAPP to verification, explanation, and causality techniques for hyperproperties.

1 Introduction

MAPP covers collision-free multi-agent path planning across varied applications and task variants, which have often received specialized algorithms. The paper instead presents a shared HyperLTL and HyperQPTL specification approach for expressing these variants, cross-agent constraints, and optimality.

1 Introduction

  • MAPP plans collision-free paths for agents in applications ranging from warehouse robots to autonomous vehicles, with MAPF requiring each agent to reach its assigned goal.Optimal MAPF is NP-hard for standard objectives, though specialized algorithms can solve many-agent instances.Source: §1 · p. 1
  • Many MAPP variants address different real-life planning tasks, and most have specialized algorithms adapted from CBS or other MAPF techniques.Source: §1 · p. 1
  • The paper models many MAPP variants modularly in HyperLTL and HyperQPTL, logics that relate multiple paths over time rather than reasoning about one path at a time.Source: §1 · p. 1
  • The contributions include expressing cross-agent constraints and cost functions such as makespan, then reducing optimal-solution finding to hyperlogic model checking.Source: §1 · p. 1

2 Preliminaries

The preliminaries define conflict-free plans, objectives, and nine MAPP variants, then introduce the trace-based logics used to specify them. HyperLTL quantifies over paths, while HyperQPTL additionally quantifies over propositions.

2.1 Planning

  • A plan assigns each agent a path from its start, requires paths to avoid vertex and edge conflicts, and can be optimized for sum-of-costs or makespan.The path cost counts actions, while sum-of-costs sums path costs and makespan takes their maximum.Source: §2.1 · p. 2
  • MAPF assigns each agent a goal, while AMAPF leaves goal assignment open, MCPF requires all goals to appear on paths, TAPF gives each agent a goal set, and MAPD assigns pickup-delivery tasks.Source: §2.1 · p. 2
  • MAPF-PC adds ordered goal sequences and cross-agent precedence constraints, specifying which agent must visit a goal before another agent visits its goal.Source: §2.1 · p. 2
  • RMAPF forbids different agents from occupying the same vertex within delay k, MTPF adds occupied tails, and MAM sends agents to a shared meeting vertex.Source: §2.1 · p. 2
  • AMAPF and MAM are optimally solvable in polynomial time, whereas the other listed variants are NP-hard; the paper treats MAPD as a one-shot problem.Source: §2.1 · p. 2

2.2 Logic

  • A labeled transition system has states, initial states, transitions, and atomic-proposition labels; its traces are infinite sequences of labels along valid state transitions.Source: §2.2 · p. 3
  • HyperLTL extends LTL with trace quantification for relational properties over executions, while HyperQPTL adds quantification over atomic propositions that can mark timesteps.Source: §2.2 · p. 3

3 Modeling MAPP in HyperLTL

The section presents HyperLTL as a modular specification language for MAPP: it separates shared path requirements from variant-specific constraints and represents graph paths as traces of a transition system. It translates MAPF and several variants into formulas, with correctness established for the MAPF encoding.

3 Modeling MAPP in HyperLTL

  • Separating core planning from cost functions makes the encodings modular across MAPP variants and objectives.The paper positions this as a specification and reasoning layer, not a claim that current model checkers compete with mature MAPP solvers.Source: §3 · p. 3, §3.1 · pp. 3–4

3.1 Motivation

  • HyperLTL can relate different agents’ paths, allowing additional cross-agent requirements to be combined with a MAPP specification.The example requires one agent to remain in a neighboring vertex whenever another occupies a given vertex; path relations can also express pairwise or beyond-pairwise reasoning patterns.Source: §3.1 · p. 4

3.2 Modeling the MAPP Instance as an LTS

  • The instance-to-LTS transformation makes each graph vertex a labeled state and allows waits or moves along edges; its traces are exactly the possible instance paths.This correspondence is stated as Observation 1.Source: §3.2 · p. 4

3.3 Translation into HyperLTL

  • The MAPF formula captures valid solutions: prescribed starts, eventual goal arrival with agents staying there, and conflict-free paths.Theorem 1 establishes that the transition system satisfies the formula exactly when the paths represent a MAPF solution; agents may pass through a goal before finally remaining there.Source: §3.3 · p. 4
  • The translation pattern covers variants including anonymous and combinatorial goals, task assignments, precedence constraints, bounded-horizon conflicts, multi-train occupancy, and meetings.The encodings reuse start, goal, and conflict components where applicable; precedence constraints use HyperQPTL propositions to mark goal-satisfaction times and compare them across agents.Source: §3.3 · p. 5

Other Assumptions on Reaching the Goal

  • Changing the goal formula can model agents clearing a reached goal and continuing to move, rather than remaining there.The paper presents this as an example of adapting the modular model to a different goal-reaching assumption.Source: Other Assumptions on Reaching the Goal · p. 6

4 Cost Functions as Hyperproperties

The section expresses makespan optimality in hyperlogic and reduces the existence of an optimal MAPP solution to model checking. It focuses on makespan because sum-of-costs requires asynchronous reasoning outside the paper’s scope.

4.1 Makespan

  • A plan is makespan-optimal when every competing solution has a path at least as long as every path in the plan.The encoding requires that in every other solution, some agent reaches its goal no earlier than all agents in the candidate plan.Source: §4.1 · p. 6
  • A HyperQPTL encoding labels each agent’s goal-satisfaction timestep, making the makespan comparison reusable across MAPP variants.Only the local definition of goal satisfaction changes between variants.Source: §4.1 · p. 6

4.2 Sum-of-Costs

  • Sum-of-costs requires asynchronous reasoning to accumulate path lengths, which is outside synchronous HyperLTL and HyperQPTL.The paper notes that asynchronous temporal hyperlogics can express it by constructing and comparing a trace representing accumulated path lengths.Source: §4.2 · p. 6

4.3 Optimal MAPP via HyperQPTL Model Checking

  • The formula combines a MAPP specification with an optimality condition, and its satisfaction is equivalent to an optimal solution existing.The paths witnessing its outer existential quantifiers form that solution.Source: §4.3 · pp. 6–7

Quantifier Alternation

  • Each path-quantifier alternation adds an exponent to worst-case model-checking complexity, and current hyperproperty tools are not efficient MAPP solvers.The paper presents specialized MAPP algorithms as the appropriate large-scale performance baseline.Source: Quantifier Alternation · p. 7

5 Related Work

Prior work connects planning with hyperproperties and also reduces MAPP to ILP, ASP, or SAT. This paper focuses on modeling concrete MAPP problems and their cost functions and optimality in hyperlogics.

5 Related Work

  • Online and lifelong MAPP introduce agents or tasks over time; the authors say their modeling can generalize by considering a sequence of one-shot problems.The paper’s considered variants are one-shot and end when their given tasks are fulfilled.Source: §5 · p. 7
  • ILP, ASP, and SAT reductions encode temporal constraints with auxiliary variables, while HyperLTL and HyperQPTL express paths and temporal constraints natively.The cited reduction approaches include ILP, ASP, and SAT (Surynek et al. 2016; Barták and Svancara 2019).Source: §5 · p. 7
  • Related work studies probabilistic hyperproperties in decentralized planning, HyperLTL and robotics (Wang, Nalluri, and Pajic 2020), and hyperproperties in conformant planning (Beutner and Finkbeiner 2025).The paper distinguishes its focus on Boolean modeling of a wider variety of concrete MAPP problems.Source: §5 · p. 7
  • Unlike prior hyperlogic-planning work, this paper models concrete MAPP problems and addresses their cost functions and solution optimality.The cited works do not apply their results to actual planning problems studied in the planning community or address cost functions and optimality.Source: §5 · p. 7

6 Conclusion and Future Work

The paper frames hyperlogic as a shared formal language for MAPP and hyperproperties research. It identifies explainability and causality as possible future applications.

6 Conclusion and Future Work

  • Formalizing MAPP variants can expose their subtleties, remove accidental formulation differences, and specify future problems unambiguously.The authors describe the connection as a common specification language for MAPP researchers and a set of concrete planning problems for the hyperproperties community.Source: §6 · p. 7
  • The authors plan to apply hyperproperty explanation techniques to MAPP, where witness traces and their relations can support questions about conflicts, delayed goals, or group constraints.They also plan to study further planning constraints and combine them with verification tasks.Source: §6 · p. 7

A Full Translations for the Makespan Cost Function

The appendix gives makespan encodings for all considered variants, with and without quantified propositions.

A Full Translations for the Makespan Cost Function

A.1 Direct Translation Using HyperLTL

The direct HyperLTL translations reason explicitly about goal formulas to express makespan optimality across MAPP variants. Their cost-function formulas can be reused when a variant retains a similar goal characterization.

A.1 Direct Translation Using HyperLTL

  • The MAPF makespan translation is repeated for completeness, while this section explains why explicit reasoning about goal formulas is needed for its optimality formulas.The quantified-proposition approach can instead treat the goal formula as a black box, with a minor modification.Source: §A.1 · p. 10
  • AMAPF optimality requires reasoning about the quantified paths in the goal formula and checking whether a path in a competing solution is longer.The section denotes non-optimal solutions by τ and their quantified paths by τ′.Source: §A.1 · p. 10
  • For MCPF and TAPF, the non-optimality tests focus respectively on a goal vertex reached too late and an agent that has not reached any goal by the optimal solution’s completion.MCPF goals are not preassigned; TAPF agents must reach one of several goals.Source: §A.1 · p. 10
  • MAPD compares delivery completion times, whereas MAPF-PC compares when an agent satisfies its last goal with the other agents’ last-goal times.The MAPD test considers a delivery vertex reached after all deliveries in the optimal solution; MAPF-PC uses propositions marking goal-satisfaction timesteps.Source: §A.1 · pp. 10–11
  • RMAPF reuses the MAPF cost function, and MTPF uses a simple goal formula; similar goal characterizations allow the cost-function formula to be reused across variants.This is presented as an example of the modularity of the HyperLTL modeling.Source: §A.1 · p. 11
  • For the meeting variant, a non-optimal solution is distinguished by whether all agents meet at a vertex later than they do in the optimal solution.The translation reasons explicitly about the shared meeting vertex.Source: §A.1 · p. 11

A.2 Translation Using HyperQPTL and Quantified Propositions

The quantified-proposition translation marks goal-satisfaction times to express cost functions without reasoning through each goal formula. It adapts these labels to the goal structure of each variant, with a special construction for the meeting variant.

A.2 Translation Using HyperQPTL and Quantified Propositions

  • Quantified propositions mark the timestep at which an agent reaches its goal, making cost-function specifications cleaner in HyperQPTL.The section introduces labeled formulas for the variants and uses them in place of the original goal formulas where applicable.Source: §A.2 · p. 11
  • For MAPF, the labeled goal formula replaces the original goal formula, and the same substitution applies to AMAPF.The AMAPF trace equality is stated to imply equality over quantified and unquantified propositions.Source: §A.2 · p. 11
  • For MCPF, labels mark each agent’s last satisfied goal, including the case where an agent satisfies no goals; TAPF labels its selected goal.MAPD adapts the MCPF reasoning to delivery vertices, while MAPF-PC labels the last goal-satisfaction position.Source: §A.2 · pp. 11–12
  • RMAPF and MTPF reuse the labeled goal formula, whereas the meeting variant uses labels that hold exactly once and simultaneously at the shared meeting time.The meeting variant has no goal formula, so its full formula is modified directly.Source: §A.2 · pp. 11–12

SUMMARY: Expressing the Makespan Cost Function Using HyperQPTL and Quantified Propositions

The generic makespan construction labels the timestep when each agent satisfies its goal, so that timestep represents the path’s length and cost. It tests optimality by comparing those labels across a candidate solution and a competing solution.

SUMMARY: Expressing the Makespan Cost Function Using HyperQPTL and Quantified Propositions

  • Each agent’s quantified label holds when it satisfies its goal, and that timestep is exactly the length and cost of its path.The section uses labeled formulas to support a generic makespan comparison across the modeled variants.Source: SUMMARY: Expressing the Makespan Cost… · p. 12
  • A candidate is checked against a non-optimal solution by asking whether some agent’s label occurs there after all agents’ labels occur in the candidate.The competing solution’s quantified propositions are denoted l′_i.Source: SUMMARY: Expressing the Makespan Cost… · pp. 12–13
  • The generic formula φL can be instantiated with any of the nine labeled formulas to express makespan optimality.The construction defines optimality with respect to the makespan function.Source: SUMMARY: Expressing the Makespan Cost… · pp. 12–13
Loading 2610.35964v1…