Digital Twin Enabled Runtime Verification for Autonomous Mobile Robots under Uncertainty

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 as a service approach to enable runtime monitoring and verification of an autonomous mobile robot and 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 different sources of uncertainties 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, checking the consistency of the robot’s actuations and approving or denying such actuations depending on the safety and performance properties. The experimental analysis demonstrated high efficiency of the proposed approach in ensuring the reliability and robustness of the autonomous robot behavior in uncertain environments by 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.