Pith. sign in

REVIEW 4 major objections 5 minor 66 references

An Abstraction-Free Method for Multi-Robot Temporal Logic Optimal Control Synthesis

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proposes TL-RRT*, an abstraction-free sampling-based planner that grows trees over the product of robot positions and Büchi automaton states, and proves it probabilistically complete and asymptotically optimal for multi-robot…

desk verdict Novel abstraction-free LTL planner with a real completeness gap in the biased suffix construction. read the letter →

arxiv 1909.00526 v4 pith:MDVTMYFT submitted 2019-09-02 cs.RO

Xusheng Luo , Yiannis Kantaros , Michael M. Zavlanos This is my paper · ORCID
classification cs.RO
keywords multi-robotplanninglineartemporallogicBüchiautomatonsampling-basedmotionRRT*optimalcontrolsynthesisprobabilisticcompletenessasymptoticoptimality
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proposes TL-RRT*, a sampling-based planner for multi-robot systems under Linear Temporal Logic (LTL) tasks that avoids the usual discrete abstraction of the workspace. The method grows randomized trees directly in the product of the continuous configuration space and the Büchi automaton representing the task, first finding a prefix that reaches an accepting automaton state and then a cycle that forms the infinite suffix. The paper claims that both the unbiased version and a biased version—which steers samples along shortest paths to accepting states in the automaton—are probabilistically complete and asymptotically optimal. If these guarantees hold, temporal-logic planning would no longer be limited by the size of an abstraction and could scale to large robot teams and complex tasks.

What carries the argument

The central object is the tree $\mathcal{T}$ whose nodes are product states $q_P=(x,q_B)\in W^N_{\mathrm{free}}\times Q_B$ and whose edges are valid product transitions: a continuous move $x\to x'$ combined with a Büchi transition $q_B\xrightarrow{L(x)}q'_B$ enabled by the observation at the starting position. Three mechanisms carry the argument: Extend/Rewire with a connection radius $r_n(V_\mathcal{T})$, which keeps the structure a tree while improving costs; the prefix-suffix decomposition of satisfying plans, which turns the infinite-horizon LTL task into two reachability problems; and biased sampling, which selects nodes close to accepting Büchi states and steers new samples toward the labeled regions required by the next automaton transition. The optimality proof covers a robust near-optimal product path by shrinking balls and shows that, with the stated radius, every ball eventually contains a sample whose label preserves the needed Büchi transition.

What would settle it

Construct a workspace where the unique shortest path satisfying the LTL formula skims along the boundary between two labeled regions, so every neighborhood of the optimal path contains points with different observations. Run unbiased TL-RRT* with growing iteration limits and record whether the tree ever adds a node with the required Büchi state within a small distance of that boundary and whether the returned cost converges to $(1+\epsilon)J^*$; if the success probability stays bounded away from 1, the label-stability assumption is the limiting step.

Watch

Extended reading notes

Core claim

The central claim is that optimal multi-robot LTL planning can be solved by RRT*-style tree search over the product state space $W^N_{\mathrm{free}}\times Q_B$, without constructing a discrete transition system. The tree grows by sampling configurations, steering toward them, and connecting a new node to the minimum-cost feasible parent in a neighborhood (Extend), then rewiring neighbors (Rewire); an edge is valid only if the straight-line motion is obstacle-free, crosses each labeled region boundary at most once, and the label enables a Büchi transition. The same construction, repeated with a root at an accepting state, produces a suffix cycle. The main theorems assert that as the iteration limits go to infinity, the probability of finding a feasible plan goes to 1, and the cost of the returned plan is at most $(1+\epsilon)$ times optimal, for both unbiased and biased sampling, with a larger connection radius required in the biased case.

Load-bearing premise

The load-bearing premise is that around every reachable position a small neighborhood exists in which the robot sees the same regions and the same Büchi transitions remain enabled—a condition that generally fails on the boundary of a labeled region.

Editorial extensions

If this is right

  • For LTL tasks without the next operator, TL-RRT* returns a prefix-suffix plan whose continuous execution provably satisfies the formula, covering sequencing, surveillance, and intermittent-connectivity tasks directly in continuous space.
  • With either unbiased or biased sampling, the probability of finding a feasible plan tends to 1 as the iteration limit grows, so no precomputed discrete abstraction is needed for completeness.
  • The biased variant is claimed to scale to dozens of robots (experiments go up to 56 robots) and to find lower-cost first feasible plans than the RRG, synergistic, and SMC baselines.
  • As the number of iterations grows, the returned plan's cost satisfies $J \le (1+\epsilon)J^*$, so longer runs trade computation for near-optimality.
  • Because only trees are stored, retrieving a plan is $O(|V_\mathcal{T}|)$, avoiding the graph-search overhead of product-automaton methods.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The label-stability assumption suggests a concrete hybrid extension: combine tree sampling with boundary-aware states or local cell decomposition near region boundaries, so that optimal paths which hug a boundary can still be approximated without the assumption failing.
  • The biased-sampling machinery depends only on having a distance metric over automaton states, so it could be ported to other automata (for example, parity or Rabin automata) or to non-Euclidean cost functions, with the same two-hop steering structure.
  • Because the proof's connection radius uses the unknown optimal cost, a practical refinement would be to estimate $J^*$ adaptively from the current tree costs, or to use radius zero for initial feasibility and then switch to a rewiring radius for refinement; the paper's simulations already show radius zero is effective for scalability.
  • A testable extension would add observation noise or require the robots to stay inside small neighborhoods of waypoints; the paper's Remark 4.1 suggests such robustness informally, and the same prefix-suffix tree construction could be re-run with inflated regions to quantify the resulting cost loss.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper proposes TL-RRT*, a sampling-based planner for multi-robot systems under global LTL−© specifications. It grows trees in the product of the continuous free workspace and the Büchi automaton, avoiding discrete abstractions, and extracts prefix-suffix plans from accepting nodes. A biased sampling variant, guided by shortest paths in the Büchi automaton, is introduced to accelerate plan construction. The paper claims probabilistic completeness and asymptotic optimality for both the unbiased and biased variants (Theorems 6.3 and 6.5, Corollaries 6.4 and 6.6) and reports simulations comparing favorably with SMC, RRG, and synergistic methods.

Significance. If the claims were correct, the contribution would be significant: an abstraction-free tree-based LTL planner with probabilistic completeness and asymptotic optimality, plus a biased variant that scales to larger teams. The paper has real strengths: the product-space tree construction is a natural extension of RRT*; the unbiased suffix closing via a direct transition into the root is a clean lasso construction; the biased sampling mechanism is described in concrete detail; and the experimental section includes comparisons to established methods with code availability stated. However, the central correctness claims are not established as written. The biased suffix construction restricts accepting cycles to a special class, and the key Assumption 6.2 fails in general labeled environments. These issues affect the headline claims and require substantial revision.

major comments (4)
  1. [Section V-B, Corollaries 6.4 and 6.6] The biased suffix construction does not realize general accepting lassos. The algorithm stores only nodes whose Büchi component equals the root's accepting state and then connects them to the root by RRT* paths that treat all labeled regions as obstacles. Therefore the only accepting cycles it can close are those in which the accepting state is re-entered and then followed by an observation-free segment that keeps the automaton in that accepting state until the root. This excludes lassos in which the accepting state must be exited immediately through a labeled transition. For example, a standard degeneralized NBA for □♦a∧□♦b has an accepting state qF with transitions qF --a--> q1 and q1 --b--> qF and no qF --∅--> qF self-loop; the qF state is visited in a position labeled a, so the label-free geometric return required by Section V-B either does not exist or changes the infinite word by omitting the required visit to a. Appendix B argues only that RRT* can find continuous return paths and that biased sampling densifies the tree; it never proves that the automaton-level cycle set generated by storing same-Büchi-component nodes covers all accepting runs. Consequently Corollaries 6.4 and 6.6 are unsupported.
  2. [Section VI, Assumption 6.2] Assumption 6.2 fails at boundaries of labeled regions. For any reachable product state (x,qB) with x ∈ ∂𝓁j, every ball Bδ(x) contains positions whose observation differs from L(x), and those positions need not be pairable with the same Büchi state qB or reachable from the root. Since Theorems 6.3 and 6.5 invoke Assumption 6.2 for every state along candidate paths, the results are conditional on an assumption that is not implied by the environment model in Definition 3.1 and Assumption 6.1. The paper should either prove Assumption 6.2 for the considered class of environments or explicitly restrict the theorems to label-stable paths, for example paths with positive clearance from every region boundary, and justify why such paths suffice for the claimed completeness and optimality.
  3. [Appendix C, proof of Theorem 6.5] The asymptotic optimality proof is incomplete as written. Appendix C states 'We omit the details due to space limitations' for event E3_n, which is needed to bound the cost of the reconstructed path by (1+ε)J(τ*) and to rule out zig-zag approximations. The argument that P(E1_n|E2_n) → 0 also treats cn, the number of balls crossed by a boundary, as 'small' without a formal bound; this is a geometric and probabilistic quantity that deserves a rigorous analysis. Theorem 6.5 therefore rests on an omitted proof step.
  4. [Section IV-A, Eq. (7)-(8)] The connection radius rn(VT) uses a constant γ_TL-RRT* whose lower bound contains the unknown optimal cost J(τ*). Section VII-A acknowledges that (7) cannot be computed and replaces it with the heuristic radius (17) in the experiments. Thus the implemented algorithm does not run in the parameter regime of Theorem 6.5, and the experiments support only the heuristic version. The paper should specify how γ_TL-RRT* is chosen before planning, or state the theorem as an existence result for all sufficiently large γ and treat the practical radius separately.
minor comments (5)
  1. [General] The symbol P is used both for the product Büchi automaton and for the set of goal nodes in Algorithm 1; these uses should be renamed to avoid confusion.
  2. [Section V-B] The sentence describing the biased suffix construction is ambiguous: it is unclear whether a node whose Büchi component equals the root's accepting state is added to the tree in addition to being stored in the set P.
  3. [Tables II and III] Table III is difficult to read: several columns are visually merged, and the remark that 'the 0 standard deviation is dropped' is unexplained. Please reformat the tables and state what each column contains.
  4. [Section V-A] There are typos such as 'prune NBA' for 'pruned NBA' and 'succesive' for 'successive'; a copyedit pass is needed.
  5. [Section VI] The notation in Eq. (7) and Eq. (17) uses different exponents (1/(dim+1) versus 1/dim). The text explains this, but a short comment near the definitions would prevent reader confusion.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the guarantees are adapted from external RRT* proofs, the sampling bias is inherited only as a design heuristic, and the theoretical connection radius is an existence parameter rather than a fitted input.

full rationale

I walked the derivation chain from Problem 1 through the prefix/suffix tree construction, the biased variant, and Theorems 6.3/6.5 and Corollaries 6.4/6.6. The prefix goal (4) and suffix goal (9) are standard Büchi lasso conditions: a prefix is a path to an accepting state and a suffix is a transition back to that accepting state. The tree-extend/rewire rules (Alg. 3-4) check the PTS and NBA transition relations directly, so the correctness claim that any plan tau_a = tau^{pre,a}[tau^{suf,a}]^omega satisfies phi is a correct-by-construction claim, not a restatement of an input. The optimality proof explicitly relies on external RRT* results (Karaman-Frazzoli [6] and Solovey et al. [47]) and adapts them to the product space; no equation in the proof is equivalent to the theorem's conclusion. The connection radius (7) depends on J(tau*) through (8), but only as a sufficient lower bound in the standard RRT* sense, not as an empirical fit; the practical radius (17) is explicitly presented as an approximation and no optimality theorem is claimed for it. The biased sampling method is motivated by the authors' earlier discrete-space work [30], [31], but Appendix B re-derives the biased completeness argument from the same one-hop-neighborhood machinery, and the external probabilistic completeness of RRT* is invoked for the cycle return path. Thus the self-citations are not load-bearing in the formal results. The reviewer's concern about the biased suffix only finding cycles with repeated root-Büchi-state nodes and observation-free returns is a correctness/coverage issue, not a circularity issue, and I do not count it here.

Assumptions & free parameters 4 free parameters · 6 assumptions · 0 invented entities

The central claim rests on standard automata theory, two explicit assumptions on the workspace and reachable neighborhoods, and the unverified assumption that continuous paths remain equivalent to discrete traces. The practical algorithm also depends on several hand-chosen simulation parameters, including a heuristic connection radius that is not the radius used in the theorems.

free parameters (4)
  • gamma heuristic for connection radius = ceil(4 * (mu(Wfree^N)/zeta_dim)^(1/dim))
    Used in Eq. (17) in simulations; chosen by hand and differs from the theoretical radius (7), which needs the unknown optimal cost J(tau*). It determines the local-neighborhood size and affects both cost and runtime.
  • step size eta = 0.25*N in simulations
    User-specified Steer bound; controls how far a new sample can be from its nearest tree node, hence connectivity of the tree in Section IV-A.
  • biased sampling parameters = pclosest=0.9, yrand=0.99, pidle=1, sigma_d=1/3, sigma_alpha=pi/108
    Hand-tuned in Section VII; these control how strongly samples are pulled toward target regions and strongly influence the reported speedups and costs.
  • cost weight w = 0.2
    User weight in the cost J = w*J_prefix + (1-w)*J_suffix in Eq. (3); affects optimality comparisons across methods.
assumptions (6)
  • standard math The LTL-to-NBA translation is correct and the NBA accepts exactly Words(phi).
    Used in Algorithm 1 line 1 and Definition 2.1; standard result from [11] and [45].
  • domain assumption Assumption 6.1: every labeled region has positive Lebesgue measure.
    Needed so random samples can hit regions with nonzero probability; reasonable for physical regions but excludes points or measure-zero goals.
  • ad hoc to paper Assumption 6.2: every reachable product state has a label-stable ball of positions all pairable with the same Büchi state and reachable from the root.
    Introduced in Section VI and used in Lemmas A.2-A.5 and the optimality proof; fails at region boundaries and is not justified by the planning model.
  • domain assumption Straight-line transitions crossing at most one region boundary per robot preserve LTL satisfaction under continuous execution.
    Stated in Section III Definition 3.1 and used to reduce continuous paths to discrete plans; relies on an ordering of boundary crossings that is not modeled in the paper.
  • domain assumption Robust feasibility and existence of an optimal plan tau*.
    Used in Theorem 6.5 following [47]; needed to construct the approximating product path for asymptotic optimality.
  • domain assumption Sampling is bounded away from zero on Wfree, and biased sampling retains a uniform component with probability (1-yrand)^N.
    Needed for probabilistic completeness and for the gamma bound in Corollary 6.6; stated informally around Eqs. (11)-(14).

how reviews work

0 comments
Cite this review

Pith. "Pith review of An Abstraction-Free Method for Multi-Robot Temporal Logic Optimal Control Synthesis." pith.science (2026). https://pith.science/paper/MDVTMYFT

@misc{pith2026190900526,
  author       = {Pith},
  title        = {Pith review of: An Abstraction-Free Method for Multi-Robot Temporal Logic Optimal Control Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MDVTMYFT}},
  note         = {Machine review of arXiv:1909.00526}
}
abstract

The majority of existing Linear Temporal Logic (LTL) planning methods rely on the construction of a discrete product automaton, that combines a discrete abstraction of robot mobility and a B$\ddot{\text{u}}$chi automaton that captures the LTL specification. Representing this product automaton as a graph and using graph search techniques, optimal plans that satisfy the LTL task can be synthesized. However, constructing expressive discrete abstractions makes the synthesis problem computationally intractable. In this paper, we propose a new sampling-based LTL planning algorithm that does not require any discrete abstraction of robot mobility. Instead, it incrementally builds trees that explore the product state-space, until a maximum number of iterations is reached or a feasible plan is found. The use of trees makes data storage and graph search tractable, which significantly increases the scalability of our algorithm. To accelerate the construction of feasible plans, we introduce bias in the sampling process which is guided by transitions in the B$\ddot{\text{u}}$chi automaton that belong to the shortest path to the accepting states. We show that our planning algorithm, with and without bias, is probabilistically complete and asymptotically optimal. Finally, we present numerical experiments showing that our method outperforms relevant temporal logic planning methods.

Figures

Figures reproduced from arXiv: 1909.00526 by the authors.

Figure 2
Figure 2. Graphical depiction of Alg. 4. The dashed gray arrow stands for the [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. The NBA for the specification ♦π `1 1 ∧ ♦π `2 2 . infinite set. To sample from a finite node set of the tree with size n, we first compute the cumulative probability function of the event {i ≤ n} assuming the node set is infinite, then we renormalize, so that the probability that a node is selected as q closest P is proportional to that when the node set is infinite. 2) Selection of q succ,1 B , q succ,2 B ∈ QB: Nex… view at source ↗
Figure 4
Figure 4. Graphical depiction of the proposed biased sampling for robot [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figures from the paper (4 more)
Figure 5
Figure 5. Figure 5: An illustration of the construction of balls covering the whole product [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: The parameters are set as follows: the step-size η of the function Steer is 0.25N, where N is the number of robots, and w in the cost function (3) is 0.2. In the biased sampling method, pidle = 1, pclosest = 0.9, yrand = 0.99, µd = µα = 0, σd = 1/3, and σα = π/108. The…
Figure 7
Figure 7. Figure 7: An illustration of the scenario where the distance between [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]
Figure 9
Figure 9. Figure 9: Graphical depiction of cases where boundaries of regions cross [PITH_FULL_IMAGE:figures/full_fig_p020_9.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

66 extracted references · 60 canonical work pages

  1. [1]

    S. M. LaValle, Planning algorithms. Cambridge university press, 2006

    2006

  2. [2]

    Principles of robot motion: theory, algorithms, and imple- mentations,

    H. Choset, K. Lynch, S. Hutchinson, G. Kantor, W. Burgard, L. Kavraki, and T. S., “Principles of robot motion: theory, algorithms, and imple- mentations,” Boston, MA, 2005

    work page 2005

  3. [3]

    Mobile robot navigation in unknown environment based on exploration principles,

    I. Arvanitakis, K. Giannousakis, and A. Tzes, “Mobile robot navigation in unknown environment based on exploration principles,” in 2016 IEEE Conference on Control Applications (CCA) . IEEE, 2016, pp. 493–498

    work page 2016

  4. [4]

    Rrt-connect: An efficient approach to single-query path planning,

    J. J. Kuffner and S. M. LaValle, “Rrt-connect: An efficient approach to single-query path planning,” in Proceedings 2000 ICRA. Millennium Conference. IEEE International Conference on Robotics and Automa- tion. Symposia Proceedings (Cat. No. 00CH37065), vol. 2. IEEE, 2000, pp. 995–1001

    work page 2000

  5. [5]

    Prob- abilistic roadmaps for path planning in high-dimensional configuration spaces,

    L. E. Kavraki, P. Svestka, J.-C. Latombe, and M. H. Overmars, “Prob- abilistic roadmaps for path planning in high-dimensional configuration spaces,” IEEE transactions on Robotics and Automation , vol. 12, no. 4, pp. 566–580, 1996

    1996

  6. [6]

    Sampling-based algorithms for optimal motion planning,

    S. Karaman and E. Frazzoli, “Sampling-based algorithms for optimal motion planning,” The International Journal of Robotics Research , vol. 30, no. 7, pp. 846–894, 2011

    2011

  7. [7]

    Temporal logic motion planning for mobile robots,

    G. E. Fainekos, H. Kress-Gazit, and G. J. Pappas, “Temporal logic motion planning for mobile robots,” in Proceedings of the 2005 IEEE International Conference on Robotics and Automation . IEEE, 2005, pp. 2020–2025

    work page 2005

  8. [8]

    Distributed data gathering with buffer constraints and intermittent communication,

    M. Guo and M. M. Zavlanos, “Distributed data gathering with buffer constraints and intermittent communication,” in2017 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2017, pp. 279– 284

    work page 2017

Show all 66 references
  1. [9]

    Distributed intermittent connectivity control of mobile robot networks,

    Y . Kantaros and M. M. Zavlanos, “Distributed intermittent connectivity control of mobile robot networks,” IEEE Transactions on Automatic Control, vol. 62, no. 7, pp. 3109–3121, 2017

    2017

  2. [10]

    Persistent surveillance for unmanned aerial vehicles subject to charging and temporal logic constraints,

    K. Leahy, D. Zhou, C.-I. Vasile, K. Oikonomopoulos, M. Schwager, and C. Belta, “Persistent surveillance for unmanned aerial vehicles subject to charging and temporal logic constraints,” Autonomous Robots, vol. 40, no. 8, pp. 1363–1378, 2016

    2016

  3. [11]

    Baier and J.-P

    C. Baier and J.-P. Katoen, Principles of model checking . MIT press Cambridge, 2008, vol. 26202649

    2008

  4. [12]

    Temporal-logic-based reactive mission and motion planning,

    H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal-logic-based reactive mission and motion planning,” IEEE Transactions on Robotics, vol. 25, no. 6, pp. 1370–1381, 2009

    2009

  5. [13]

    Where’s waldo? sensor-based temporal logic motion planning,

    ——, “Where’s waldo? sensor-based temporal logic motion planning,” in Proceedings 2007 IEEE International Conference on Robotics and Automation. IEEE, 2007, pp. 3116–3121

    2007

  6. [14]

    Synthesis of distributed control and communication schemes from global ltl specifications,

    Y . Chen, X. C. Ding, and C. Belta, “Synthesis of distributed control and communication schemes from global ltl specifications,” in 2011 50th IEEE Conference on Decision and Control and European Control Conference. IEEE, 2011, pp. 2718–2723

    2011

  7. [15]

    Formal approach to the deployment of distributed robotic teams,

    Y . Chen, X. C. Ding, A. Stefanescu, and C. Belta, “Formal approach to the deployment of distributed robotic teams,” IEEE Transactions on Robotics, vol. 28, no. 1, pp. 158–171, 2012

    2012

  8. [16]

    E. M. Clarke, O. Grumberg, and D. Peled, Model checking. MIT press, 1999

    1999

  9. [17]

    Optimal path planning for surveillance with temporal-logic constraints,

    S. L. Smith, J. T ˚umov´a, C. Belta, and D. Rus, “Optimal path planning for surveillance with temporal-logic constraints,” The International Journal of Robotics Research , vol. 30, no. 14, pp. 1695–1708, 2011

    2011

  10. [18]

    Multi-agent plan reconfiguration under local ltl specifications,

    M. Guo and D. V . Dimarogonas, “Multi-agent plan reconfiguration under local ltl specifications,” The International Journal of Robotics Research, vol. 34, no. 2, pp. 218–235, 2015

    2015

  11. [19]

    Automatic deployment of distributed teams of robots from temporal logic motion specifications,

    M. Kloetzer and C. Belta, “Automatic deployment of distributed teams of robots from temporal logic motion specifications,” IEEE Transactions on Robotics, vol. 26, no. 1, pp. 48–61, 2010

    2010

  12. [20]

    Optimality and robustness in multi-robot path planning with temporal logic con- straints,

    A. Ulusoy, S. L. Smith, X. C. Ding, C. Belta, and D. Rus, “Optimality and robustness in multi-robot path planning with temporal logic con- straints,” The International Journal of Robotics Research, vol. 32, no. 8, pp. 889–911, 2013

    2013

  13. [21]

    Optimal multi-robot path planning with ltl constraints: guaranteeing correctness through synchronization,

    A. Ulusoy, S. L. Smith, and C. Belta, “Optimal multi-robot path planning with ltl constraints: guaranteeing correctness through synchronization,” in Distributed Autonomous Robotic Systems . Springer, 2014, pp. 337– 351

    2014

  14. [22]

    Composition of local potential functions for global robot control and navigation,

    D. C. Conner, A. A. Rizzi, and H. Choset, “Composition of local potential functions for global robot control and navigation,” in Proceed- ings 2003 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2003)(Cat. No. 03CH37453) , vol. 4. IEEE, 2003, pp. 3546–3551

    2003

  15. [23]

    Constructing decidable hybrid systems with velocity bounds,

    C. Belta and L. Habets, “Constructing decidable hybrid systems with velocity bounds,” in 2004 43rd IEEE Conference on Decision and Control (CDC)(IEEE Cat. No. 04CH37601) , vol. 1. IEEE, 2004, pp. 467–472

    2004

  16. [24]

    Discrete abstractions for robot motion planning and control in polygonal environments,

    C. Belta, V . Isler, and G. J. Pappas, “Discrete abstractions for robot motion planning and control in polygonal environments,” IEEE Trans- actions on Robotics , vol. 21, no. 5, pp. 864–874, 2005

    2005

  17. [25]

    Reachability analysis of multi-affine sys- tems,

    M. Kloetzer and C. Belta, “Reachability analysis of multi-affine sys- tems,” in International Workshop on Hybrid Systems: Computation and Control. Springer, 2006, pp. 348–362

    2006

  18. [26]

    Decentralized abstractions for multi-agent systems under coupled constraints,

    D. Boskos and D. V . Dimarogonas, “Decentralized abstractions for multi-agent systems under coupled constraints,” European Journal of Control, vol. 45, pp. 1–16, 2019

    2019

  19. [27]

    Intermittent connectivity control in mobile robot networks,

    Y . Kantaros and M. M. Zavlanos, “Intermittent connectivity control in mobile robot networks,” in 49th Asilomar Conference on Signals, Systems and Computers, Pacific Grove, CA, USA, November, 2015, pp. 1125–1129

    2015

  20. [28]

    Sampling-based control synthesis for multi-robot systems under global temporal specifications,

    ——, “Sampling-based control synthesis for multi-robot systems under global temporal specifications,” in 2017 ACM/IEEE 8th International Conference on Cyber-Physical Systems (ICCPS) . IEEE, 2017, pp. 3– 14

    2017

  21. [29]

    Sampling-based optimal control synthesis for multirobot systems under global temporal tasks,

    ——, “Sampling-based optimal control synthesis for multirobot systems under global temporal tasks,” IEEE Transactions on Automatic Control , vol. 64, no. 5, pp. 1916–1931, 2018

    1916

  22. [30]

    Temporal logic optimal control for large-scale multi-robot sys- tems: 10 400 states and beyond,

    ——, “Temporal logic optimal control for large-scale multi-robot sys- tems: 10 400 states and beyond,” in 2018 IEEE Conference on Decision and Control (CDC) . IEEE, 2018, pp. 2519–2524

    2018

  23. [31]

    Stylus*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,

    ——, “Stylus*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,” The International Journal of Robotics Research, vol. 39, no. 7, pp. 812–836, 2020

    2020

  24. [32]

    Transfer planning for temporal logic tasks,

    X. Luo and M. M. Zavlanos, “Transfer planning for temporal logic tasks,” in 2019 IEEE 58th Conference on Decision and Control (CDC) . IEEE, 2019, pp. 5306–5311

    2019

  25. [33]

    Distributed optimal control synthesis for multi-robot systems under global temporal tasks,

    Y . Kantaros and M. M. Zavlanos, “Distributed optimal control synthesis for multi-robot systems under global temporal tasks,” in Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems. IEEE Press, 2018, pp. 162–173

    2018

  26. [34]

    Control of magnetic microrobot teams for temporal micromanipulation tasks,

    Y . Kantaros, B. V . Johnson, S. Chowdhury, D. J. Cappelleri, and M. M. Zavlanos, “Control of magnetic microrobot teams for temporal micromanipulation tasks,” IEEE Transactions on Robotics , no. 99, pp. 1–18, 2018

    2018

  27. [35]

    Provably-correct coordination of large collections of agents with counting temporal logic constraints,

    Y . E. Sahin, P. Nilsson, and N. Ozay, “Provably-correct coordination of large collections of agents with counting temporal logic constraints,” in 2017 ACM/IEEE 8th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 2017, pp. 249–258

    2017

  28. [36]

    Linear temporal logic vehicle routing with applications to multi-uav mission planning,

    S. Karaman and E. Frazzoli, “Linear temporal logic vehicle routing with applications to multi-uav mission planning,” International Journal of Robust and Nonlinear Control , vol. 21, no. 12, pp. 1372–1395, 2011

    2011

  29. [37]

    Optimization-based trajec- tory generation with linear temporal logic specifications,

    E. M. Wolff, U. Topcu, and R. M. Murray, “Optimization-based trajec- tory generation with linear temporal logic specifications,” in 2014 IEEE International Conference on Robotics and Automation (ICRA) . IEEE, 2014, pp. 5319–5325

    2014

  30. [38]

    Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming,

    Y . Shoukry, P. Nuzzo, A. Balkan, I. Saha, A. L. Sangiovanni-Vincentelli, S. A. Seshia, G. J. Pappas, and P. Tabuada, “Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming,” in 2017 IEEE 56th Conference on Decisi...

    2017

  31. [39]

    Smc: Satisfiability modulo convex programming,

    Y . Shoukry, P. Nuzzo, A. L. Sangiovanni-Vincentelli, S. A. Seshia, G. J. Pappas, and P. Tabuada, “Smc: Satisfiability modulo convex programming,” Proceedings of the IEEE , vol. 106, no. 9, pp. 1655– 1679, 2018

    2018

  32. [40]

    Sampling-based motion planning with deterministicµ-calculus specifications,

    S. Karaman and E. Frazzoli, “Sampling-based motion planning with deterministicµ-calculus specifications,” in Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference. IEEE, 2009, pp. 2222–2229

    2009

  33. [41]

    Sampling-based algorithms for optimal motion planning with de- terministic µ-calculus specifications,

    ——, “Sampling-based algorithms for optimal motion planning with de- terministic µ-calculus specifications,” in American Control Conference (ACC), Montreal, Canada, June 2012, pp. 735–742

    2012

  34. [42]

    Sampling-based temporal logic path plan- ning,

    C. I. Vasile and C. Belta, “Sampling-based temporal logic path plan- ning,” in IEEE/RSJ International Conference on Intelligent Robots and Systems, Tokyo, Japan, November 2013, pp. 4817–4822

    2013

  35. [43]

    Sampling-based motion planning with temporal goals,

    A. Bhatia, L. E. Kavraki, and M. Y . Vardi, “Sampling-based motion planning with temporal goals,” in International Conference on Robotics and Automation (ICRA) , Anchorage, AL, May 2010, pp. 2689–2696

    2010

  36. [44]

    Towards manipulation planning with temporal logic specifications,

    K. He, M. Lahijanian, L. E. Kavraki, and M. Y . Vardi, “Towards manipulation planning with temporal logic specifications,” in IEEE International Conference on Robotics and Automation, ICRA 2015, Seattle, WA, USA, 26-30 May, 2015 , 2015, pp. 346–352

    2015

  37. [45]

    An automata-theoretic approach to automatic program verification,

    M. Y . Vardi and P. Wolper, “An automata-theoretic approach to automatic program verification,” in 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society, 1986

    1986

  38. [46]

    A fully automated framework for control of linear systems from temporal logic specifications,

    M. Kloetzer and C. Belta, “A fully automated framework for control of linear systems from temporal logic specifications,” IEEE Transactions on Automatic Control , vol. 53, no. 1, pp. 287–297, 2008

    2008

  39. [47]

    Revisiting the asymptotic optimality of rrt,

    K. Solovey, L. Janson, E. Schmerling, E. Frazzoli, and M. Pavone, “Revisiting the asymptotic optimality of rrt,” in2020 IEEE International Conference on Robotics and Automation (ICRA) . IEEE, 2020, pp. 2189–2195

    2020

  40. [48]

    Probabilistic planning with formal performance guarantees for mobile service robots,

    B. Lacerda, F. Faruq, D. Parker, and N. Hawes, “Probabilistic planning with formal performance guarantees for mobile service robots,” The International Journal of Robotics Research , vol. 38, no. 9, pp. 1098– 1123, 2019

    2019

  41. [49]

    Uniform-geometric distribution,

    Y . Akdo ˘gan, C. Kus ¸, A. Asgharzadeh, ˙I. Kınacı, and F. Sharafi, “Uniform-geometric distribution,” Journal of Statistical Computation and Simulation, vol. 86, no. 9, pp. 1754–1770, 2016

    2016

  42. [50]

    Global planning for multi-robot communication networks in complex environments,

    Y . Kantaros and M. M. Zavlanos, “Global planning for multi-robot communication networks in complex environments,” IEEE Transactions on Robotics, vol. 32, no. 5, pp. 1045–1061, 2016

    2016

  43. [51]

    A formal methods approach to interpretable reinforcement learning for robotic planning,

    X. Li, Z. Serlin, G. Yang, and C. Belta, “A formal methods approach to interpretable reinforcement learning for robotic planning,” Science Robotics, vol. 4, no. 37, 2019

    2019

  44. [52]

    Distributed state estimation using intermittently connected robot networks,

    R. Khodayi-mehr, Y . Kantaros, and M. M. Zavlanos, “Distributed state estimation using intermittently connected robot networks,” IEEE Transactions on Robotics , vol. 35, no. 3, pp. 709–724, 2019

    2019

  45. [53]

    Collision avoidance for per- sistent monitoring in multi-robot systems with intersecting trajectories,

    D. E. Soltero, S. L. Smith, and D. Rus, “Collision avoidance for per- sistent monitoring in multi-robot systems with intersecting trajectories,” in 2011 IEEE/RSJ International Conference on Intelligent Robots and Systems. IEEE, 2011, pp. 3645–3652

    2011

  46. [54]

    Collision and deadlock avoidance in multirobot systems: A distributed approach,

    Y . Zhou, H. Hu, Y . Liu, and Z. Ding, “Collision and deadlock avoidance in multirobot systems: A distributed approach,” IEEE Transactions on Systems, Man, and Cybernetics: Systems , vol. 47, no. 7, pp. 1712–1726, 2017

    2017

  47. [55]

    Van Kreveld, O

    M. Van Kreveld, O. Schwarzkopf, M. de Berg, and M. Overmars, Computational geometry algorithms and applications . Springer, 2000

    2000

  48. [56]

    Fast LTL to b ¨uchi automata translation,

    P. Gastin and D. Oddoux, “Fast LTL to b ¨uchi automata translation,” in International Conference on Computer Aided Verification . Springer, 2001, pp. 53–65

    2001

  49. [57]

    Monte carlo motion plan- ning for robot trajectory optimization under uncertainty,

    L. Janson, E. Schmerling, and M. Pavone, “Monte carlo motion plan- ning for robot trajectory optimization under uncertainty,” in Robotics Research. Springer, 2018, pp. 343–361

    2018

  50. [58]

    Z3: An efficient smt solver,

    L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in Inter- national conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2008, pp. 337–340

    2008

  51. [59]

    Linear encodings of bounded ltl model checking,

    A. Biere, K. Heljanko, T. Junttila, T. Latvala, and V . Schuppan, “Linear encodings of bounded ltl model checking,” arXiv preprint cs/0611029 , 2006

    2006 arXiv

  52. [60]

    Rudin, Real and complex analysis

    W. Rudin, Real and complex analysis . Tata McGraw-Hill Education, 2006

    2006

  53. [61]

    V oronoi diagrams—a survey of a fundamental geo- metric data structure,

    F. Aurenhammer, “V oronoi diagrams—a survey of a fundamental geo- metric data structure,” ACM Computing Surveys (CSUR), vol. 23, no. 3, pp. 345–405, 1991. APPENDIX A PROOF OF THEOREM 6.3 To prove completeness of TL-RRT ∗, we cannot directly adopt the proof for RRT [4] since in...

    1991

  54. [62]

    Specifically, letτ∗ be the optimal continuous path that optimizes (2)

    Construction of the product path pϵ: This step differs from [6], [47] in that here we build a product path that lives in the combined continuous and discrete state space. Specifically, letτ∗ be the optimal continuous path that optimizes (2). Since Problem 1 is robustly feasible...

  55. [63]

    Construction of the sequence of sets of balls {Bn}n∈N: This step differs from [6], [47] in that here we construct a set of balls along the product path pϵ instead of the continuous path τϵ. Specifically, given the product path pϵ, we define a set of Mn ballsBn = {Bn,1,..., Bn,Mn...

  56. [64]

    To do so, we need to show that eventually every ball in Bn contains at least one node of Gn

    Connecting nodes in consecutive balls in {Bn}n∈N: To prove the optimality of Gn, we show that a path exists in Gn that is arbitrarily close to pϵ. To do so, we need to show that eventually every ball in Bn contains at least one node of Gn. Given a sequence of uniformly sampled...

  57. [65]

    Furthermore, since x′ 2 is sampled before x′ 3, (R2) holds

    Then, since x′ 2 and x′ 3 are located in two consecutive balls and we have proved in step 2) that the distance between any states in any two consecutive balls is no more than rn(VT ), (R1) is satisfied. Furthermore, since x′ 2 is sampled before x′ 3, (R2) holds. Recall from ste...

  58. [66]

    Substituting in (26) we have that P(E1 n) converges to 1 as n→∞

    Thus, P(E1n|E2 n) approaches 0. Substituting in (26) we have that P(E1 n) converges to 1 as n→∞ . This guarantees that Gn will contain a path that approximates pϵ. The rest of the proof is similar to that in [47]. Essentially, we show that the probability of the event E3 n tha...

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.