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