Synthesis for robots: guarantees and feedback for robot behavior
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 i...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Published: |
Annual Reviews
2018
|
| _version_ | 1797057576755527680 |
|---|---|
| author | Kress-Gazit, H Lahijanian, M Raman, V |
| author_facet | Kress-Gazit, H Lahijanian, M Raman, V |
| author_sort | Kress-Gazit, H |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T19:38:25Z |
| format | Journal article |
| id | oxford-uuid:1fd2aabc-5bbf-4253-9e48-0e0bd35bf8e8 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:38:25Z |
| publishDate | 2018 |
| publisher | Annual Reviews |
| record_format | dspace |
| spelling | oxford-uuid:1fd2aabc-5bbf-4253-9e48-0e0bd35bf8e82022-03-26T11:24:07ZSynthesis for robots: guarantees and feedback for robot behaviorJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:1fd2aabc-5bbf-4253-9e48-0e0bd35bf8e8Symplectic Elements at OxfordAnnual Reviews2018Kress-Gazit, HLahijanian, MRaman, VRobot 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. |
| spellingShingle | Kress-Gazit, H Lahijanian, M Raman, V Synthesis for robots: guarantees and feedback for robot behavior |
| title | Synthesis for robots: guarantees and feedback for robot behavior |
| title_full | Synthesis for robots: guarantees and feedback for robot behavior |
| title_fullStr | Synthesis for robots: guarantees and feedback for robot behavior |
| title_full_unstemmed | Synthesis for robots: guarantees and feedback for robot behavior |
| title_short | Synthesis for robots: guarantees and feedback for robot behavior |
| title_sort | synthesis for robots guarantees and feedback for robot behavior |
| work_keys_str_mv | AT kressgazith synthesisforrobotsguaranteesandfeedbackforrobotbehavior AT lahijanianm synthesisforrobotsguaranteesandfeedbackforrobotbehavior AT ramanv synthesisforrobotsguaranteesandfeedbackforrobotbehavior |