Digital Twin Enabled Runtime Verification for Autonomous Mobile Robots under Uncertainty

TL;DR

This paper presents a digital twin-based runtime verification system for autonomous mobile robots, enhancing safety and performance under environmental uncertainties through real-time monitoring and intervention.

Contribution

It introduces a novel integration of digital twins with runtime verification using TeSSLa and MQTT, specifically tailored for autonomous robots in uncertain environments.

Findings

Reduced speed deviation by up to 41%

Effective real-time monitoring and intervention

Improved reliability and robustness of robot behavior

Abstract

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.