A Caltech Library Service

Provably correct reactive control from natural language

Lignos, Constantine and Raman, Vasumathi and Finucane, Cameron and Marcus, Mitchell and Kress-Gazit, Hadas (2015) Provably correct reactive control from natural language. Autonomous Robots, 38 (1). pp. 89-105. ISSN 0929-5593.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


This paper presents an integrated system for generating, troubleshooting, and executing correct-by-construction controllers for autonomous robots using natural language input, allowing non-expert users to command robots to perform high-level tasks. This system unites the power of formal methods with the accessibility of natural language, providing controllers for implementable high-level task specifications, easy-to-understand feedback on those that cannot be achieved, and natural language explanation of the reason for the robot’s actions during execution. The natural language system uses domain-general components that can easily be adapted to cover the vocabulary of new applications. Generation of a linear temporal logic specification from the user’s natural language input uses a novel data structure that allows for subsequent mapping of logical propositions back to natural language, enabling natural language feedback about problems with the specification that are only identifiable in the logical form. We demonstrate the robustness of the natural language understanding system through a user study where participants interacted with a simulated robot in a search and rescue scenario. Automated analysis and user feedback on unimplementable specifications is demonstrated using an example involving a robot assistant in a hospital.

Item Type:Article
Related URLs:
URLURL TypeDescription ReadCube access
Additional Information:© 2014 Springer Science+Business Media New York. Received: 1 October 2013. Accepted: 8 October 2014. Published online: 19 November 2014. We would like to thank Taylor Turpen, Israel Geselowitz, and Kenton Lee for their assistance with software development and data collection. This work was supported in part by: ARO MURI (SUBTLE) W911NF-07-1-0216, NSF CAREER CNS-0953365, DARPA N66001-12-1-4250, and TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA.
Funding AgencyGrant Number
Army Research Office (ARO)W911NF-07-1-0216
Defense Advanced Research Projects Agency (DARPA)N66001-12-1-4250
Microelectronics Advanced Research Corp. (MARCO)UNSPECIFIED
Subject Keywords:Natural language, Formal methods, High-level control. Synthesis
Issue or Number:1
Record Number:CaltechAUTHORS:20150212-132815606
Persistent URL:
Official Citation:Lignos, C., Raman, V., Finucane, C. et al. Auton Robot (2015) 38: 89. doi:10.1007/s10514-014-9418-8
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:54790
Deposited By: Ruth Sustaita
Deposited On:13 Feb 2015 04:30
Last Modified:03 Oct 2019 08:00

Repository Staff Only: item control page