#### DMCA

## Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints

### Citations

1645 |
The temporal logic of programs
- Pnueli
- 1977
(Show Context)
Citation Context ...such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], [3], [4], [5], [6], [7], [8]. We have chosen LTL =-=[9]-=-, [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly survey regions A and B while avoiding dangerous reg... |

1130 | Planning Algorithms
- LaValle
(Show Context)
Citation Context ... checking. We demonstrate the utilization and benefits of the suggested framework in an illustrative example. I. INTRODUCTION In this paper, we consider the problem of robot path planning (see, e.g., =-=[1]-=- for an overview) with more complex missions than ”Go from A to B while avoiding obstacles.”. Recently, different versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Log... |

420 |
Principles of Model Checking
- Baier, Katoen
- 2008
(Show Context)
Citation Context ...as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], [3], [4], [5], [6], [7], [8]. We have chosen LTL [9], =-=[10]-=- as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly survey regions A and B while avoiding dangerous regions. ... |

180 | Fast LTL to Buchi automata translation.
- Gastin, Oddoux
- 2001
(Show Context)
Citation Context ...nstraints, requestresponse properties, and safety properties are allowed. Complexity: The size of a BA for an LTL formula φ is 2O(|φ|) in the worst case, where |φ| denotes the length of the formula φ =-=[15]-=-. However, note that the actual size of the BA is in practice often quite small. The size of the product automaton P is O(|Q|·2O(|φ|)). A simple modification of the Floyd-Warshall algorithm is employe... |

145 | A fully automated framework for control of linear systems from temporal logic specifications
- Kloetzer, Belta
- 2008
(Show Context)
Citation Context ...tly, different versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], [3], =-=[4]-=-, [5], [6], [7], [8]. We have chosen LTL [9], [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly survey ... |

51 | Temporal logic motion planning for dynamic robots,
- Fainekos, Girard, et al.
- 2009
(Show Context)
Citation Context ...versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], [3], [4], [5], [6], =-=[7]-=-, [8]. We have chosen LTL [9], [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly survey regions A and B... |

48 |
Sampling-based motion planning with deterministic µ-calculus specifications.
- Karaman, Frazzoli
- 2009
(Show Context)
Citation Context ...different versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], [3], [4], =-=[5]-=-, [6], [7], [8]. We have chosen LTL [9], [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly survey regio... |

37 | Receding horizon temporal logic planning for dynamical systems
- Wongpiromsarn, Topcu, et al.
(Show Context)
Citation Context ...rol. In this work, we focus on interconnecting the receding horizon control with the synthesis of a path that is provably correct with respect to a given temporal logic formula. This idea appeared in =-=[12]-=-, [13], where the receding horizon approach was employed to fight the high computational complexity of reactive motion planning with a specification in GR(1) fragment of LTL. However, the authors did ... |

31 | Discrete event models + temporal logic = supervisory controller: Automatic synthesis of locomotion controllers,”
- Antoniotti, Mishra
- 1995
(Show Context)
Citation Context ...s.”. Recently, different versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions =-=[2]-=-, [3], [4], [5], [6], [7], [8]. We have chosen LTL [9], [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeated... |

19 | Temporal logicbased reactive mission and motion planning,”
- Kress-Gazit, Fainekos, et al.
- 2009
(Show Context)
Citation Context ...rent versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], [3], [4], [5], =-=[6]-=-, [7], [8]. We have chosen LTL [9], [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly survey regions A ... |

19 | LTL Robot Motion Control based on Automata Learning of Environmental Dynamics,”
- Chen, Tumova, et al.
- 2012
(Show Context)
Citation Context ...that all the transitions leading to an accepting states are labeled with a set containing pisur, is used in the product automaton construction. For instance, a surveillance fragment of LTL defined in =-=[17]-=- guarantees existence of such a BA. The fragment includes LTL formulas that require to repeatedly visit a surveillance proposition pisur (called an optimizing proposition in [17]) and to visit a given... |

7 |
ltl2dstar - LTL to deterministic Streett and Rabin automata.
- Klein
- 2007
(Show Context)
Citation Context ...phabet 2Π accepting all and only the words satisfying formula φ. Algorithms for translation of an LTL formula into a corresponding Büchi automaton were proposed [15], and several tools are available =-=[16]-=-. Definition 4 (Weighted Product Automaton): A weighted product automaton between a TS T = (Q, q0, T,Π, L,W ) and a BA Bφ = (S, s0, 2Π, δ, F ) is a tuple P = T × Bφ = (SP , sP0, δP , FP ,WP), where • ... |

6 |
Cassandras, “Receding horizon surveillance with temporal logic specifications
- Ding, Belta, et al.
- 2010
(Show Context)
Citation Context ...ational complexity of reactive motion planning with a specification in GR(1) fragment of LTL. However, the authors did not consider any rewards collection to be optimized. In contrast, the authors in =-=[14]-=- addressed a similar problem that we do. They assumed a deterministic weighted transition system with locally sensed rewards changing according to an unknown dynamics. While they required the satisfac... |

1 |
Automatic Synthesis of Multiagent Motion
- Loizou, Kyriakopoulos
(Show Context)
Citation Context ...Recently, different versions of temporal logics, such as Linear Temporal Logic (LTL), Computation Tree Logic (CTL), or µ-calculus have been successfully employed to specify such robotic missions [2], =-=[3]-=-, [4], [5], [6], [7], [8]. We have chosen LTL [9], [10] as the specification means for its resemblance to natural language and its ability to express interesting robot behavior, such as ”Repeatedly su... |

1 |
Simulation of attraction-based approach to receding horizon control with LTL specification. [Online]. Available: http://www.fi.muni.cz/$\ sim$x175388/simulationLTLrhc
- Svorenova, Tumova, et al.
- 2012
(Show Context)
Citation Context ... online planning algorithm would be in O(d·dh) per iteration. V. EXAMPLE We implemented the framework with several concrete choices of the state potential and the preference function in a Java applet =-=[18]-=-. In this section, we report on simulation results to illustrate employment of our approach. We consider a data gathering robot in a grid-like partitioned environment modeled as a TS depicted in Fig. ... |