Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2509.10936

Framework for Formal Modelling of Metaverse Applications Using Hierarchical Colored Petri Nets

Maryam Amin·Umara Noor·Zahid Rashid·Jorn Altmann
View original source ↗Read source document ↗Export metadata ↓

Abstract

The Metaverse emerges by integrating highly-distributed, complex, and interconnecting technologies. These technologies need to be formally verified and evaluated through formal modelling before executing them in real-world applications, in order to avoid negative impacts on the real world due to failure of the Metaverse technologies. However, the formal modelling of Metaverse technologies is challenging due to its highly complex nature. Therefore, a comprehensive formal verification of the Metaverse technologies is needed for its realization in multiple potential areas. In this study, a framework is proposed for the formal modelling of Metaverse technologies, which allows holistic insights for all applications of Metaverse technologies. By utilizing the proposed framework, Metaverse applications of any complexity can be modeled. The working of the proposed framework is illustrated by modelling a case study of an Air Traffic Control system. In the proposed framework, we utilize hierarchical colored Petri nets for formal modelling of behavior of the air traffic control system. The correctness of air traffic control system properties, such as liveness, reachability, and boundedness, is verified in the proposed framework. The results of the case study reveal that the proposed framework can be used as a template for mathematical verification of challenging and complex Metaverse applications. The results also show that formal modelling provides an effective tool for identifying flaws in the early phases of the design of Metaverse applications. The implication of using formal verification is that it can increase confidence about the correctness of the Metaverse applications.

Explore related subjects

cs.ET

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Maryam Amin, Umara Noor, Zahid Rashid, Jorn Altmann. 2025-09-13. Framework for Formal Modelling of Metaverse Applications Using Hierarchical Colored Petri Nets. https://arxiv.org/abs/2509.10936

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Beyond HBM-on-GPU: Thermal Design Envelope for 3D Volumetric DRAM-on-GPU Integration

The scaling of GPUs for AI and HPC workloads is increasingly constrained by the capacity, bandwidth, and thermal limits of both 2.5D HBM-GPU and direct-stacked 3D HBM-on-GPU integration. This work establishes the thermal design envelope for 3D volumetric DRAM-on-GPU integration, in which vertically oriented DRAM dies and interleaved cooling cavities reshape heat flow and memory interfacing above the GPU. Using a package-level thermal model anchored to a consistent HBM-on-GPU baseline and driven by a realistic reticle-scale non-uniform GPU power map, we quantify the key parameters governing thermal feasibility. Stack height is the dominant limiter of peak temperature, while cooling-cavity conductivity shifts the feasible region, and mold insertion and stack orientation further modulate thermal behavior. A distributed memory-controller and network-on-chip tier introduces only a moderate thermal penalty. Although die-level parallelism increases bandwidth, the reduction in simulated training time saturates once execution becomes compute-bound. These results define a bounded co-design space across bandwidth, capacity, and thermal constraints for 3D volumetric DRAM-on-GPU integration.

cs.ET↗
arXiv2026

Droop-Aware Foundation Model Power Flow

This paper develops a droop-aware extension of the GridFM power systems foundation model, embedding droop gains and frequency/voltage deadband parameters as per-bus node features to enable control-aware AC power-flow analysis. Existing power-flow datasets encode only static electrical features, conflating operating points from qualitatively different control regimes; this work resolves that gap by exposing droop and deadband parameters as structured node features, with deadband discontinuities handled through a smooth tanh approximation that preserves solver differentiability. A transformer-based graph neural network is pre-trained on masked reconstruction and fine-tuned on the resulting control-aware datasets. The framework is validated against PSCAD electromagnetic-transient simulations on a two-bus system (0.11% maximum steady-state error) and cross-validated against an independent PyPower droop solver on the IEEE 24-bus RTS. On the 24-bus system the surrogate attains R2 = 0.9996 for active generation and 0.0015 p.u. voltage-magnitude RMSE; scalability is confirmed on the IEEE 300-bus system (0.0036 p.u. RMSE, R2 = 0.9841 for voltage magnitude across 299,700 predictions). A three-mode control study further shows that the deadband widens the control-error distribution while leaving total droop compensation unchanged, establishing deadband width as an actionable node-level design feature.

cs.ET↗
arXiv2026

GNN-based Path-aware multi-view Circuit Learning for Technology Mapping

Traditional technology mapping suffers from systemic inaccuracies in delay estimation due to its reliance on abstract, technology-agnostic delay models that fail to capture the nuanced timing behavior behavior of real post-mapping circuits. To address this fundamental limitation, we introduce GPA(graph neural network (GNN)-based Path-Aware multi-view circuit learning), a novel GNN framework that learns precise, data-driven delay predictions by synergistically fusing three complementary views of circuit structure: And-Inverter Graphs (AIGs)-based functional encoding, post-mapping technology emphasizes critical timing paths. Trained exclusively on real cell delays extracted from critical paths of industrial-grade post-mapping netlists, GPA learns to classify cut delays with unprecedented accuracy, directly informing smarter mapping decisions. Evaluated on the 19 EPFL combinational benchmarks, GPA achieves 19.9%, 2.1% and 4.1% average delay reduction over the conventional heuristics methods (techmap, MCH) and the prior state-of-the-art ML-based approach SLAP, respectively-without compromising area efficiency.

cs.ET↗