We develop a novel Bayesian learning framework that enables the runtime verification of autonomous robots performing critical missions in uncertain environments. Our framework exploits prior knowledge and observations of the verified robotic system to learn expected ranges of values for the occurrence rates of its events. We support both events observed regularly during system operation, and singular events such as catastrophic failures or the completion of difficult one-off tasks. Furthermore, we use the learnt event-rate ranges to assemble interval continuous-time Markov models, and we apply quantitative verification to these models to compute expected intervals of variation for key system properties. These intervals reflect the uncertainty intrinsic to many real-world systems, enabling the robust verification of their quantitative properties under parametric uncertainty. We apply the proposed framework to the case study of verification of an autonomous robotic mission for underwater infrastructure inspection and repair.

翻译：我们提出了一种新颖的贝叶斯学习框架，能够在不确定环境中对执行关键任务的自主机器人进行运行时验证。该框架利用先验知识及对已验证机器人系统的观测结果，学习其事件发生率的预期取值范围。我们支持两类事件：系统运行期间可定期观测的事件，以及灾难性故障或困难的一次性任务完成等偶发事件。此外，我们利用学习到的事件率区间构建区间连续时间马尔可夫模型，并对这些模型应用定量验证，以计算关键系统属性的预期变化区间。这些区间反映了诸多真实系统固有的不确定性，从而能够在参数不确定性条件下对其定量属性进行鲁棒验证。我们将所提框架应用于水下基础设施巡检与维修自主机器人任务的验证案例研究。