Probabilistic Model Checking of Robots Deployed in Extreme Environments
  Robots are increasingly used to carry out critical missions in extreme
environments that are hazardous for humans. This requires a high degree of
operational autonomy under uncertain conditions, and poses new challenges for
assuring the robot's safety and reliability. In this paper, we develop a
framework for probabilistic model checking on a layered Markov model to verify
the safety and reliability requirements of such robots, both at pre-mission
stage and during runtime. Two novel estimators based on conservative Bayesian
inference and imprecise probability model with sets of priors are introduced to
learn the unknown transition parameters from operational data. We demonstrate
our approach using data from a real-world deployment of unmanned underwater
vehicles in extreme environments.
