ABSTRACT. The range of difficulties that can occur when running an experimental study in robotics is broad.
Subjects can behave in unforeseen ways, rendering the experimental scenario inconclusive, or
misunderstand questionnaire items or instructions. The robot may exhibit seemingly random
physical behaviors, or break down in the middle of the experiment. To increase the intricacy, imagine
the experiment being reproduced in another lab, research field, or country by other researchers with a
regular research publication as their only starting point.

Furthermore, assume that the publication is in an interdisciplinary research field, like social robotics or
HRI, in which authors from different fields often carry different levels of knowledge and disciplinary
interest about the social science methodologies, the technical system, and the conceptual background of the work.

Based on my experience in the field, I will introduce and discuss the "big five" issues of reproducible robotics
from both, a developer's and also from a reviewer's perspective. The discussed topics range from technical, to
methodological, to social aspects of reproducible robotics and are motivated by applied "real life"
projects and scenarios.

ABSTRACT. We propose to demonstrate the application of RoboChart and its associated tool, RoboTool, for the verification and validation of robotic applications. In our demonstration, we will consider a few small examples for illustration, and the larger example of a transporter. It is part of a swarm and cooperates with other identical robots to push an object to a target location.

ABSTRACT. In this demo, we will illustrate our work on integrating formal verification techniques, in particular probabilistic model checking, to enable long term deployments of mobile service robots in everyday environments. Our framework is based on generating policies for Markov decision process (MDP) models of mobile robots, using (co-safe) linear temporal logic specifications. More specifically, we build MDP models of robot navigation and action execution where the probability of successfully navigating between two locations and the expected time to do so are learnt from experience. For a specification over these models, we maximise the probability of the robot satisfying it, and minimise the expected time to do so. The policy obtained for this objective can be seen as a robot plan with attached probabilistic performance guarantees.

Our proposal is to showcase this framework live during the workshop, deploying our robot in the workshop venue and having it perform tasks throughout the day (the robot is based in the Oxford Robotics Institute, hence it can be easily moved to the workshop venue). In conjunction with showing the live robot behaviour, we will, among other things, provide visualisation of the generated policies on a map of the environment; showcase how the robot keeps track of the performance guarantees calculated offline during policy execution; and show how these guarantees can be used for execution monitoring.