Multi-Agent Planning under Local LTL Specifications and Event-Based Synchronization

1 Introduction

• Agents may need collaborators to satisfy individual missions, so plans must include both actions and synchronization decisions while avoiding unnecessary synchronization.The paper focuses on generating discrete plans within a hierarchical controller-synthesis approach.Source: §1 · p. 1
• The method combines local LTL specifications with iterative finite-horizon planning and event-based synchronization rather than synchronization after every discrete step.The approach adapts to differing step durations and replans during execution.Source: §1 · p. 2
• The paper analyzes correctness and identifies assumptions under which repeated planning and execution lead to satisfaction of all tasks.The introduction positions this as a bottom-up approach to multi-agent planning from local LTL specifications.Source: §1 · p. 2

2 Preliminaries

• Words are finite or infinite sequences over a set, with prefixes and suffixes defined as contiguous portions beginning at the start or continuing to infinity.The notation 2^S denotes subsets of S, while S^ω denotes infinite sequences of elements of S.Source: §2 · p. 2
• A transition system has states, an initial state, actions, and a partial deterministic transition function; its trace alternates states and actions.The paper treats a finite trace fragment as a factor of a trace beginning and ending with a state.Source: §2 · p. 2
• LTL formulas express propositions and temporal conditions over infinite words, while Büchi automata accept words when a run visits accepting states infinitely often.The preliminaries define eventuality, always, next, and until operators, and use shortest-path distance in automaton graphs.Source: §2 · pp. 2–3

3 Problem Formulation and Approach

• Each agent’s task may refer to services of itself and a subset of other agents, and the task is satisfied locally from that agent’s perspective.The agent’s strategy includes actions and synchronization requests, and must work regardless of planned action durations.Source: §3 · pp. 3–4
• Action durations are unknown before execution, and their histories inform the semantics of agent behavior and task satisfaction.Transition systems abstract states, actions, and capabilities, while action executions take time.Source: §3 · p. 3
• Agents synchronize by waiting until all agents have sent synchronization requests, then start their next actions simultaneously; otherwise they may request no synchronization.The model assumes requests are sent immediately after an action and actions start immediately after synchronization, with no idling.Source: §3 · p. 3
• Services label actions as events of interest, while a special silent service marks actions without an associated event.Services are the events on which task specifications are defined.Source: §3 · pp. 3–4
• The formal problem seeks traces and synchronization sequences whose behaviors are compatible and whose agent subsets locally satisfy their LTL specifications for arbitrary transition durations.The agents are modeled as transition systems with action-execution and synchronization capabilities.Source: §3 · pp. 3, 5
• Collisions are outside the paper’s scope; they may instead be handled through LTL constraints or low-level controllers.The paper identifies these as alternative ways to resolve collisions.Source: §3 · p. 5
• A conventional solution synchronizes agents in each dependency class after every action and searches a product automaton, which grows exponentially with dependent agents.This correct and complete procedure can also slow the team through frequent synchronization.Source: §3 · pp. 5–6
• The approach decomposes infinite-horizon planning into iterative finite-horizon problems, dynamically builds dependency classes, and replaces stepwise synchronization with event-triggered synchronization.Under certain assumptions, repeated execution and replanning lead to satisfaction of all specifications.Source: §3 · p. 6

4.1 Preliminary Synchronization Sequence

• The preliminary synchronization sequence synchronizes all agents after every action, making their behaviors compatible despite differing transition durations.This sequence is the baseline adjusted by the event-triggered procedure.Source: §4.1 · p. 6, §4.3.2 · p. 10

4.2 Finite Horizon Planning

• Finite-horizon planning separates agents into dependency classes based on current specification states and horizon-limited interactions, enabling separate planning for each class.The partition is recomputed each iteration; splitting an offline class can yield an exponential reduction in computational demands.Source: §4.2 · pp. 6–7

Definition 10 (Progressive function and state)

• For each class, the method builds an intersection automaton and product system, scores progress toward specifications, then projects a shortest path to a maximally progressive state into agent plans.The product system combines permitted task behavior with each agent's finite trace fragments.Source: §4.2 · pp. 7–8, Definition 10 (Progressive function… · p. 8

4 Problem Solution

• Within a finite horizon, the intersection automaton tracks progress across the class’s specifications, and its product with agent transition systems supports selecting executable service-producing paths.The planning inputs include the current system and automaton states, an agent ordering, and horizons h and H.Source: §4.2 · pp. 6–8

4.3.1 Stepwise Solution

• Each iteration executes the first planned action, updates agent and automaton states, and reorders priorities when an agent reaches an accepting state.The stepwise procedure synchronizes agents after each action; the paper assumes plan computation takes no time, with synchronization proposed to handle different computation times.Source: §4.3.1 · p. 9

4.3 Infinite Horizon Replanning

• The iterative procedure shifts the planning horizon forward; replanning keeps the procedure informed about future possibilities, while less frequent replanning trades plan efficiency for lower computational demand.The number of iterations cannot generally be upper-bounded because transition durations are arbitrary.Source: §4.3.1 · p. 9, §4.3 · p. 9

4.3.2 Event-Triggered Solution

• Event-triggered replanning waits to synchronize until collaboration or another specified trigger is needed, reducing synchronization frequency while preserving compatible behavior.Triggers include a non-silent service, an accepting state, the end of a planned fragment, or a synchronization request received from another agent.Source: §4.3.2 · p. 10

• For event-triggered Alg. 3, behaviors remain compatible regardless of transition durations, and each agent visits accepting states infinitely often under Assumptions 1 and 2.The proof also relies on every agent repeatedly becoming the most prioritized one.Source: §5 · p. 11
• The analysis establishes that the returned traces and synchronization sequences solve Problem 1.Source: §5 · p. 11
• Each iteration is linear in the size of PH, but its worst-case complexity reaches that of the straightforward solution: O(N · ∏_{i∈N} |Ti| · |Bi|).Source: §5 · p. 11
• When no accepting state is available within horizon h, the algorithm extends h; if extension stops changing the automaton, it backtracks and forbids a previously executed service.It also extends H when that horizon is too short to find a progressive state.Source: §5 · pp. 11–12
• Horizon selection trades search size against planning progress: short horizons may need extension, while long ones can make the intersection automaton too large.The guidance is to keep that automaton manageable while including as many actions with non-silent services as possible.Source: §5 · p. 12

6 Example

• At most two agents shared a dependency class, yielding product automata with thousands of states rather than about 3 million in the centralized solution.When agents were independent within horizon h, product automata had tens to hundreds of states; each iteration took seconds to minutes.Source: §6 · p. 12
• 30.3 iterations on average completed agent 2’s first 7 services with event-triggered synchronization, versus 54 iterations under stepwise synchronization.For the 20 event-triggered simulations, average completion time was 494.2 time units; the stepwise run averaged about 477.1 time units.Source: §6 · p. 12
• With agent 2 executing transitions faster, event-triggered synchronization averaged 26.3 iterations and 355.6 time units for its first 7 services, versus about 457.5 time units for stepwise synchronization.The faster-agent case used transition durations randomly drawn from {1, ..., 5} for agent 2.Source: §6 · p. 12
• Figure 4 contrasts stepwise trace snapshots after 1, 4, 6, and 7 of agent 2’s services with event-triggered examples after 7 services and after 477 time units.Colors distinguish agents, squares mark services, and arrows show snapshot positions.Source: Figure 4 · p. 13

7 Summary and Future Work

• The approach decomposes infinite-horizon planning into iterative finite-horizon problems, letting agents focus on those constrained by their formulas within a limited horizon.Finite horizons also reduce the size of the handled state space.Source: §7 · p. 13
• Event-based synchronization can replace stepwise synchronization, enabling less frequent synchronization and greater agent independence during execution.Source: §7 · p. 13
• Future work includes optimality requirements, robustness to small perturbations, and evaluation using mobile robots.Source: §7 · p. 13