Authoring and Verifying Human-Robot Interactions
summary
A web authoring tool called RoVer lets designers drag and drop microinteractions into a state‑machine, translates that model into a transition system, and checks encoded social norms expressed in linear temporal logic with a standard verification engine. The system reports which norms are violated and highlights offending states; a user study (N=9) shows assisted designers halve the gap between perceived and actual violations and find and interpret errors more easily. Limitations: no probabilistic or continuous‑time models yet.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:25Background
- 0:48What Situations Do We Envision Robots Serving
- 1:23The Delivery Robot
- 3:34Research Question
- 4:14Proposed Solution
- 5:16Design Tools
- 5:40Micro Interactions
- 7:02Under the Hood
- 8:13Low Level Transition System
- 11:07Linear Temporal Logic
- 13:43Evaluation of Rover
- 16:39Model Precision
related talks
12mAuthr: A Task Authoring Environment for Human-Robot Teams
09mSituated Live Programming for Human-Robot Collaboration
29mSynchronous Programming and Refinement Types in Robotics: From Verification to Implementation
59mOn Human-robot Interactions via Multimodal Intent Modeling and Reachability-based Safety Assurance
14mTowards Unobtrusive Physical AI: Augmenting Everyday Objects with Intelligence and Robotic Moveme...
05mInterview
11mLearning Socially Appropriate Robo-waiter Behaviours through Real-time User Feedback
10mCognitively Assistive Robots at Home: HRI Design Patterns for Translational Science