Formal Verification of Digital Twins with the Temporal Logic of Actions

Verification of digital twins, especially in the presence of distributed components and asynchronous communication, remains a fundamental challenge. Uncertainty arises not only from the physical environment and virtual representations, but also from the bidirectional flow of data between them. This paper presents a formal verification methodology that captures these dynamics by translating a digital twin’s probabilistic elements into a finite state machine, augmented with explicit models of message delay and concurrent evolution. Using the Temporal Logic of Actions (TLA), we specify and verify temporal properties that ensure system-level correctness despite communication disorder and component-level asynchrony. We demonstrate this approach on a digital twin of an unmanned aerial vehicle, showing how to verify synchronization properties that govern end-to-end coherence between the physical and virtual components. Our case study highlights how formal specification clarifies system modeling choices, including which guarantees must hold, how system behaviors should be represented, and what assumptions are essential.