{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T08:58:14Z","timestamp":1783501094861,"version":"3.55.0"},"reference-count":122,"publisher":"Annual Reviews","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annu. Rev. Control Robot. Auton. Syst."],"published-print":{"date-parts":[[2018,5,28]]},"abstract":"<jats:p> Robot control for tasks such as moving around obstacles or grasping objects has advanced significantly in the last few decades. However, controlling robots to perform complex tasks is still accomplished largely by highly trained programmers in a manual, time-consuming, and error-prone process that is typically validated only through extensive testing. Formal methods are mathematical techniques for reasoning about systems, their requirements, and their guarantees. Formal synthesis for robotics refers to frameworks for specifying tasks in a mathematically precise language and automatically transforming these specifications into correct-by-construction robot controllers or into a proof that the task cannot be done. Synthesis allows users to reason about the task specification rather than its implementation, reduces implementation error, and provides behavioral guarantees for the resulting controller. This article reviews the current state of formal synthesis for robotics and surveys the landscape of abstractions, specifications, and synthesis algorithms that enable it. <\/jats:p>","DOI":"10.1146\/annurev-control-060117-104838","type":"journal-article","created":{"date-parts":[[2018,1,19]],"date-time":"2018-01-19T21:17:10Z","timestamp":1516396630000},"page":"211-236","source":"Crossref","is-referenced-by-count":134,"title":["Synthesis for Robots: Guarantees and Feedback for Robot Behavior"],"prefix":"10.1146","volume":"1","author":[{"given":"Hadas","family":"Kress-Gazit","sequence":"first","affiliation":[{"name":"Sibley School of Mechanical and Aerospace Engineering, Cornell University, Ithaca, New York 14853, USA;"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Morteza","family":"Lahijanian","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford OX1 3QD, United Kingdom;"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vasumathi","family":"Raman","sequence":"additional","affiliation":[{"name":"San Francisco, California 94103, USA;"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"22","reference":[{"key":"B1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"issue":"2","key":"B2","volume-title":"J. Field Robot","volume":"34","author":"Spenko M","year":"2017"},{"key":"B3","first-page":"153","volume-title":"43rd IEEE Conference on Decision and Control","author":"Loizou SSG","year":"2004"},{"key":"B4","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2006.889492"},{"key":"B5","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2008.4586787"},{"key":"B6","doi-asserted-by":"publisher","DOI":"10.1109\/COASE.2008.4626521"},{"key":"B7","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426027"},{"key":"B8","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6631293"},{"key":"B9","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907487"},{"key":"B10","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942581"},{"key":"B11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-51532-8_28"},{"key":"B12","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2015.7139021"},{"key":"B13","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2016.04.006"},{"key":"B14","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942758"},{"key":"B15","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6906924"},{"key":"B16","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799298"},{"key":"B17","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2012.2214558"},{"key":"B18","doi-asserted-by":"publisher","DOI":"10.1007\/s10514-014-9418-8"},{"key":"B19","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-016-0232-7"},{"key":"B20","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340472"},{"key":"B21","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2011.5979895"},{"key":"B22","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461330"},{"key":"B23","first-page":"5025","volume-title":"2013 IEEE International Conference on Robotics and Automation (ICRA)","author":"Guo M","year":"2013"},{"key":"B24","doi-asserted-by":"publisher","DOI":"10.1177\/0278364915587034"},{"key":"B25","first-page":"3664","volume-title":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence","author":"Lahijanian M","year":"2015"},{"key":"B26","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799414"},{"key":"B27","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"B28","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679387"},{"key":"B29","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2015.7139025"},{"key":"B30","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883832"},{"key":"B31","doi-asserted-by":"publisher","DOI":"10.1177\/0278364914562980"},{"key":"B32","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883847"},{"key":"B33","unstructured":"33.\u2002  McDermott  D,  Ghallab  M,  Howe  A,  Knoblock  C,  Ram  A,  et al.  1998.  PDDL\u2014the Planning Domain Definition Language.  Tech. Rep. CVC TR-98-003\/DCS TR-1165, Cent. Comput. Vision Control, Yale Univ., New Haven, CT"},{"key":"B34","first-page":"1215","volume-title":"Proceedings of the Thirteenth National Conference on Artificial Intelligence","author":"Bacchus F","year":"1996"},{"key":"B35","doi-asserted-by":"publisher","DOI":"10.1007\/10720246_18"},{"key":"B36","first-page":"1039","volume-title":"Proceedings of the Tenth International Joint Conference on Artificial Intelligence (IJCAI-87)","author":"Schoppers M","year":"1987"},{"key":"B37","doi-asserted-by":"publisher","DOI":"10.1613\/jair.277"},{"key":"B38","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509274"},{"key":"B39","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00374-0"},{"key":"B40","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.05.003"},{"key":"B41","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-015-0223-0"},{"key":"B42","volume-title":"Model Checking","author":"Clarke EM","year":"1999"},{"key":"B43","doi-asserted-by":"publisher","DOI":"10.1090\/crmm\/023"},{"key":"B44","volume-title":"Communicating and Mobile Systems: The \u03c0 Calculus","author":"Milner R.","year":"1999"},{"key":"B45","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2003.08.001"},{"key":"B46","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2003.1249705"},{"key":"B47","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2005.1582713"},{"key":"B48","doi-asserted-by":"publisher","DOI":"10.1109\/70.163777"},{"key":"B49","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2010.2062070"},{"key":"B50","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.02.021"},{"key":"B51","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2176409"},{"key":"B52","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2016.02.002"},{"key":"B53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_49"},{"key":"B54","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461343"},{"key":"B55","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883834"},{"key":"B56","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.851439"},{"key":"B57","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942113"},{"key":"B58","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2015.7402390"},{"key":"B59","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2006.II.008"},{"key":"B60","doi-asserted-by":"publisher","DOI":"10.1177\/0278364910369189"},{"key":"B61","doi-asserted-by":"publisher","DOI":"10.3182\/20110828-6-IT-1002.03098"},{"key":"B62","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6315544"},{"key":"B63","doi-asserted-by":"publisher","DOI":"10.1177\/0278364917712421"},{"key":"B64","unstructured":"64.\u2002  Tedrake  R, Drake Dev. Team.  2014.  Drake: a planning, control, and analysis toolbox for nonlinear dynamical systems.  http:\/\/drake.mit.edu"},{"key":"B65","doi-asserted-by":"publisher","DOI":"10.1177\/0278364914557736"},{"key":"B66","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2015.2414134"},{"key":"B67","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2012.2205651"},{"key":"B68","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"B69","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"B70","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011254632723"},{"key":"B71","volume-title":"Principles of Model Checking","author":"Baier C","year":"2008"},{"key":"B72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"B73","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"B74","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"B75","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"B76","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"B77","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2009.5152605"},{"key":"B78","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.08.008"},{"key":"B79","doi-asserted-by":"publisher","DOI":"10.1177\/0278364911417911"},{"key":"B80","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6631296"},{"key":"B81","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461380"},{"key":"B82","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2016.2544339"},{"key":"B83","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509503"},{"key":"B84","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942115"},{"key":"B85","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2013.6697051"},{"key":"B86","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6943085"},{"key":"B87","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2015.7139022"},{"key":"B88","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509686"},{"key":"B89","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2011.5990952"},{"key":"B90","first-page":"11803","volume":"18","author":"Cizelj I","year":"2011","journal-title":"IFAC-PapersOnline"},{"key":"B91","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2011.2172150"},{"key":"B92","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400629"},{"key":"B93","first-page":"3515","volume":"18","author":"Ding XC","year":"2011","journal-title":"IFAC-PapersOnline"},{"key":"B94","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760491"},{"key":"B95","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2298143"},{"key":"B96","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2015.2499164"},{"key":"B97","first-page":"4687","volume-title":"2012 IEEE International Conference on Robotics and Automation (ICRA)","author":"Wang J","year":"2012"},{"key":"B98","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2014.X.039"},{"key":"B99","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"B100","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039527"},{"key":"B101","doi-asserted-by":"publisher","DOI":"10.1177\/0278364915581505"},{"key":"B102","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426174"},{"key":"B103","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2398883"},{"key":"B104","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16595-0_20"},{"key":"B105","unstructured":"105.\u2002  de Alfaro  L.  1997.  Formal verification of probabilistic systems.  PhD Thesis, Dep. Comput. Sci., Stanford Univ.,  Stanford, CA"},{"key":"B106","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"B107","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942116"},{"key":"B108","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2195811"},{"key":"B109","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"B110","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_9"},{"key":"B111","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_18"},{"key":"B112","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_18"},{"key":"B113","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2010.5650371"},{"key":"B114","doi-asserted-by":"publisher","DOI":"10.1109\/CCA.2016.7587949"},{"key":"B115","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2008.4739370"},{"key":"B116","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_23"},{"key":"B117","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907641"},{"key":"B118","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2017.7963399"},{"key":"B119","first-page":"343","volume-title":"HSCC'13: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control","author":"Gol EA","year":"2013"},{"key":"B120","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728628"},{"key":"B121","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"B122","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_10"}],"container-title":["Annual Review of Control, Robotics, and Autonomous Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.annualreviews.org\/doi\/pdf\/10.1146\/annurev-control-060117-104838","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,8]],"date-time":"2021-10-08T10:46:54Z","timestamp":1633690014000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.annualreviews.org\/doi\/10.1146\/annurev-control-060117-104838"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,28]]},"references-count":122,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,5,28]]}},"alternative-id":["10.1146\/annurev-control-060117-104838"],"URL":"https:\/\/doi.org\/10.1146\/annurev-control-060117-104838","relation":{},"ISSN":["2573-5144","2573-5144"],"issn-type":[{"value":"2573-5144","type":"print"},{"value":"2573-5144","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,28]]}}}