Interactive Robot Transition Repair With SMT
Interactive Robot Transition Repair With SMT
Jarrett Holtz, Arjun Guha, Joydeep Biswas
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 4905-4911.
https://doi.org/10.24963/ijcai.2018/681
Complex robot behaviors are often structured as
state machines, where states encapsulate actions
and a transition function switches between states.
Since transitions depend on physical parameters,
when the environment changes, a roboticist has to
painstakingly readjust the parameters to work in
the new environment. We present interactive SMT-
based Robot Transition Repair (SRTR): instead of
manually adjusting parameters, we ask the roboticist to identify a few instances where the robot is
in a wrong state and what the right state should
be. An automated analysis of the transition function 1) identifies adjustable parameters, 2) converts the transition function into a system of logical constraints, and 3) formulates the constraints
and user-supplied corrections as a MaxSMT problem that yields new parameter values. We show
that SRTR finds new parameters 1) quickly, 2)
with few corrections, and 3) that the parameters
generalize to new scenarios. We also show that
a SRTR-corrected state machine can outperform a
more complex, expert-tuned state machine.
Keywords:
Constraints and SAT: MaxSAT, MinSAT
Robotics: Robotics
Robotics: Dependable Robots
Constraints and SAT: SAT: Applications