Formal Verification of Digital Twins with TLA and Information Leakage Control

TL;DR

This work presents a formal methodology for designing and verifying digital twins using the Temporal Logic of Actions (TLA+), addressing uncertainties in both the virtual and physical domains and the bidirectional data exchange across distributed components. It introduces a novel augmentation of the digital twin probabilistic graphical model (PGM) to account for distributed communication and translates the augmented PGM into a finite-state machine suitable for model checking, while also weakening formal verification with statistical guarantees on information leakage. The UAV digital twin serves as a concrete demonstration, where synchronization between physical and digital states is formally specified and verified, including analysis of state-space growth and iterative bug fixes (e.g., timestamp validation). The approach yields formal guarantees on system orchestration and controlled information leakage, offering a principled path toward safe, verifiable digital twins in safety-critical settings, though it also highlights scalability challenges inherent to model checking of complex distributed systems.

Abstract

Verifying the correctness of a digital twin provides a formal guarantee that the digital twin operates as intended. Digital twin verification is challenging due to the presence of uncertainties in the virtual representation, the physical environment, and the bidirectional flow of information between physical and virtual. A further challenge is that a digital twin of a complex system is composed of distributed components. This paper presents a methodology to specify and verify digital twin behavior, translating uncertain processes into a formally verifiable finite state machine. We use the Temporal Logic of Actions (TLA) to create a specification, an implementation abstraction that defines the properties required for correct system behavior. Our approach includes a novel weakening of formal security properties, allowing controlled information leakage while preserving theoretical guarantees. We demonstrate this approach on a digital twin of an unmanned aerial vehicle, verifying synchronization of physical-to-virtual and virtual-to-digital data flows to detect unintended misalignments.

Figures (13)

• Figure 1: Digital twin consisting of a physical system (unmanned aerial vehicle), a virtual representation (structural health models), and bidirectional connections among components.
• Figure 2: Derivation of state machine processes from PGM representation. Nodes represent variables and edges between nodes represent the dependence of the destination node on the parent node. The subscript $X_t$ denote the variable $X$'s state at time $t$.
• Figure 3: PGM with distributed communication required for two processes: (1) $O \rightarrow D$ and (2) $U \rightarrow S$.
• Figure 4: Augmentation for $O$, which is communicated over a distributed channel to $D$.
• Figure 5: Reproduced with permission from salinger: testbed UAV (top) equipped with individually-transmitting Bluetooth sensors (bottom)

Theorems & Definitions (1)

• Theorem 1