Searcharxiv⌕ 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

From Grid to Chip: Power Architecture, Stability, and Flexibility of AI Data Centers

The rapid growth of artificial intelligence (AI) computing is transforming data centers into large, dynamic electrical loads. Their deployment is primarily constrained by energy availability and grid-connection capacity, which is further aggravated by the ability of power-delivery architectures, control systems, and computing workloads to operate reliably during fast grid disturbances. This article presents a technological perspective on AI data centers as grid-interactive computing systems. First, it reviews grid-integration bottlenecks, evolving connection policies, grid-code requirements, which has fostered new technological trends via spatio-temporal flexibility available through workload orchestration, cooling systems, on-site resources, and energy storage. Second, it maps the evolution of power-delivery architectures from medium-voltage grid interfaces to chip-level, discussing higher-voltage DC distribution, solid-state transformers, wide-bandgap devices, advanced chip-level power delivery, and liquid cooling. Third, it establishes a three-level stability framework spanning rack-level DC-bus dynamics, facility-level converter interactions, and system-level grid-coupled behavior. The framework connects dominant instability mechanisms, including constant power load effects, impedance interactions, forced oscillations, and operating-mode transitions, with suitable modeling, assessment, and mitigation approaches. Synthesizing these topics, this article highlights grid-to-chip co-design as a central requirement for scalable AI infrastructure, linking computing workloads, power-delivery systems, energy buffers, and grid operation.

cs.ET↗
arXiv2026

A Time-Based Readout for Vector-Matrix Multiplication in Fully Analog Memristive SNNs

Artificial neural networks rely on vector-matrix multiplications (VMMs), whose implementation in von Neumann architectures is dominated by costly data movement between memory and processing units. Spiking neural networks (SNNs) mitigate this bottleneck by performing in-memory, analog VMMs using memristive crossbar arrays. However, conventional current-mode readout circuits incur significant area and power overhead. This work proposes a fully analog readout architecture based on voltage-to-time conversion of the VMM output. By sensing the column voltage, the proposed approach avoids current-mode summing and scaling circuitry, improving area and energy efficiency. Post-layout simulations of a 10x1 SNN implemented in a 130 nm CMOS technology validate the proposed architecture, while application to a trained 64x10 SNN for digit classification further demonstrates its feasibility for SNN inference.

cs.ET↗
arXiv2026

Fractional-order hardware for neuromorphic computing: Is the order really the problem?

Does a neuromorphic system need a true power-law memory kernel, and if so, can anyone build one? Neuromorphic systems process signals spanning many timescales at once, from milliseconds to tens of seconds. Integer-order circuits buy each additional timescale with an additional state variable. Fractional-order dynamics offer a different bargain: one operator whose power-law kernel carries a continuum of timescales, tuned by one parameter, the order alpha. A fractional derivative is non-local, so evaluating it costs storage and arithmetic that grow with the retained history, where an integer-order derivative costs a constant. This review organizes the hardware literature around that cost. We derive the retained history needed to hold the truncation error below a tolerance epsilon, show that it scales as epsilon^(-1/alpha), and set beside it a second and independent limit on the direct form: in fixed point the weights themselves underflow, so word length caps the usable history however long the buffer is. The two limits move at very different rates with the order, and where they cross decides whether a word length can serve an order at all. We use both to sort published hardware into three strategies, note a fourth the numerical literature has developed and this hardware has not, and survey digital, analog and device work. Along the way we ask whether the field is worried about the right obstacle. It is not. Fabricated constant-phase devices already span the orders two groups identify as task-optimal, so the order gap has largely closed, leaving a residual gap near 0.1 and at the lower order describing cortical adaptation. What remains is a frequency-band gap of about three decades at the low end. That corner is not empty, since double-layer electrodes work there, but every device in it is discrete, and no integrable thin-film element has been characterized there.

cs.ET↗