Verification of Digital Twins using Classical and Statistical Model Checking

• URL: http://arxiv.org/abs/2505.04322v1
• Date: Wed, 07 May 2025 11:12:46 GMT
• Title: Verification of Digital Twins using Classical and Statistical Model Checking
• Authors: Raghavendran Gunasekaran, Boudewijn Haverkort,
• Abstract summary: The concept of digital twin (DT) has received a widespread attention in both industry and academia.<n>We present our observations and findings from applying these techniques on the DT of an autonomously driving truck.<n>Results from these verification techniques suggest that this DT adheres to properties of deadlock freeness and functional correctness, but not adhering to timeliness properties.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: With the increasing adoption of digital techniques, the concept of digital twin (DT) has received a widespread attention in both industry and academia. While several definitions exist for a DT, most definitions focus on the existence of a virtual entity (VE) of a real-world object or process, often comprising interconnected models which interact with each other, undergoing changes continuously owing to the synchronization with the real-world object. These interactions might lead to inconsistencies at execution time, due to their highly stochastic and/or time-critical nature, which may lead to undesirable behavior. In addition, the continuously varying nature of VE owing to its synchronization with the real-world object further contributes to the complexity arising from these interactions and corresponding model execution times, which could possibly affect its overall functioning at runtime. This creates a need to perform (continuous) verification of the VE, to ensure that it behaves consistently at runtime by adhering to desired properties such as deadlock freeness, functional correctness, liveness and timeliness. Some critical properties such as deadlock freeness can only be verified using classical model checking; on the other hand, statistical model checking provides the possibility to model actual stochastic temporal behavior. We therefore propose to use both these techniques to verify the correctness and the fulfillment of desirable properties of VE. We present our observations and findings from applying these techniques on the DT of an autonomously driving truck. Results from these verification techniques suggest that this DT adheres to properties of deadlock freeness and functional correctness, but not adhering to timeliness properties.

Related papers

• Causal Discovery in Multivariate Time Series through Mutual Information Featurization [0.1657441317977376]
  Temporal Dependency to Causality (TD2C) learns to recognize complex causal signatures from a rich set of information-theoretic and statistical descriptors.<n>Our results show that TD2C achieves state-of-the-art performance, consistently outperforming established methods.
  arXiv  Detail & Related papers  (2025-08-03T17:03:13Z)
• Learning Time-Aware Causal Representation for Model Generalization in Evolving Domains [50.66049136093248]
  We develop a time-aware structural causal model (SCM) that incorporates dynamic causal factors and the causal mechanism drifts.<n>We show that our method can yield the optimal causal predictor for each time domain.<n>Results on both synthetic and real-world datasets exhibit that SYNC can achieve superior temporal generalization performance.
  arXiv  Detail & Related papers  (2025-06-21T14:05:37Z)
• ShaTS: A Shapley-based Explainability Method for Time Series Artificial Intelligence Models applied to Anomaly Detection in Industrial Internet of Things [0.0]
  This work presents ShaTS (Shapley values for Time Series models), which is a model-agnostic explainable Artificial Intelligence method designed to enhance the precision of Shapley value explanations for time series models.<n> Experiments conducted on the SWaT dataset demonstrate that ShaTS accurately identifies critical time instants, precisely pinpoints the sensors, actuators, and processes affected by anomalies, and outperforms SHAP in terms of both explainability and resource efficiency.
  arXiv  Detail & Related papers  (2025-06-02T09:07:27Z)
• Bridging the Reality Gap in Digital Twins with Context-Aware, Physics-Guided Deep Learning [3.0996501197166975]
  Digital twins (DTs) enable powerful predictive analytics, but persistent discrepancies between simulations and real systems--known as the reality gap--undermine their reliability.<n>We propose a Reality Gap Analysis (RGA) module for DTs that continuously integrates new sensor data, detects misalignments, and recalibrates DTs via a query-response framework.<n>Our approach fuses domain-adversarial deep learning with reduced-order simulator guidance to improve context inference and preserve physical consistency.
  arXiv  Detail & Related papers  (2025-05-17T05:18:46Z)
• On the Identification of Temporally Causal Representation with Instantaneous Dependence [50.14432597910128]
  Temporally causal representation learning aims to identify the latent causal process from time series observations. Most methods require the assumption that the latent causal processes do not have instantaneous relations. We propose an textbfIDentification framework for instantanetextbfOus textbfLatent dynamics.
  arXiv  Detail & Related papers  (2024-05-24T08:08:05Z)
• A Poisson-Gamma Dynamic Factor Model with Time-Varying Transition Dynamics [51.147876395589925]
  A non-stationary PGDS is proposed to allow the underlying transition matrices to evolve over time. A fully-conjugate and efficient Gibbs sampler is developed to perform posterior simulation. Experiments show that, in comparison with related models, the proposed non-stationary PGDS achieves improved predictive performance.
  arXiv  Detail & Related papers  (2024-02-26T04:39:01Z)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity. We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
  arXiv  Detail & Related papers  (2023-12-13T21:53:32Z)
• Introducing 3DCNN ResNets for ASD full-body kinematic assessment: a comparison with hand-crafted features [1.3499500088995464]
  We propose a newly adapted 3DCNN ResNet from and compare it to widely used hand-crafted features for motor ASD assessment. Specifically, we developed a virtual reality environment with multiple motor tasks and trained models using both approaches. Results show the proposed model achieves a maximum accuracy of 85$pm$3%, outperforming state-of-the-art end-to-end models with short 1-to-3 minute samples.
  arXiv  Detail & Related papers  (2023-11-24T14:56:36Z)
• TimeTuner: Diagnosing Time Representations for Time-Series Forecasting with Counterfactual Explanations [3.8357850372472915]
  This paper contributes a novel visual analytics framework, namely TimeTuner, to help analysts understand how model behaviors are associated with localized, stationarity, and correlations of time-series representations. We show that TimeTuner can help characterize time-series representations and guide the feature engineering processes.
  arXiv  Detail & Related papers  (2023-07-19T11:40:15Z)
• Edge Continual Learning for Dynamic Digital Twins over Wireless Networks [68.65520952712914]
  Digital twins (DTs) constitute a critical link between the real-world and the metaverse. In this paper, a novel edge continual learning framework is proposed to accurately model the evolving affinity between a physical twin and its corresponding cyber twin. The proposed framework achieves a simultaneously accurate and synchronous CT model that is robust to catastrophic forgetting.
  arXiv  Detail & Related papers  (2022-04-10T23:25:37Z)
• Continuity-Discrimination Convolutional Neural Network for Visual Object Tracking [150.51667609413312]
  This paper proposes a novel model, named Continuity-Discrimination Convolutional Neural Network (CD-CNN) for visual object tracking. To address this problem, CD-CNN models temporal appearance continuity based on the idea of temporal slowness. In order to alleviate inaccurate target localization and drifting, we propose a novel notion, object-centroid.
  arXiv  Detail & Related papers  (2021-04-18T06:35:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.