UNIVERSITY OF HERTFORDSHIRE
             COMPUTER SCIENCE RESEARCH COLLOQUIUM

                            presents

        "Formal Methods for Robot Behavior Verification 
                   using Linear Temporal Logic"
 
                        Dr. Joe Saunders 

    (Adaptive Systems Research Group, School of Computer Science,
                  University of Hertfordshire)

                    26 October 2016  (Wednesday)
                           1 - 2 pm 


                  Hatfield, College Lane Campus
                        Seminar Room D102 

                  Everyone is Welcome to Attend

                  Refreshments will be available


Abstract:

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. 


------------------------------------------------------------------------
Hertfordshire Computer Science Research Colloquium
http://cs-colloq.cs.herts.ac.uk