Evaluating the Effectiveness of Digital Twins Through Statistical Model Checking with Feedback and Perturbations

We present DT-Stark, an extension of the Stark tool aimed at the verification and evaluation of the effectiveness of digital twins, i.e., their ability to direct the physical counterparts. To this end, we introduce feedback in Stark, a special mechanism that allow us to model the communications, and their effects, between the digital and the physical (perturbed) twin in a concise, clean fashion. We can then exploit the features of Stark to compare the behaviour of the twins, to verify properties over them, and to measure effectiveness. We provide some examples of the use of our tool by applying it to the evaluation of the effectiveness of digital twins in two robotic scenarios.