{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T22:10:21Z","timestamp":1743199821745,"version":"3.40.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2012,5,26]],"date-time":"2012-05-26T00:00:00Z","timestamp":1337990400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1007\/s11432-012-4605-8","type":"journal-article","created":{"date-parts":[[2012,5,26]],"date-time":"2012-05-26T00:09:30Z","timestamp":1337990970000},"page":"1675-1692","source":"Crossref","is-referenced-by-count":11,"title":["A framework for multi-robot motion planning from temporal logic specifications"],"prefix":"10.1007","volume":"55","author":[{"given":"T. John","family":"Koo","sequence":"first","affiliation":[]},{"given":"RongQing","family":"Li","sequence":"additional","affiliation":[]},{"given":"Michael M.","family":"Quottrup","sequence":"additional","affiliation":[]},{"given":"Charles A.","family":"Clifton","sequence":"additional","affiliation":[]},{"given":"Roozbeh","family":"Izadi-Zamanabadi","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Bak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,5,26]]},"reference":[{"key":"4605_CR1","doi-asserted-by":"crossref","first-page":"926","DOI":"10.1109\/70.736776","volume":"14","author":"T. Balch","year":"1998","unstructured":"Balch T, Arkin R C. Behavior-based formation control for multirobot teams. IEEE Trans Robot Autom, 1998, 14: 926\u2013939","journal-title":"IEEE Trans Robot Autom"},{"key":"4605_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013162","DOI":"10.1109\/ROBOT.2001.932546"},{"key":"4605_CR3","doi-asserted-by":"crossref","first-page":"1466","DOI":"10.1109\/JPROC.2011.2160108","volume":"99","author":"R. A. Zachery","year":"2011","unstructured":"Zachery R A, Sastry S S, Kumar V. Special issue on swarming in natural and engineered systems. Proc IEEE, 2011, 99: 1466\u20131469","journal-title":"Proc IEEE"},{"key":"4605_CR4","doi-asserted-by":"crossref","unstructured":"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\u20133402","DOI":"10.1109\/ROBOT.2000.845244"},{"key":"4605_CR5","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1109\/100.667325","volume":"5","author":"R. Alami","year":"1998","unstructured":"Alami R, Fleury S, Herrb M, et al. Multi-robot cooperation in the MARTHA project. IEEE Robot Autom Mag, 1998, 5: 36\u201347","journal-title":"IEEE Robot Autom Mag"},{"key":"4605_CR6","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1109\/TRA.2002.803462","volume":"18","author":"B. P. Gerkey","year":"2002","unstructured":"Gerkey B P, Mataric M J. Sold: Auction methods for multirobot coordination. IEEE Trans Robot Autom, 2002, 18: 758\u2013768","journal-title":"IEEE Trans Robot Autom"},{"key":"4605_CR7","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0005-1098(01)00185-6","volume":"38","author":"M. Egerstedt","year":"2002","unstructured":"Egerstedt M, Hu X. A hybrid control approach to action coordination for mobile robots. Automatica, 2002, 38: 125\u2013130","journal-title":"Automatica"},{"key":"4605_CR8","first-page":"221","volume":"2","author":"M. Egerstedt","year":"2002","unstructured":"Egerstedt M, Martin C F. Conflict resolution for autonomous vehicles: A case study in hierarchical control design. Int J Hybrid Syst, 2002, 2: 221\u2013234","journal-title":"Int J Hybrid Syst"},{"key":"4605_CR9","unstructured":"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\u2013232"},{"key":"4605_CR10","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-45873-5_23","volume":"2289","author":"T. J. Koo","year":"2002","unstructured":"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\u2013293","journal-title":"Hybrid Systems: Computation and Control, Stanford, 2002"},{"key":"4605_CR11","unstructured":"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\u20131446"},{"key":"4605_CR12","unstructured":"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\u20134422"},{"key":"4605_CR13","doi-asserted-by":"crossref","unstructured":"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\u20132025","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"4605_CR14","doi-asserted-by":"crossref","first-page":"864","DOI":"10.1109\/TRO.2005.851359","volume":"21","author":"C. Belta","year":"2005","unstructured":"Belta C, Isler V, Pappas G J. Discrete abstractions for robot planning and control in polygonal environments. IEEE Trans Robot, 2005, 21: 864\u2013875","journal-title":"IEEE Trans Robot"},{"key":"4605_CR15","unstructured":"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\u20134890"},{"key":"4605_CR16","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/11730637_26","volume":"3927","author":"M. Kloetzer","year":"2006","unstructured":"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\u2013347","journal-title":"Hybrid Systems: Computation and Control, Santa Barbara, 2006"},{"key":"4605_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013583","DOI":"10.1109\/ICNSC.2006.1673210"},{"key":"4605_CR18","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/TRO.2009.2035776","volume":"26","author":"M. Kloetzer","year":"2010","unstructured":"Kloetzer M, Belta C. Automatic deployment of distributed teams of robots from temporal logic motion specifications. IEEE Trans Robot, 2010, 26: 48\u201361","journal-title":"IEEE Trans Robot"},{"key":"4605_CR19","unstructured":"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"},{"key":"4605_CR20","doi-asserted-by":"crossref","first-page":"1695","DOI":"10.1177\/0278364911417911","volume":"30","author":"S. L. Smith","year":"2011","unstructured":"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\u20131708","journal-title":"Int J Robot Res"},{"key":"4605_CR21","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/j.automatica.2008.08.008","volume":"45","author":"G. E. Fainekos","year":"2009","unstructured":"Fainekos G E, Girard A, Kress-Gazit H, et al. Temporal logic motion planning for dynamic robots. Automatica, 2009, 45: 343\u2013352","journal-title":"Automatica"},{"key":"4605_CR22","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge: The MIT Press, 1999"},{"key":"4605_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"McMillan K L. Symbolic Model Checking. Norwell: Kluwer Academic Publishers, 1993"},{"key":"4605_CR24","volume-title":"Getting started with SMV: User\u2019s manual","author":"K. L. McMillan","year":"1998","unstructured":"McMillan K L. Getting started with SMV: User\u2019s manual. Berkeley: Cadence Berkeley Laboratories, 1998"},{"key":"4605_CR25","doi-asserted-by":"crossref","first-page":"1401","DOI":"10.1109\/9.948467","volume":"46","author":"A. Chutinan","year":"2001","unstructured":"Chutinan A, Krogh B H. Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans Automat Contr, 2001, 46: 1401\u20131410","journal-title":"IEEE Trans Automat Contr"},{"key":"4605_CR26","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/11730637_38","volume":"3927","author":"A. Podelski","year":"2006","unstructured":"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\u2013521","journal-title":"Hybrid Systems: Computation and Control, Santa Barbara, 2006"},{"key":"4605_CR27","doi-asserted-by":"crossref","first-page":"2035","DOI":"10.1016\/j.automatica.2003.07.003","volume":"39","author":"G. J. Pappas","year":"2003","unstructured":"Pappas G J. Bisimilar linear systems. Automatica, 2003, 39: 2035\u20132047","journal-title":"Automatica"},{"key":"4605_CR28","unstructured":"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\u2013993"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-012-4605-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-012-4605-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-012-4605-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T21:46:14Z","timestamp":1743198374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-012-4605-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,26]]},"references-count":28,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["4605"],"URL":"https:\/\/doi.org\/10.1007\/s11432-012-4605-8","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"type":"print","value":"1674-733X"},{"type":"electronic","value":"1869-1919"}],"subject":[],"published":{"date-parts":[[2012,5,26]]}}}