MIO-BDT: Construction of Basic Models and Formal Verification of Building Digital Twins That Supports Multiple Interactive Objects

As a high-fidelity digital mapping of the physical built environment, the Building Digital Twin (BDT) relies on physical–virtual interaction as a core enabler for lifecycle management. However, existing BDT conceptual models predominantly focus on unidirectional or single-threaded physical–virtual interactions, neglecting the dynamic, concurrent exchanges among multiple digital twins and human users. To overcome this limitation, the Multi-Interactive-Object BDT (MIO-BDT) framework is proposed. The central hypothesis is that explicitly modeling concurrent, multi-party interactions within a formalized conceptual structure can address a key representational gap in current BDT paradigms. The work pursues two testable objectives: (1) to formally define the components, relationships, and rules of the MIO-BDT framework and (2) to validate through a representative use case that the framework can model complex interaction scenarios that are inadequately supported by existing approaches. A systematic analysis of the state of the art is first conducted to ground the framework’s design. The MIO-BDT is then elaborated at both the system level (supporting dynamic interactions among twins, users, and physical entities) and the component level (integrating visual, physical, and interaction sub-models). Formal modeling and verification demonstrate that the framework is logically consistent and deadlock-free and effectively coordinates multi-entity data flows. These findings confirm that the MIO-BDT framework provides enhanced representational capacity, structural clarity for system design, and a unified model for diverse interaction types, thereby establishing a validated conceptual foundation for next-generation, interaction-aware BDT systems.