# zbMATH — the first resource for mathematics

##### Examples
 Geometry Search for the term Geometry in any field. Queries are case-independent. Funct* Wildcard queries are specified by * (e.g. functions, functorial, etc.). Otherwise the search is exact. "Topological group" Phrases (multi-words) should be set in "straight quotation marks". au: Bourbaki & ti: Algebra Search for author and title. The and-operator & is default and can be omitted. Chebyshev | Tschebyscheff The or-operator | allows to search for Chebyshev or Tschebyscheff. "Quasi* map*" py: 1989 The resulting documents have publication year 1989. so: Eur* J* Mat* Soc* cc: 14 Search for publications in a particular source with a Mathematics Subject Classification code (cc) in 14. "Partial diff* eq*" ! elliptic The not-operator ! eliminates all results containing the word elliptic. dt: b & au: Hilbert The document type is set to books; alternatively: j for journal articles, a for book articles. py: 2000-2015 cc: (94A | 11T) Number ranges are accepted. Terms can be grouped within (parentheses). la: chinese Find documents in a given language. ISO 639-1 language codes can also be used.

##### Operators
 a & b logic and a | b logic or !ab logic not abc* right wildcard "ab c" phrase (ab c) parentheses
##### Fields
 any anywhere an internal document identifier au author, editor ai internal author identifier ti title la language so source ab review, abstract py publication year rv reviewer cc MSC code ut uncontrolled term dt document type (j: journal article; b: book; a: book article)
A framework for multi-robot motion planning from temporal logic specifications. (English) Zbl 1245.68227
Summary: We propose a framework for the coordination of a network of robots with respect to formal requirement specifications expressed in temporal logics. A regular tessellation is used to partition the space of interest into a union of disjoint regular and equal cells with finite facets, and each cell can only be occupied by a robot or an obstacle. Each robot is assumed to be equipped with a finite collection of continuous-time nonlinear closed-loop dynamics to be operated in. The robot is then modeled as a hybrid automaton for capturing the finitely many modes of operation for either staying within the current cell or reaching an adjacent cell through the corresponding facet. By taking the motion capabilities into account, a bisimilar discrete abstraction of the hybrid automaton can be constructed. Having the two systems bisimilar, all properties that are expressible in temporal logics such as linear-time temporal logic, computation tree logic, and $\mu$-calculus can be preserved. Motion planning can then be performed at a discrete level by considering the parallel composition of discrete abstractions of the robots with a requirement specification given in a suitable temporal logic. The bisimilarity ensures that the discrete planning solutions are executable by the robots. For demonstration purposes, a finite automaton is used as the abstraction and the requirement specification is expressed in computation tree logic. The model checker Cadence SMV is used to generate coordinated verified motion planning solutions. Two autonomous aerial robots are used to demonstrate how the proposed framework may be applied to solve coordinated motion planning problems.
##### MSC:
 68T40 Robotics (AI aspects) 68T20 AI problem solving (heuristics, search strategies, etc.) 68T27 Logic in artificial intelligence 68Q60 Specification and verification of programs
Cadence SMV
##### References:
 [1] Balch T, Arkin R C. Behavior-based formation control for multirobot teams. IEEE Trans Robot Autom, 1998, 14: 926–939 · doi:10.1109/70.736776 [2] Fierro R, Das A K, Kumar V, et al. Hybrid control of formations of robots. In: Proceedings of the 2001 IEEE International Conference on Robotics and Automation, Shanghai, 2001. 157–162 [3] Zachery R A, Sastry S S, Kumar V. Special issue on swarming in natural and engineered systems. Proc IEEE, 2011, 99: 1466–1469 · doi:10.1109/JPROC.2011.2160108 [4] Klavins E, Koditschek D E. A formalism for the composition of concurrent robot rehaviors. In: Proceedings of the 2000 IEEE International Conference on Robotics and Automation, San Francisco, 2000. 3395–3402 [5] Alami R, Fleury S, Herrb M, et al. Multi-robot cooperation in the MARTHA project. IEEE Robot Autom Mag, 1998, 5: 36–47 · doi:10.1109/100.667325 [6] Gerkey B P, Mataric M J. Sold: Auction methods for multirobot coordination. IEEE Trans Robot Autom, 2002, 18: 758–768 · doi:10.1109/TRA.2002.803462 [7] Egerstedt M, Hu X. A hybrid control approach to action coordination for mobile robots. Automatica, 2002, 38: 125–130 · Zbl 0997.93074 · doi:10.1016/S0005-1098(01)00185-6 [8] Egerstedt M, Martin C F. Conflict resolution for autonomous vehicles: A case study in hierarchical control design. Int J Hybrid Syst, 2002, 2: 221–234 [9] Alur R, Esposito J, Kim M, et al. Formal modeling and analysis of hybrid systems: A case study in multi-robot coordination. In: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, 1999. Goos G, Hartmanis J, Van Leeuwen J, eds. Lecture Notes in Computer Science, 1999, 1708: 212–232 [10] Koo T J, Sastry S. Bisimulation based hierarchical system architecture for single-agent multi-modal systems. In: Hybrid Systems: Computation and Control, Stanford, 2002. Lecture Notes in Computer Science, 2002, 2289: 281–293 · doi:10.1007/3-540-45873-5_23 [11] Antoniotti M, Mishra B. Discrete event models + temporal logic = supervisory controller: Automatic synthesis of locomotion controllers. In: Proceedings of the 1995 IEEE Conference on Robotics & Automation, Nagoya, 1995. 1441–1446 [12] Quottrup M M, Bak T, Izadi-Zamanabadi R. Multi-robot planning: A timed automata approach. In: Proceedings of the 2004 IEEE International Conference on Robotics & Automation, Barcelona, 2004. 4417–4422 [13] Fainekos G E, Kress-Gazit H, Pappas G J. Temporal logic motion planning for mobile robots. In: Proceedings of the 2005 IEEE International Conference on Robotics and Automation, Barcelona, 2005. 2020–2025 [14] Belta C, Isler V, Pappas G J. Discrete abstractions for robot planning and control in polygonal environments. IEEE Trans Robot, 2005, 21: 864–875 · doi:10.1109/TRO.2005.851359 [15] Fainekos G E, Kress-Gazit H, Pappas G J. Hybrid controllers for path planning: A temporal logic approach. In: Proceedings of the 2005 IEEE Conference on Decision and Control and the European Control Conference, Seville, 2005. 4885–4890 [16] Kloetzer M, Belta C. A fully automated framework for Control of linear systems from LTL specifications. In: Hybrid Systems: Computation and Control, Santa Barbara, 2006. Lecture Notes in Computer Science, 2006, 3927: 333–347 [17] Kloetzer M, Belta C. LTL planning for groups of robots. In: Proceedings of the 2006 IEEE International Conference on Networking, Sensing, and Control, Ft. Lauderdale, 2006. 578–583 [18] Kloetzer M, Belta C. Automatic deployment of distributed teams of robots from temporal logic motion specifications. IEEE Trans Robot, 2010, 26: 48–61 · doi:10.1109/TRO.2009.2035776 [19] Chen Y, Ding X C, Stefanescu A, et al. A formal approach to deployment of robotic teams in an urban-like environment. In: Proceedings of the 10th International Symposium on Distributed Autonomous Robotics Systems (DARS), Lausanne, 2010 [20] Smith S L, Tumova J, Belta C, et al. Optimal path planning for surveillance with temporal-logic constraints. Int J Robot Res, 2011, 30: 1695–1708 · doi:10.1177/0278364911417911 [21] Fainekos G E, Girard A, Kress-Gazit H, et al. Temporal logic motion planning for dynamic robots. Automatica, 2009, 45: 343–352 · Zbl 1158.93369 · doi:10.1016/j.automatica.2008.08.008 [22] Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge: The MIT Press, 1999 [23] McMillan K L. Symbolic Model Checking. Norwell: Kluwer Academic Publishers, 1993 [24] McMillan K L. Getting started with SMV: User’s manual. Berkeley: Cadence Berkeley Laboratories, 1998 [25] Chutinan A, Krogh B H. Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans Automat Contr, 2001, 46: 1401–1410 · Zbl 1031.93123 · doi:10.1109/9.948467 [26] Podelski A, Wagner S. Model checking of hybrid systems: from reachability towards stability. In: Hybrid Systems: Computation and Control, Santa Barbara, 2006. Lecture Notes in Computer Science, 2006, 3927: 507–521 [27] Pappas G J. Bisimilar linear systems. Automatica, 2003, 39: 2035–2047 · Zbl 1045.93033 · doi:10.1016/j.automatica.2003.07.003 [28] Koo T J, Clifton C A, Hemingway G. Cascaded control design for a quadrotor aerial robot. In: Proceedings of the 2006 Asian Control Conference, Bali, 2006. 989–993