{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:08Z","timestamp":1740099128663,"version":"3.37.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030001506"},{"type":"electronic","value":"9783030001513"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00151-3_5","type":"book-chapter","created":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T09:54:31Z","timestamp":1535190871000},"page":"71-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Reactive Synthesis for Robotic Swarms"],"prefix":"10.1007","author":[{"given":"Salar","family":"Moarref","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hadas","family":"Kress-Gazit","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,26]]},"reference":[{"issue":"3","key":"5_CR1","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.: Timing semantics for abstraction and execution of synthesized high-level robot control. IEEE Trans. Robot. 31(3), 591\u2013604 (2015)","journal-title":"IEEE Trans. Robot."},{"issue":"1","key":"5_CR2","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.: Swarm robotics: a review from the swarm engineering perspective. Swarm Intell. 7(1), 1\u201341 (2013)","journal-title":"Swarm Intell."},{"issue":"1","key":"5_CR3","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.: Path formation in a robot swarm. Swarm Intell. 2(1), 1\u201323 (2008)","journal-title":"Swarm Intell."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Soysal, O., Sahin, E.: Probabilistic aggregation strategies in swarm robotic systems. In: Proceedings 2005 IEEE Swarm Intelligence Symposium, SIS 2005, pp. 325\u2013332. IEEE (2005)","DOI":"10.1109\/SIS.2005.1501639"},{"issue":"1","key":"5_CR5","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.: Division of labor in a group of robots inspired by ants\u2019 foraging behavior. ACM Trans. Auton. Adapt. Syst. (TAAS) 1(1), 4\u201325 (2006)","journal-title":"ACM Trans. Auton. Adapt. Syst. (TAAS)"},{"issue":"6","key":"5_CR6","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.: Composable continuous-space programs for robotic swarms. Neural Comput. Appl. 19(6), 825\u2013847 (2010)","journal-title":"Neural Comput. Appl."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Balch, T., Hybinette, M.: Social potentials for scalable multi-robot formations. In: IEEE International Conference on Robotics and Automation 2000. Proceedings of ICRA 2000, vol. 1, pp. 73\u201380. IEEE (2000)","DOI":"10.1109\/ROBOT.2000.844042"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Moarref, S., Kress-Gazit, H.: Decentralized control of robotic swarms from high-level temporal logic specifications. In: International Symposium on Multi-Robot and Multi-Agent Systems. IEEE (2017, to appear)","DOI":"10.1109\/MRS.2017.8250926"},{"issue":"6","key":"5_CR9","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Robot."},{"issue":"11","key":"5_CR10","doi-asserted-by":"publisher","first-page":"2817","DOI":"10.1109\/TAC.2012.2195811","volume":"57","author":"T Wongpiromsarn","year":"2012","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Autom. Control 57(11), 2817\u20132830 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/MRA.2011.942116","volume":"18","author":"H Kress-gazit","year":"2011","unstructured":"Kress-gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive robot control from abstraction and temporal logic specifications. IEEE Robot. Autom. Mag. 18, 65\u201374 (2011)","journal-title":"IEEE Robot. Autom. Mag."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Ulusoy, A., Belta, C., Frazzoli, E., Rus, D.: Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications. In: IEEE International Conference on Robotics and Automation, pp. 5011\u20135018. IEEE (2013)","DOI":"10.1109\/ICRA.2013.6631293"},{"issue":"1","key":"5_CR13","doi-asserted-by":"publisher","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. 26(1), 48\u201361 (2010)","journal-title":"IEEE Trans. Robot."},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Nilsson, P., Ozay, N.: 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 (2016)","DOI":"10.1145\/2883817.2883831"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Kloetzer, M., Belta, C.: Hierarchical abstractions for robotic swarms. In: Proceedings 2006 IEEE International Conference on Robotics and Automation 2006. ICRA 2006, pp. 952\u2013957. IEEE (2006)","DOI":"10.1109\/ROBOT.2006.1641832"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Kloetzer, M., Ding, X.C., Belta, C.: 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 (2011)","DOI":"10.1109\/CDC.2011.6160478"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1146\/annurev-control-060117-104838","volume":"1","author":"H Kress-Gazit","year":"2018","unstructured":"Kress-Gazit, H., Lahijanian, M., Raman, V.: Synthesis for robots: guarantees and feedback for robot behavior. Ann. Rev. Control Robot. Auton. Syst. 1, 211\u2013236 (2018)","journal-title":"Ann. Rev. Control Robot. Auton. Syst."},{"key":"5_CR18","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23\u201335 (1962)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"key":"5_CR20","unstructured":"Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)"},{"issue":"3","key":"5_CR21","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.: Synthesis of reactive (1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-24743-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"JM Davoren","year":"2004","unstructured":"Davoren, J.M., Coulthard, V., Markey, N., Moor, T.: Non-deterministic temporal logics for general flow systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 280\u2013295. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24743-2_19"},{"issue":"7","key":"5_CR23","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"issue":"11","key":"5_CR24","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.: Towards temporal verification of swarm robotic systems. Robot. Auton. Syst. 60(11), 1429\u20131441 (2012)","journal-title":"Robot. Auton. Syst."},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-34281-3_7","volume-title":"Formal Methods and Software Engineering","author":"E Gjondrekaj","year":"2012","unstructured":"Gjondrekaj, E., et al.: Towards a formal verification methodology for collective robotic systems. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 54\u201370. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-34281-3_7"},{"key":"5_CR26","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)"},{"issue":"1","key":"5_CR27","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.: An algorithm for strongly connected component analysis in n log n symbolic steps. Form. Methods Syst. Des. 28(1), 37\u201356 (2006)","journal-title":"Form. Methods Syst. Des."},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive (1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11609773_24"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Raman, V., Kress-Gazit, H.: Synthesis for multi-robot controllers with interleaved motion. In: 2014 IEEE International Conference on Robotics and Automation (ICRA), pp. 4316\u20134321. IEEE (2014)","DOI":"10.1109\/ICRA.2014.6907487"},{"key":"5_CR30","unstructured":"Vahidi, A.: JDD (2018). \nhttp:\/\/javaddlib.sourceforge.net\/jdd\/index.html\n\n. Accessed 16 June 2018"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-41540-6_18","volume-title":"Computer Aided Verification","author":"R Ehlers","year":"2016","unstructured":"Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 333\u2013339. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_18"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-41540-6_14","volume-title":"Computer Aided Verification","author":"R Alur","year":"2016","unstructured":"Alur, R., Moarref, S., Topcu, U.: Compositional synthesis of reactive controllers for multi-agent systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 251\u2013269. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_14"},{"issue":"3","key":"5_CR33","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.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261\u2013296 (2011)","journal-title":"Form. Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00151-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T09:56:12Z","timestamp":1535190972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00151-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030001506","9783030001513"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00151-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}