{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,23]],"date-time":"2026-01-23T12:05:08Z","timestamp":1769169908855,"version":"3.49.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T00:00:00Z","timestamp":1558396800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T00:00:00Z","timestamp":1558396800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"crossref","award":["N66001-17-2-4058"],"award-info":[{"award-number":["N66001-17-2-4058"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Auton Robot"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s10514-019-09861-4","type":"journal-article","created":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T10:47:23Z","timestamp":1558522043000},"page":"585-600","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Automated synthesis of decentralized controllers for robot swarms from high-level temporal logic specifications"],"prefix":"10.1007","volume":"44","author":[{"given":"Salar","family":"Moarref","sequence":"first","affiliation":[]},{"given":"Hadas","family":"Kress-Gazit","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,21]]},"reference":[{"key":"9861_CR1","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1016\/j.ic.2018.02.021","volume":"261","author":"R Alur","year":"2018","unstructured":"Alur, R., Moarref, S., & Topcu, U. (2018). Compositional and symbolic synthesis of reactive controllers for multi-agent systems. Information and Computation, 261, 616\u2013633.","journal-title":"Information and Computation"},{"issue":"6","key":"9861_CR2","doi-asserted-by":"publisher","first-page":"825","DOI":"10.1007\/s00521-010-0382-8","volume":"19","author":"J Bachrach","year":"2010","unstructured":"Bachrach, J., Beal, J., & McLurkin, J. (2010). Composable continuous-space programs for robotic swarms. Neural Computing and Applications, 19(6), 825\u2013847.","journal-title":"Neural Computing and Applications"},{"key":"9861_CR3","doi-asserted-by":"crossref","unstructured":"Balch, T., & Hybinette, M. (2000). Social potentials for scalable multi-robot formations. In IEEE international conference on robotics and automation, 2000. Proceedings. ICRA\u201900 (Vol. 1, pp. 73\u201380). IEEE.","DOI":"10.1109\/ROBOT.2000.844042"},{"issue":"1","key":"9861_CR4","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-006-4341-z","volume":"28","author":"R Bloem","year":"2006","unstructured":"Bloem, R., Gabow, H. N., & Somenzi, F. (2006). An algorithm for strongly connected component analysis in n log n symbolic steps. Formal Methods in System Design, 28(1), 37\u201356.","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"9861_CR5","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., & Sa\u2019ar, Y. (2012). Synthesis of reactive (1) designs. Journal of Computer and System Sciences, 78(3), 911\u2013938.","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"9861_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11721-012-0075-2","volume":"7","author":"M Brambilla","year":"2013","unstructured":"Brambilla, M., Ferrante, E., Birattari, M., & Dorigo, M. (2013). Swarm robotics: A review from the swarm engineering perspective. Swarm Intelligence, 7(1), 1\u201341.","journal-title":"Swarm Intelligence"},{"issue":"3","key":"9861_CR7","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R. E. (1992). Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR), 24(3), 293\u2013318.","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"9861_CR8","unstructured":"Chen, J., Moarref, S., & Kress-Gazit, H. (2018). Verifiable control of robotic swarm from high-level specifications. In Proceedings of the 17th international conference on autonomous agents and multiagent systems (AAMAS 2018) (to appear)."},{"key":"9861_CR9","unstructured":"Church, A. (1962). Logic, arithmetic and automata. In Proceedings of the international congress of mathematicians (pp. 23\u201335)."},{"key":"9861_CR10","doi-asserted-by":"crossref","unstructured":"Claessen, K., Een, N., Sheeran, M., & Sorensson, N. (2008). Sat-solving in practice. In 9th international workshop on discrete event systems, 2008. WODES 2008 (pp. 61\u201367). IEEE.","DOI":"10.1109\/WODES.2008.4605923"},{"issue":"11","key":"9861_CR11","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E. M., Emerson, E. A., & Sifakis, J. (2009). Model checking: Algorithmic verification and debugging. Communications of the ACM, 52(11), 74\u201384.","journal-title":"Communications of the ACM"},{"issue":"11","key":"9861_CR12","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1016\/j.robot.2012.03.003","volume":"60","author":"C Dixon","year":"2012","unstructured":"Dixon, C., Winfield, A. F., Fisher, M., & Zeng, C. (2012). Towards temporal verification of swarm robotic systems. Robotics and Autonomous Systems, 60(11), 1429\u20131441.","journal-title":"Robotics and Autonomous Systems"},{"key":"9861_CR13","unstructured":"Ehlers, R. (2010). Symbolic bounded synthesis. In International conference on computer aided verification (pp. 365\u2013379). Berlin: Springer."},{"issue":"3","key":"9861_CR14","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E. A., & Clarke, E. M. (1982). Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3), 241\u2013266.","journal-title":"Science of Computer Programming"},{"issue":"3","key":"9861_CR15","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10703-011-0115-3","volume":"39","author":"E Filiot","year":"2011","unstructured":"Filiot, E., Jin, N., & Raskin, J. F. (2011). Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design, 39(3), 261\u2013296.","journal-title":"Formal Methods in System Design"},{"key":"9861_CR16","doi-asserted-by":"crossref","unstructured":"Filippidis, I., Dimarogonas, D. V., & Kyriakopoulos, K. J. (2012). Decentralized multi-agent control from local LTL specifications. In 2012 IEEE 51st annual conference on decision and control (CDC) (pp. 6235\u20136240). IEEE.","DOI":"10.1109\/CDC.2012.6426027"},{"key":"9861_CR17","unstructured":"Gjondrekaj, E., Loreti, M., Pugliese, R., Tiezzi, F., Pinciroli, C., Brambilla, M., Birattari, M., & Dorigo, M. (2012). Towards a formal verification methodology for collective robotic systems. In Formal methods and software engineering (pp. 54\u201370). Berlin: Springer."},{"key":"9861_CR18","volume-title":"Genetic algorithms in search, optimization, and machine learning","author":"DE Goldberg","year":"1989","unstructured":"Goldberg, D. E. (1989). Genetic algorithms in search, optimization, and machine learning. Reading: Addison-Wesley."},{"issue":"2","key":"9861_CR19","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1177\/0278364914546174","volume":"34","author":"M Guo","year":"2015","unstructured":"Guo, M., & Dimarogonas, D. V. (2015). Multi-agent plan reconfiguration under local LTL specifications. The International Journal of Robotics Research, 34(2), 218\u2013235.","journal-title":"The International Journal of Robotics Research"},{"key":"9861_CR20","doi-asserted-by":"crossref","unstructured":"Guo, M., Tumova, J., & Dimarogonas, D. V. (2014). Cooperative decentralized multi-agent control under local LTL tasks and connectivity constraints. In 2014 IEEE 53rd annual conference on decision and control (CDC) (pp. 75\u201380). IEEE.","DOI":"10.1109\/CDC.2014.7039362"},{"key":"9861_CR21","doi-asserted-by":"crossref","unstructured":"Karaman, S., & Frazzoli, E. (2008). Vehicle routing with linear temporal logic specifications: Applications to multi-UAV mission planning. In AIAA guidance, navigation and control conference and exhibit (p. 6838).","DOI":"10.2514\/6.2008-6838"},{"key":"9861_CR22","volume-title":"Algorithm design","author":"J Kleinberg","year":"2006","unstructured":"Kleinberg, J., & Tardos, E. (2006). Algorithm design. London: Pearson Education India."},{"key":"9861_CR23","doi-asserted-by":"crossref","unstructured":"Kloetzer, M., & Belta, C. (2006). Hierarchical abstractions for robotic swarms. In Proceedings 2006 IEEE international conference on robotics and automation, 2006. ICRA 2006 (pp. 952\u2013957). IEEE.","DOI":"10.1109\/ROBOT.2006.1641832"},{"key":"9861_CR24","doi-asserted-by":"crossref","unstructured":"Kloetzer, M., Ding, X. C., & Belta, C. (2011). Multi-robot deployment from LTL specifications with reduced communication. In 2011 50th IEEE conference on decision and control and European control conference (CDC-ECC) (pp. 4867\u20134872). IEEE.","DOI":"10.1109\/CDC.2011.6160478"},{"issue":"1","key":"9861_CR25","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1152934.1152936","volume":"1","author":"TH Labella","year":"2006","unstructured":"Labella, T. H., Dorigo, M., & Deneubourg, J. L. (2006). Division of labor in a group of robots inspired by ants\u2019 foraging behavior. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 1(1), 4\u201325.","journal-title":"ACM Transactions on Autonomous and Adaptive Systems (TAAS)"},{"key":"9861_CR26","doi-asserted-by":"crossref","unstructured":"Loizou, S. G., & Kyriakopoulos, K. J. (2005). Automated planning of motion tasks for multi-robot systems. In 44th IEEE conference on decision and control, 2005 and 2005 European control conference. CDC-ECC\u201905 (pp. 78\u201383). IEEE.","DOI":"10.1109\/CDC.2005.1582134"},{"issue":"1","key":"9861_CR27","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., & Wolper, P. (1984). Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 6(1), 68\u201393.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"9861_CR28","doi-asserted-by":"crossref","unstructured":"Moarref, S., & Kress-Gazit, H. (2017). Decentralized control of robotic swarms from high-level temporal logic specifications. In 2017 international symposium on multi-robot and multi-agent systems (MRS) (pp. 17\u201323). IEEE.","DOI":"10.1109\/MRS.2017.8250926"},{"key":"9861_CR29","unstructured":"Nilsson, P., & Ozay, N. (2016). Control synthesis for large collections of systems with mode-counting constraints. In Proceedings of the 19th international conference on hybrid systems: Computation and control (pp. 205\u2013214). ACM."},{"issue":"1","key":"9861_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11721-007-0009-6","volume":"2","author":"S Nouyan","year":"2008","unstructured":"Nouyan, S., Campo, A., & Dorigo, M. (2008). Path formation in a robot swarm. Swarm Intelligence, 2(1), 1\u201323.","journal-title":"Swarm Intelligence"},{"issue":"3","key":"9861_CR31","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s10458-005-2631-2","volume":"11","author":"L Panait","year":"2005","unstructured":"Panait, L., & Luke, S. (2005). Cooperative multi-agent learning: The state of the art. Autonomous Agents and Multi-agent Systems, 11(3), 387\u2013434.","journal-title":"Autonomous Agents and Multi-agent Systems"},{"key":"9861_CR32","unstructured":"Pickem, D., Glotfelter, P., Wang, L., Mote, M., Ames, A., Feron, E., & Egerstedt, M. (2016). The robotarium: A remotely accessible swarm robotics research testbed. arXiv preprint \narXiv:1609.04730\n\n."},{"key":"9861_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A., & Rosner, R. (1989). On the synthesis of a reactive module. In Proceedings of the 16th ACM symposium on principles of programming languages (pp. 179\u2013190). ACM.","DOI":"10.1145\/75277.75293"},{"key":"9861_CR34","doi-asserted-by":"crossref","unstructured":"Raman, V., & Kress-Gazit, H. (2014). Synthesis for multi-robot controllers with interleaved motion. In 2014 IEEE international conference on robotics and automation (ICRA) (pp. 4316\u20134321). IEEE.","DOI":"10.1109\/ICRA.2014.6907487"},{"issue":"3","key":"9861_CR35","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1109\/TRO.2015.2414134","volume":"31","author":"V Raman","year":"2015","unstructured":"Raman, V., Piterman, N., Finucane, C., & Kress-Gazit, H. (2015). Timing semantics for abstraction and execution of synthesized high-level robot control. IEEE Transactions on Robotics, 31(3), 591\u2013604.","journal-title":"IEEE Transactions on Robotics"},{"key":"9861_CR36","unstructured":"Rosner, R. (1992). Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science."},{"key":"9861_CR37","doi-asserted-by":"crossref","unstructured":"Soysal, O., & Sahin, E. (2005). Probabilistic aggregation strategies in swarm robotic systems. In Swarm intelligence symposium, 2005. SIS 2005. Proceedings 2005 IEEE (pp. 325\u2013332). IEEE.","DOI":"10.1109\/SIS.2005.1501639"},{"key":"9861_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and control of hybrid systems: A symbolic approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P. (2009). Verification and control of hybrid systems: A symbolic approach. Berlin: Springer."},{"issue":"8","key":"9861_CR39","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1177\/0278364913487931","volume":"32","author":"A Ulusoy","year":"2013","unstructured":"Ulusoy, A., Smith, S. L., Ding, X. C., Belta, C., & Rus, D. (2013). Optimality and robustness in multi-robot path planning with temporal logic constraints. The International Journal of Robotics Research, 32(8), 889\u2013911.","journal-title":"The International Journal of Robotics Research"},{"key":"9861_CR40","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., & Yorsh, G. (2010). Abstraction-guided synthesis of synchronization. In ACM Sigplan notices (Vol. 45, pp. 327\u2013338). ACM.","DOI":"10.1145\/1707801.1706338"}],"container-title":["Autonomous Robots"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10514-019-09861-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10514-019-09861-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10514-019-09861-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T23:10:52Z","timestamp":1589929852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10514-019-09861-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,21]]},"references-count":40,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["9861"],"URL":"https:\/\/doi.org\/10.1007\/s10514-019-09861-4","relation":{},"ISSN":["0929-5593","1573-7527"],"issn-type":[{"value":"0929-5593","type":"print"},{"value":"1573-7527","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,5,21]]},"assertion":[{"value":"7 May 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 May 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 May 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}