As autonomous robots increasingly navigate complex and unpredictable environments, ensuring their reliable behavior under uncertainty becomes a critical challenge. This paper introduces a digital twin-based runtime verification for an autonomous mobile robot to mitigate the impact posed by uncertainty in the deployment environment. The safety and performance properties are specified and synthesized as runtime monitors using TeSSLa. The integration of the executable digital twin, via the MQTT protocol, enables continuous monitoring and validation of the robot's behavior in real-time. We explore the sources of uncertainties, including sensor noise and environment variations, and analyze their impact on the robot safety and performance. Equipped with high computation resources, the cloud-located digital twin serves as a watch-dog model to estimate the actual state, check the consistency of the robot's actuations and intervene to override such actuations if a safety or performance property is about to be violated. The experimental analysis demonstrated high efficiency of the proposed approach in ensuring the reliability and robustness of the autonomous robot behavior in uncertain environments and securing high alignment between the actual and expected speeds where the difference is reduced by up to 41\% compared to the default robot navigation control.

翻译：随着自主机器人在复杂且不可预测环境中日益广泛应用，确保其在不确定性下的可靠行为成为关键挑战。本文提出一种基于数字孪生的自主移动机器人运行时验证方法，以降低部署环境不确定性带来的影响。通过TeSSLa语言将安全性与性能属性规约并合成为运行时监控器。借助MQTT协议集成的可执行数字孪生，实现了对机器人行为的持续实时监测与验证。我们探究了传感器噪声与环境变化等不确定性来源，并分析其对机器人安全性与性能的影响。依托云端强大的计算资源，数字孪生作为看门狗模型执行以下功能：估计实际状态、检查机器人执行动作的一致性，并在安全或性能属性即将被违反时介入并覆盖原有动作。实验分析表明，该方法能高效保障自主机器人在不确定环境中的行为可靠性与鲁棒性，实际速度与期望速度的匹配度显著提升——相较于默认机器人导航控制，速度差异最高可减少41%。