Sage Journals: Discover world-class research

Abstract

In this paper we present a method for automatic planning of optimal paths for a group of robots that satisfy a common high-level mission specification. The motion of each robot is modeled as a weighted transition system, and the mission is given as a linear temporal logic (LTL) formula over a set of propositions satisfied at the regions of the environment. In addition, an optimizing proposition must repeatedly be satisfied. The goal is to minimize a cost function that captures the maximum time between successive satisfactions of the optimizing proposition while guaranteeing that the formula is satisfied. When the robots can follow a given trajectory exactly, our method computes a set of optimal satisfying paths that minimize the cost function and satisfy the LTL formula. However, if the traveling times of the robots are uncertain, then the robots may not be able to follow a given trajectory exactly, possibly violating the LTL formula during deployment. We handle such cases by leveraging the communication capabilities of the robots to guarantee correctness during deployment and provide bounds on the deviation from the optimal values. We implement and experimentally evaluate our method for various persistent surveillance tasks in a road network environment.

Keywords

optimal path planning optimal multi-robot path planning temporal logic formal methods

Get full access to this article

View all access options for this article.

References

Baier

Katoen

(2008) Principles of Model Checking. Cambridge, MA: MIT Press.

Bianco

de Alfaro

(1995) Model checking of probabilistic and nondeterministic systems. In: Foundations of Software Technology and Theoretical Computer Science ( Lecture Notes in Computer Science, vol. 1026). Berlin: Springer, pp. 499–513.

Chen

Ding

Belta

(2011) Synthesis of distributed control and communication schemes from global LTL specifications. In: 2011 IEEE Conference on Decision and Control (CDC 2011), Orlando, FL, pp. 2718–2723.

Chen

Ding

Stefanescu

Belta

(2012) A formal approach to the deployment of distributed robotic teams. IEEE Transactions on Robotics 28(1): 158–171.

Choset

Lynch

Hutchinson

. (2005) Principles of Robot Motion - Theory, Algorithms, and Implementations. Cambridge, MA: MIT Press.

Clarke

Peled

Grumberg

(1999) Model checking. Cambridge, MA: MIT Press.

Ding

Smith

Belta

Rus

(2011) MDP optimal control under temporal logic constraints. In: 2011 IEEE Conference on Decision and Control (CDC 2011), Orlando, FL, pp. 532–538.

Gastin

Oddoux

(2001) Fast LTL to Büchi automata translation. In: CAV ′01 Proceedings of the 13th International Conference on Computer Aided Verification (Lecture Notes in Computer Science, vol. 2102). Berlin: Springer, pp. 53–65.

Hagberg

Schult

Swart

(2008) Exploring network structure, dynamics, and function using NetworkX. In: Proceedings of the 7th Python in Science Conference (SciPy2008), Pasadena, CA, pp. 11–15.

10.

Hopcroft

Motwani

Ullman

(2007) Introduction to Automata Theory, Languages, and Computation. Reading, MA: Addison-Wesley.

11.

Karaman

Frazzoli

(2008a) Complex mission optimization for multiple-UAVs using linear temporal logic. In: American Control Conference, Seattle, WA, pp. 2003–2009.

12.

Karaman

Frazzoli

(2008b) Vehicle routing problem with metric temporal logic specifications. In: IEEE Conference on Decision and Control, Cancún, México, pp. 3953–3958.

13.

Kavraki

Svestka

Latombe

Overmars

(1996) Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Transactions on Robotics and Automation 12(4): 566–580.

14.

Kloetzer

Belta

(2008) Dealing with non-determinism in symbolic control. In: Egerstedt

Mishra

(eds.), Hybrid Systems: Computation and Control: 11th International Workshop ( Lecture Notes in Computer Science, vol. 4981). Berlin: Springer, pp. 287–300.

15.

Kloetzer

Belta

(2010) Automatic deployment of distributed teams of robots from temporal logic specifications. IEEE Transactions on Robotics 26(1): 48–61.

16.

Kress-Gazit

Fainekos

Pappas

(2007) Where’s Waldo? Sensor-based temporal logic motion planning. In: IEEE International Conference Robotics and Automation, pp. 3116–3121.

17.

Kress-Gazit

Wongpiromsarn

Topcu

(2011) Correct, reactive robot control from abstraction and temporal logic specifications. IEEE Robotics & Automation Magazine 18: 65–74.

18.

Kuffner

LaValle

(2000) Rrt-connect: An efficient approach to single-query path planning. In: IEEE International Conference Robotics and Automation, pp. 995–1001.

19.

Kwiatkowska

Norman

Parker

(2002) Probabilistic symbolic model checking with PRISM: A hybrid approach. In: International Journal on Software Tools for Technology Transfer 6(2): 52–66.

20.

LaValle

(2006) Planning Algorithms. Cambridge: Cambridge University Press.

21.

Lozano-Perez

(1983) Spatial planning: A configuration space approach. IEEE Transactions on Computers 32(2): 108–120.

22.

Peled

Wilke

Wolper

(1998) An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages. Theoretical Computer Science 195(2): 183–203.

23.

Quottrup

Bak

Izadi-Zamanabadi

(2004) Multi-robot motion planning: A timed automata approach. In: IEEE International Conference Robotics and Automation, New Orleans, LA, pp. 4417–4422.

24.

Rimon

Koditschek

(1992) Exact robot navigation using artificial potential functions. IEEE Transactions on Robotics and Automation 8(5): 501–518.

25.

Sistla

Clarke

(1985) The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery 32(3): 733–749.

26.

Smith

Tůmová

Belta

Rus

(2011) Optimal path planning for surveillance with temporal logic constraints. The International Journal of Robotics Research 30(14): 1695–1708.

27.

Tabuada

Pappas

(2006) Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control 51(12): 1862–1877.

28.

Thomas

(2002) Infinite games and verification. In: Proceedings of CAV, pp. 58–64.

29.

Toth

Vigo

(eds.) (2001) The Vehicle Routing Problem ( Monographs on Discrete Mathematics and Applications). Philadelphia, PA: SIAM.

30.

Ulusoy

Smith

Belta

(2012a) Optimal multi-robot path planning with LTL constraints: Guaranteeing correctness through synchronization. In: International Symposium on Distributed and Autonomous Robotic Systems, Baltimore, MD, USA.

31.

Ulusoy

Smith

Ding

Belta

(2012b) Robust multi-robot optimal path planning with temporal logic constraints. In: IEEE International Conference Robotics and Automation, St. Paul, MN, USA, pp. 4693–4698.

32.

Ulusoy

Smith

Ding

Belta

Rus

(2011) Optimal multi-robot path planning with temporal logic constraints. In: IEEE/RSJ International Conference Intelligent Robots and Systems, San Francisco, CA, pp. 3087–3092.

33.

Yordanov

Tumova

Cerna

Barnat

Belta

(2012) Temporal logic control of discrete-time piecewise affine systems. IEEE Transactions on Automatic Control 57(6): 1491–1504.

Supplementary Material

Please find the following supplemental material available below.

For Open Access articles published under a Creative Commons License, all supplemental material carries the same license as the article it is associated with.

For non-Open Access articles published, all supplemental material carries a non-exclusive license, and permission requests for re-use of supplemental material or any part of supplemental material shall be sent directly to the copyright owner as specified in the copyright notice associated with the article.

0.00 MB

Optimality and Robustness in Multi-Robot Path Planning with Temporal Logic Constraints

Abstract

Keywords

Get full access to this article

References

Supplementary Material