Formal methods for robot behavior verification using linear temporal logic

This talk was given on 13th January 2016 by Joe Saunders.

How can we have sophisticated interactions with robots in a safe and trustworthy manner? This is a fundamental research question that must be addressed before the traditional physical safety barrier between the robot and the human can be removed. There has been some work on safety at lower mechanical/compliance levels to restrict robot movements near humans. However the safety of robotic high-level behaviors during interaction with humans has not been actively researched.

In this talk I will present some work carried out by UH in collaboration with the University of Liverpool studying the formal verification of high level robot behaviors using a technique called `model checking'. I will outline this verification method, and introduce the concept of temporal logic for ensuring correctness of behaviors. I will also present come results of applying this work to real robotic scenarios operating in the UH robot house.

2012 © Adaptive Systems Research Group

web stat counter