SMT-Based Control and Feedback for Social Navigation
Thais Campos, Adam Pacheck, Guy Hoffman, Hadas Kress-Gazit
Abstract
This paper combines techniques from Formal Methods and Human-Robot Interaction (HRI) to address the challenge of a robot walking with a human while maintaining a socially acceptable distance and avoiding collisions. We formulate a set of constraints on the robot motion using Satisfiability Modulo Theories (SMT) formulas, and synthesize robot control that is guaranteed to be safe and correct. Due to its use of high-level formal specifications, the controller is able to provide feedback to the user in situations where human behavior causes the robot to fail. This feedback allows the human to adjust their behavior and recover joint navigation. We demonstrate the behavior of the robot in a variety of simulated scenarios and compare it to utility-based side-by-side navigation control.
BibTeX
@inproceedings{icra2019_smtbasedcontrola,
title = {SMT-Based Control and Feedback for Social Navigation},
author = {Thais Campos and Adam Pacheck and Guy Hoffman and Hadas Kress-Gazit},
booktitle = {ICRA 2019},
year = {2019}
}