Pith. sign in

REVIEW 5 major objections 5 minor 66 references

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

T0 review · 5 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proposes a reusable framework for formally modelling and verifying Metaverse applications with hierarchical colored Petri nets, and demonstrates it on an air-traffic-control case study.

desk verdict Reasonable high-level idea—hierarchical CPNs as a template for Metaverse modelling—but the ATC verification evidence is internally inconsistent and does not support the central claim. read the letter →

arxiv 2509.10936 v1 pith:DJBOD2RE submitted 2025-09-13 cs.ET

Maryam Amin , Umara Noor , Zahid Rashid , Jorn Altmann This is my paper
classification cs.ET
keywords MetaverseFormalmodellingverificationHierarchicalcoloredPetrinetsAirtrafficcontrolState-spaceanalysisLiveness/reachability/boundednessModelchecking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Metaverse applications are highly distributed and safety-critical, but they are usually deployed without formal guarantees. This paper proposes a framework, FoMAV, that uses hierarchical colored Petri nets to model all layers of a Metaverse application and to verify correctness properties before implementation. The framework is demonstrated on an air-traffic-control Metaverse, where the authors build subnets for the controller, network, Metaverse engine, virtual environment, physical world, and cloud server, and check liveness, reachability, boundedness, concurrency, safety, and session termination. The paper concludes that the framework can serve as a reusable template for mathematical verification of other complex Metaverse applications, so that design flaws are caught early.

What carries the argument

Hierarchical colored Petri nets (CPNs) with substitution transitions and a user-defined PACKET colour. A CPN token carries a typed value; here each token is a tuple (receiver, data, flag) that encodes a command. Substitution transitions let the model be decomposed into subnets, one per Metaverse layer and per ATC component, so the whole application is represented as a hierarchical net. State-space analysis of this net is the mechanism that yields the liveness, reachability, boundedness, and model-checking results.

What would settle it

Rerun the state-space analysis after adding realistic network behavior to the network subnet (e.g., packet loss, reordering, or delay). If a dead marking appears, or if the safety property 'the Cloud Server makes predictions only after the Metaverse Engine sends all required parameters' fails, then the paper's liveness and safety results rely on the idealized no-loss network assumption and do not transfer to the real system.

Watch

Extended reading notes

Core claim

At the center of the paper is the claim that a single hierarchical colored Petri net model can represent the behavior of a complete Metaverse application—physical world, virtual world, Metaverse engine, and infrastructure—as coordinated subnets, and that the same model can be reused as a template. The ATC case study instantiates this template: a special PACKET token type (receiver, data, command flag) flows through subnets for the ATC controller, the network, the Metaverse engine, the virtual environment, the physical world, and the cloud server. State-space analysis and ASK-CTL model checking verify that the model is live, reachable, and bounded, and that specific safety properties hold, su

Load-bearing premise

The load-bearing premise is that the hierarchical CPN model faithfully captures the safety-relevant behavior of the real ATC Metaverse—the paper assumes all subsystems set their states contingent on the controller's authorization and abstracts the network as a reliable packet forwarder; if those abstractions omit realistic failures, the verified properties do not transfer to the actual application.

Editorial extensions

If this is right

  • Metaverse applications can be formally verified before deployment, reducing the risk of runtime failures in safety-critical domains.
  • The four-layer architecture plus PACKET communication pattern gives a starting template; a new Metaverse application can reuse the subnets for layers it shares and replace only domain-specific parts.
  • The verified properties provide concrete guarantees for the ATC Metaverse model: no deadlock in the modelled scenarios, bounded token counts in each subnet, mutual exclusion of initialization and refresh, and prompt session termination.
  • Formal modelling at the design stage can expose dead states and unreachable subnets that correspond to design flaws, making fixes cheaper than after implementation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The template claim is supported by only one case study; testing it on a second, non-ATC Metaverse application (e.g., remote healthcare or virtual collaboration) would show whether the framework generalizes.
  • The guarantees are about the model, not a deployed system; transferring them requires a refinement or abstraction relation that the paper does not provide.
  • The state-space sizes in the liveness and boundedness tables indicate that state explosion is already a practical concern, so a scalability benchmark (number of subnets and tokens versus state-space nodes) would clarify the framework's ceiling.
  • Formalizing the security-and-privacy pillar with the same CPN pattern could yield verifiable access-control and data-protection properties; the paper leaves this to future work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 5 minor

Summary. The paper proposes a framework, FoMAV, for formal modelling and verification of Metaverse applications using hierarchical coloured Petri nets (CPNs). The framework extends a seven-layer Metaverse architecture into four CPN subnets (Physical World, Virtual World, Metaverse Engine, Infrastructure) plus two pillars. The authors define a PACKET colour type and verify a case study of an Air Traffic Control (ATC) Metaverse using CPN Tools. The verification claims include state-space construction, liveness analysis (dead markings/transitions), boundedness analysis, and ASK-CTL model checking of concurrency, safety, and reachability properties. The abstract concludes that the framework can serve as a template for mathematical verification of complex Metaverse applications.

Significance. If the framework and its verification were rigorous, this would fill a genuine gap: there is little formal modelling work for Metaverse systems, and hierarchical CPNs are a reasonable choice for distributed, concurrent, safety-critical applications. The paper also makes the alleged model available on GitHub (ref [23]), which is a constructive step. However, the formal definitions in Section 4 are placeholders, and the verification evidence in Section 5 is internally inconsistent and conceptually confused. The central claim is therefore not supported by the present manuscript.

major comments (5)
  1. [§5.2.1 and Table 5] The paper reports two irreconcilable state-space sizes for the same model. §5.2.1 states that 'The formal ATC Metaverse generated a state space consisting of 210 nodes and 553 arcs,' while Table 5 lists 2235 nodes/7571 arcs for input 0, 1515/4754 for input 1, 2235/7061 for input 2, and 1305/4083 for input 3. A CPN model with a fixed initial marking has one full state space; if the inputs correspond to different initial markings, the 210-node count is unexplained, and if they do not, the Table 5 counts cannot all describe the same model. This inconsistency makes it impossible to determine which state space was actually verified.
  2. [§5.2.2 and Table 5] The liveness analysis conflates dead transitions with dead markings. Table 5's 'Dead States' column lists transitions such as 'Caching' and 'Get Tutorials', and the text justifies them as 'must be dead logically' because the given input does not exercise them. The paper itself defines a dead marking as a marking with no enabled transitions and a dead transition as a transition disabled in every reachable marking. These are distinct notions, and neither is established by noting that an input does not use a feature. The conclusion that the model 'demonstrates correct behaviour from the perspective of liveness' is therefore unsupported.
  3. [§5.2.3 and Table 6] The boundedness analysis is self-contradictory. The text states that 'the unreachable subnets for a specific input remained unbounded with a value 0' and that such a subnet 'must be unbound'. A place with no tokens in the reachable state space has an upper integer bound of 0, which is bounded, not unbounded. Unreachability of a subnet does not imply unboundedness. Hence the claim that the model 'demonstrated correct behaviour from the perspective of boundedness' is not supported by the data.
  4. [§4.3–§4.6] The formal definitions of the subnets are placeholders rather than CPN specifications. Each tuple (e.g., Cp in §4.3) is defined with generic sets Pp={pw1,…,pwn}, Tp={tw1,…,twn}, Ap={aw1,…,awn} and 'n ∈ Z+' without giving concrete elements, guards are written as '{} | BOOL' and arc expressions as '{} | BOOL', which are not well-formed CPN expressions. The same pattern is repeated for Cv, Cm, and Ci. The paper does not provide the CPN ML declarations, concrete places/transitions, or initial marking of the ATC model; the figures in §5.1 are informal diagrams. The framework's formal foundation is therefore underspecified.
  5. [§5.1.1] No abstraction or refinement relation is given between the ATC Metaverse and the CPN model. The paper asserts that 'It is assumed that all other subsystems set their states contingent upon the controller's authorization' (§5.1.1), but this is an unverified modelling assumption, not a formal relation. Even if all reported state-space properties were correct, they concern the CPN model only; without a conformance or refinement relation, they do not transfer to the actual Metaverse application. This gap is load-bearing for the abstract's claim that the framework can be used as a template for mathematical verification of Metaverse applications.
minor comments (5)
  1. [§5.2.4(c)] The opening sentence of the Reachability Property subsection says 'Liveness is the property that ...' but the subsection is about reachability. This puzzling wording should be corrected.
  2. [§6] 'CNP combines Petri Nets with a programming language' — 'CNP' should be 'CPN'. The paper also switches inconsistently between 'colored' and 'coloured'.
  3. [§4.6] The initialization function is written as Ii = {(pi1, PACKET} with an unmatched brace; the notation needs fixing.
  4. [§5.2.4] The ASK-CTL model-checking descriptions are too informal. For example, the concurrency property is said to be evaluated by checking 'whether the state space contains independent paths with non-overlapping states', but the actual CTL formula is not shown. Providing the concrete ASK-CTL queries would make the checks reproducible.
  5. [§5.2.1, Figure 12] Figure 12 is described as showing only the first few nodes of the state space; a full state-space report or a link to the reproducible script would be more informative.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the verification pipeline is independent of its inputs, though its technical soundness is questionable.

full rationale

The paper's derivation chain is not circular. The FoMAV framework is defined generically in Section 4 and then applied to an ATC case study in Section 5; the case study is instantiated from the framework rather than being used to define the framework. Verification is performed with CPN Tools as an external model checker: a state space is generated, and separately stated properties (concurrency, safety, reachability) are checked as queries over that state space. These properties are not constructed to be true by definition; they could in principle fail. The liveness and boundedness sections contain serious interpretive errors (e.g., calling an unreachable place with bound 0 'unbounded' in Section 5.2.3, and labeling unused transitions as 'dead states' that are 'logically dead' in Section 5.2.2), but these are correctness/soundness defects in the verification argument, not circular reductions of the claimed result to its own inputs. The 'template' conclusion in Section 6 is a generalization from a single case study, which is weak inductive support but not circular reasoning. Reference [35] supplies domain conflict scenarios, but that prior work is not load-bearing for the formal verification claim. Therefore, no step reduces to its own input, and the circularity score is 0.

Assumptions & free parameters 2 free parameters · 5 assumptions · 1 invented entities

The central claim rests on the authors' architectural assumptions (four-layer completeness), the expressiveness of the PACKET tuple, the faithfulness of the CPN abstraction, and the reliability of CPN Tools. No external benchmarks or independent artifacts are provided beyond the authors' own GitHub reference.

free parameters (2)
  • Command flag encoding = 0=create virtual environment, 1=avatar movement, 2=get recommendations, 3=get cached tutorials
    Chosen by hand in Section 5.1.2 to distinguish command types in the PACKET tuple; it drives guards and the resulting state space.
  • Initial marking token counts = e.g., 1`("ATC","DATA",0) in the main net; subnet-specific initializations implied by state-space counts
    Initial token configurations are author-specified for the ATC case study and determine the generated state space and boundedness values (Sections 5.1, 5.2).
assumptions (5)
  • domain assumption The four-layer Metaverse architecture (Infrastructure, Metaverse Engine, Virtual World, Physical World) with two pillars is complete for arbitrary Metaverse applications.
    Invoked in Sections 3 and 6, where the framework claims applicability to Metaverse applications of 'any complexity'.
  • domain assumption Hierarchical CPN with the PACKET color set captures all behavior of Metaverse inter-layer communication.
    Section 4.1 defines PACKET as (receiver, data, flag); the paper assumes every interaction reduces to this tuple.
  • domain assumption CPN Tools' state-space and ASK-CTL model checking correctly answer reachability, liveness, boundedness, and CTL queries.
    Section 5.2 relies on CPN Tools' built-in analysis without independent theorem proving or formal proof certificates.
  • ad hoc to paper All subsystems set their states contingent upon the controller's authorization.
    Stated in Section 5.1.1: 'It is assumed that all other subsystems set their states contingent upon the controller's authorization, which is pivotal in ensuring coordinated and conflict-free operation.' This constrains the model and is not derived from ATC domain requirements.
  • standard math Standard Colored Petri Net firing semantics (token availability, transition enabling, substitution transitions).
    Used implicitly throughout Section 5; standard background for CPN modelling.
invented entities (1)
  • PACKET tuple (Receiver STRING, Data STRING, Flag INT)
    purpose: Encodes all messages between Metaverse layers and subnets; the flag integer encodes command type.
    Introduced in Section 4.1 as the only color set; it shapes every transition and guard. No independent evidence that it captures real Metaverse protocols; it is a modeling device.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Framework for Formal Modelling of Metaverse Applications Using Hierarchical Colored Petri Nets." pith.science (2026). https://pith.science/paper/DJBOD2RE

@misc{pith2026250910936,
  author       = {Pith},
  title        = {Pith review of: Framework for Formal Modelling of Metaverse Applications Using Hierarchical Colored Petri Nets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DJBOD2RE}},
  note         = {Machine review of arXiv:2509.10936}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2509.10936 by the authors.

Figure 1
Figure 1. Layers of Metaverse 2.2. Architecture of Metaverse For this study, the capabilities of existing frameworks in the domain of the Metaverse are explored ( [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Proposed architecture of Metaverse 3.1. Infrastructure Layer The infrastructure layer is the core layer of the Metaverse and provides basic functionalities of communication, computation, and storage. Computation is an extensive set of services offered by Metaverse from data gathering to rendering data and videos for providing an immersive experience to users that require expensive computations to be performed by pro… view at source ↗
Figure 3
Figure 3. Hierarchical Representation of Proposed Metaverse Architecture [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (12 more)
Figure 4
Figure 4. Figure 4: Conceptual diagram of air traffic control (ATC) Metaverse, which has been derived from the Metaverse framework. Starting from services of the top most layer named the “Physical Layer” of the Metaverse, which primarily provides integrated access to a digital world for A…
Figure 5
Figure 5. Figure 5: Main hierarchical Petri net developed for the ATC Metaverse [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: Subnet ATC controller developed for the ATC Metaverse. 5.1.3. B5G Network The ultra-high-speed Internet called B5G (Beyond 5G also called 6G) is abstracted through a subnet named B5G Network ( [PITH_FULL_IMAGE:figures/full_fig_p018_6.png]
Figure 7
Figure 7. Figure 7: Subnet B5G Network developed for the ATC Metaverse. 5.1.4. Metaverse Engine It is the hub of the Metaverse system that is formalized by the subnet named Metaverse Engine ( [PITH_FULL_IMAGE:figures/full_fig_p019_7.png]
Figure 8
Figure 8. Figure 8: Subnet Metaverse Engine developed for the ATC Metaverse. 5.1.5. Virtual Environment The virtual environment is represented by a subnet named Virtual Environment ( [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]
Figure 9
Figure 9. Figure 9: Subnet Virtual Environment developed for the ATC Metaverse. 5.1.6. Physical Environment The formalization of the physical world is shown by the subnet Physical World ( [PITH_FULL_IMAGE:figures/full_fig_p020_9.png]
Figure 10
Figure 10. Figure 10: Subnet Physical World developed for the ATC Metaverse. 5.1.7. Cloud Server The formalization of the Cloud Server is shown by the subnet Cloud Server ( [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Subnet Cloud Server developed for the ATC Metaverse. 5.2. Verification of ATC Metaverse Model CPN Tools are a toolset for analysing the dynamic behaviour of a system’s model through a deep inspection of critical properties such as concurrency, synchronization, and con…
Figure 12
Figure 12. Figure 12: State space graph of the ATC Metaverse model [PITH_FULL_IMAGE:figures/full_fig_p021_12.png]
Figure 13
Figure 13. Figure 13: Formalization of the concurrency property in the ATC Metaverse model. The defined concurrency property is evaluated via Execute ML command of state space tool, which investigates whether the state space contains independent paths with non-overlapping states. First, it…
Figure 14
Figure 14. Figure 14: Formalization of safety property for the ATC Metaverse model. This property is evaluated via Execute ML command of state space tool which investigates whether, the state space contains a directed path from a place named loading parameters of subnet Metaverse Engine. I…
Figure 15
Figure 15. Figure 15: Fig.15 [PITH_FULL_IMAGE:figures/full_fig_p024_15.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

66 extracted references · 2 linked inside Pith

  1. [23]

    https://github.com/Maryam-IIUI/FM-Metaverse.git

  2. [1]

    Coronato, and De Pietro, G

    A. Coronato, and De Pietro, G. (2011). Formal specification and verification of ubiquitous and pervasive systems. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 6(1), 1-6

    2011

  3. [2]

    Hall (2007)

    A. Hall (2007). Realising the Benefits of Formal Methods. J. Univers. Comput. Sci., 13(5), 669-678

    2007

  4. [3]

    Houser, Ma, L

    A. Houser, Ma, L. M., Feigh, K. M., and Bolton, M. L. (2018). Using formal methods to reason about taskload and resource conflicts in simulated air traffic scenarios. Innovations in Systems and Software Engineering, 14, 1-14

    2018

  5. [4]

    Jarrar and Balouki, Y

    A. Jarrar and Balouki, Y. (2018). Towards sophisticated air traffic control system using formal methods. Modelling and Simulation in Engineering, 2018

    2018

  6. [5]

    Jarrar, Ait Wakrime, A., and Balouki, Y

    A. Jarrar, Ait Wakrime, A., and Balouki, Y. (2020). Formal approach to model complex adaptive computing systems. Complex Adaptive Systems Modeling, 8(1), 3

    2020

  7. [6]

    Martín Montes, Burbano Cendales, A

    A. Martín Montes, Burbano Cendales, A. M., and León de Mora, C. (2017). An Intelligent Methodology for Modeling Semantic Knowledge in Industrial Networks. WSEAS Transactions on Computers, 16, 179-188

    2017

  8. [7]

    Rehman (2021)

    A. Rehman (2021). Machine learning based air traffic control strategy. International Journal of Machine Learning and Cybernetics, 12, 2151-2161

    2021

Show all 66 references
  1. [8]

    Siyaev and Jo, G

    A. Siyaev and Jo, G. S. (2021). Towards aircraft maintenance metaverse using speech interactions with virtual objects in mixed reality. Sensors, 21(6), 2066

    2021

  2. [9]

    Souri, Rahmani, A

    A. Souri, Rahmani, A. M., Navimipour, N. J., and Rezaei, R. (2020). A hybrid formal verification approach for QoS-aware multi-cloud service composition. Cluster Computing, 23, 2453-2470

    2020

  3. [10]

    Kye, Han, N., Kim, E., Park, Y., and Jo, S

    B. Kye, Han, N., Kim, E., Park, Y., and Jo, S. (2021). Educational applications of metaverse: possibilities and limitations. Journal of educational evaluation for health professions, 18

    2021

  4. [11]

    Vogel-Heuser, Huber, C., Cha, S., and Beckert, B

    B. Vogel-Heuser, Huber, C., Cha, S., and Beckert, B. (2021, July). Integration of a formal specification approach into CPPS engineering workflow for machinery validation. In 2021 IEEE 19th International Conference on Industrial Informatics (INDIN) (pp. 1-8)

    2021

  5. [12]

    C. B. Fernandez and Hui, P., 2022, July. Life, the Metaverse and everything: An overview of privacy, ethics, and governance in Metaverse. In 2022 IEEE 42nd International Conference on Distributed Computing Systems Workshops (ICDCSW) (pp. 272-277). IEEE

    2022

  6. [13]

    Mahmoudi, Mourlin, F., and Battou, A

    C. Mahmoudi, Mourlin, F., and Battou, A. (2018, April). Formal definition of edge computing: An emphasis on mobile cloud and IoT composition. In 2018 Third international conference on fog and mobile edge computing (FMEC) (pp. 34-42)

    2018

  7. [14]

    Ivanov and Dolgui, A., 2021

    D. Ivanov and Dolgui, A., 2021. A digital supply chain twin for managing the disruption risks and resilience in the era of Industry 4.0. Production Planning and Control, 32(9), pp.775-788

    2021

  8. [15]

    D. L. Parnas (2010). Really rethinking' formal methods'. Computer, 43(1), 28-34

    2010

  9. [16]

    Liu, Zhu, H., Xu, C., Bayley, I., Lightfoot, D., Green, M., and Marshall, P

    D. Liu, Zhu, H., Xu, C., Bayley, I., Lightfoot, D., Green, M., and Marshall, P. (2016, June). Cide: An integrated development environment for microservices. In 2016 IEEE International Conference on Services Computing (SCC) (pp. 808-812)

    2016

  10. [17]

    Li, 2020

    F. Li, 2020. Leading digital transformation: three emerging approaches for managing the transition. International Journal of Operations and Production Management, 40(6), pp.809-817

    2020

  11. [18]

    Li, 2020

    F. Li, 2020. The digital transformation of business models in the creative industries: A holistic framework and emerging trends. Technovation, 92, p.102012

    2020

  12. [19]

    Vial, 2021

    G. Vial, 2021. Understanding digital transformation: A review and a research agenda. Managing Digital Transformation, pp.13-66

    2021

  13. [20]

    Garavel, Beek, M

    H. Garavel, Beek, M. H. T., and Pol, J. V. D. (2020). The 2020 expert survey on formal methods. In Formal Methods for Industrial Critical Systems: 25th International Conference, FMICS 2020, Vienna, Austria, September 2–3, 2020, Proceedings 25 (pp. 3-69). Springer International...

    2020

  14. [21]

    Ning, Wang, H., Lin, Y., Wang, W., Dhelim, S., Farha, F.,

    H. Ning, Wang, H., Lin, Y., Wang, W., Dhelim, S., Farha, F., ... and Daneshmand, M. (2021). A Survey on Metaverse: The State-of-the-art, Technologies, Applications, and Challenges. arXiv preprint arXiv:2111.09673

    2021 arXiv

  15. [22]

    https://formalmethods.fandom.com/wiki/Companies (last visited: 06-02-2023)

    2023

  16. [24]

    https://www.frequentis.com/en/air-traffic-management/digital-experience

  17. [25]

    https://www.reuters.com/technology/boeing-wants-build-its-next-airplane-metaverse-2021-12-17/

    2021

  18. [26]

    I. A. Akour, Al-Maroof, R. S., Alfaisal, R., and Salloum, S. A. (2022). A conceptual framework for determining metaverse adoption in higher institutions of gulf area: An empirical study using hybrid SEM-ANN approach. Computers and Education: Artificial Intelligence, 3, 100052

    2022

  19. [27]

    Cafezeiro, Viterbo, J., Rademaker, A., Haeusler, E

    I. Cafezeiro, Viterbo, J., Rademaker, A., Haeusler, E. H., and Endler, M. (2014). Specifying ubiquitous systems through the algebra of contextualized ontologies. The Knowledge Engineering Review, 29(2), 171-185. 27

    2014

  20. [28]

    J. D. N. Dionisio, III, W. G. B., and Gilbert, R. (2013). 3D virtual worlds and the metaverse: Current status and future possibilities. ACM Computing Surveys (CSUR), 45(3), 1-38

    2013

  21. [29]

    Holmström, Holweg, M., Lawson, B., Pil, F.K

    J. Holmström, Holweg, M., Lawson, B., Pil, F.K. and Wagner, S.M., 2019. The digitalization of operations and supply chain management: Theoretical and methodological implications. Journal of Operations Management, 65(8), pp.728-734

    2019

  22. [30]

    Huang, Xue, J., You, Z., and Zhou, Z

    J. Huang, Xue, J., You, Z., and Zhou, Z. (2021, June). Design and Implementation of Virtual Reality Geometric Modeling in Apla+ VR. In Structured Object-Oriented Formal Language and Method: 10th International Workshop, SOFL+ MSVL 2020, Singapore, March 1, 2021, Revised Selecte...

    2021

  23. [31]

    Kim (2021)

    J. Kim (2021). Advertising in the metaverse: Research agenda. Journal of Interactive Advertising, 21(3), 141-144

    2021

  24. [32]

    J. L. Peterson (1977). Petri nets. ACM Computing Surveys (CSUR), 9(3), 223-252

    1977

  25. [33]

    Maryam and Zafar, N

    J. Maryam and Zafar, N. A. (2016, October). Formalizing the resurrecting duckling into hierarchical coloured Petri nets. In 2016 International Conference on Emerging Technologies (ICET) (pp. 1-6). IEEE

    2016

  26. [34]

    Maryam and Zafar, N

    J. Maryam and Zafar, N. A. (2017, March). Extending agent-based Mobile Petri Nets with access control. In 2017 International Conference on Communication, Computing and Digital Systems (C-CODE) (pp. 133-138). IEEE

    2017

  27. [35]

    Maryam, Zafar N

    J. Maryam, Zafar N. A., Rahman A., Musleh D., Gollapalli M. A., and Chabani S. (2022). Modeling and verification of aircraft takeoff through novel quantum nets. Computers, Materials and Continua, 72(2), 3331-3348

    2022

  28. [36]

    K. D. Setiawan and Anthony, A. (2022, August). The essential factor of metaverse for business based on 7 layers of metaverse–systematic literature review. In 2022 International Conference on Information Management and Technology (ICIMTech) (pp. 687-692). IEEE

    2022

  29. [37]

    Singh and Auernheimer, B

    K. Singh and Auernheimer, B. (2016). Formal specification of Multi-Window user interface in PVS. In HCI International 2016–Posters' Extended Abstracts: 18th International Conference, HCI International 2016, Toronto, Canada, July 17-22, 2016, Proceedings, Part I 18 (pp. 144-149...

    2016

  30. [38]

    Brunese, Mercaldo, F., Reginelli, A., and Santone, A

    L. Brunese, Mercaldo, F., Reginelli, A., and Santone, A. (2019). A blockchain based proposal for protecting healthcare systems through formal methods. Procedia Computer Science, 159, 1787-1794

    2019

  31. [39]

    L. E. G. Martins and Gorschek, T. (2016). Requirements engineering for safety-critical systems: A systematic literature review. Information and software technology, 75, 71-89

    2016

  32. [40]

    Elgaard, 2002

    L. Elgaard, 2002. The Symmetry Method for Coloured Petri Nets. DAIMI Report Series, (564)

    2002

  33. [41]

    Bourlakis, Papagiannidis, S., and Li, F

    M. Bourlakis, Papagiannidis, S., and Li, F. (2009). Retail spatial evolution: paving the way from traditional to metaverse retailing. Electronic Commerce Research, 9, 135-148

    2009

  34. [42]

    M. D. Petty (2018). Modeling and validation challenges for Complex Systems. In Engineering Emergence (pp. 199-216). CRC Press

    2018

  35. [43]

    Damar (2021)

    M. Damar (2021). Metaverse shape of your life for future: A bibliometric snapshot. Journal of Metaverse, 1(1), 1-8

    2021

  36. [44]

    Hendrix, Arnab, S., Dunwell, I., Petridis, P., Lameras, P., De Freitas, S., E

    M. Hendrix, Arnab, S., Dunwell, I., Petridis, P., Lameras, P., De Freitas, S., E. Knutov and Auneau, L. (2013). Integrating serious games in adaptive hypermedia applications for personalised learning experiences

    2013

  37. [45]

    Hilia, Chibani, A., Djouani, K., and Amirat, Y

    M. Hilia, Chibani, A., Djouani, K., and Amirat, Y. (2016). Formal Specification and Verification Framework for Multi-domain Ubiquitous Environment. In Service-Oriented Computing: 14th International Conference, ICSOC 2016, Banff, AB, Canada, October 10-13, 2016, Proceedings 14 ...

    2016

  38. [46]

    Vergara-Fernández, Heilmann, C., and Szymanowska, M

    M. Vergara-Fernández, Heilmann, C., and Szymanowska, M. (2023). Describing model relations: The case of the capital asset pricing model (CAPM) family in financial economics. Studies in History and Philosophy of Science, 97, 91-100

    2023

  39. [47]

    Xu, Ng, W

    M. Xu, Ng, W. C., Lim, W. Y. B., Kang, J., Xiong, Z., Niyato, D., Yang Q., Sherman S. X., and Miao, C. (2022). A full dive into realizing the edge-enabled metaverse: Visions, enabling technologies, and challenges. IEEE Communications Surveys and Tutorials

    2022

  40. [48]

    Akhtar and Missen, M

    N. Akhtar and Missen, M. M. S. (2015). Contribution to the formal specification and verification of a multi-agent robotic system. arXiv preprint arXiv:1604.05577

    2015 arXiv

  41. [49]

    Fulton and Platzer, A

    N. Fulton and Platzer, A. (2018, April). Safe reinforcement learning via formal methods: Toward safe control through proof and learning. In Proceedings of the AAAI Conference on Artificial Intelligence (Vol. 32, No. 1)

    2018

  42. [50]

    S. A. Seshia, Desai, A., Dreossi, T., Fremont, D. J., Ghosh, S., Kim, E., Sumukh S., Marcell V., and Yue X. (2018). Formal specification for deep neural networks. In Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, U...

    2018

  43. [51]

    Braithwaite, Buchman, E., Konnov, I., Milosevic, Z., Stoilkovska, I., Widder, J., and Zamfir, A

    S. Braithwaite, Buchman, E., Konnov, I., Milosevic, Z., Stoilkovska, I., Widder, J., and Zamfir, A. (2020). Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020...

    2020

  44. [52]

    Hollensen, Kotler, P., and Opresnik, M

    S. Hollensen, Kotler, P., and Opresnik, M. O. (2022). Metaverse–the new marketing universe. Journal of Business Strategy, (ahead-of- print)

    2022

  45. [53]

    Liu and Miao, W

    S. Liu and Miao, W. (2021). A formal specification animation method for operation validation. Journal of Systems and Software, 178, 110948. 28

    2021

  46. [54]

    Pourtalebi and Horváth, I

    S. Pourtalebi and Horváth, I. (2016). Towards a methodology of system manifestation features-based pre-embodiment design. Journal of Engineering Design, 27(4-6), 232-268

    2016

  47. [55]

    Hess, Matt, C., Benlian, A

    T. Hess, Matt, C., Benlian, A. and Wiesböck, F., 2016. Options for formulating a digital transformation strategy. MIS Quarterly Executive, 15(2)

    2016

  48. [56]

    Neroda, (2020, April)

    T. Neroda, (2020, April). Filing of Formal Model for Educational and Methodical Materials Content Stuff in Academic Information Space. In the XI th International scientific and practical conference Theoretical Foundations of Modern Science and Practice, (06-07 April 2020) Melb...

    2020

  49. [57]

    Sun and Yu, W

    T. Sun and Yu, W. (2020). A formal verification framework for security issues of blockchain smart contracts. Electronics, 9(2), 255

    2020

  50. [58]

    Gehlot (2019, December)

    V. Gehlot (2019, December). From petri NETS to colored petri NETS: A tutorial introduction to NETS based formalism for modeling and simulation. In 2019 Winter, Simulation Conference (WSC) (pp. 1519-1533). IEEE

    2019

  51. [59]

    Classification of formal specification methods

    V. S. Alagar, Periyasamy, K. V. S. Alagar, and K. Periyasamy. (2011). "Classification of formal specification methods." Specification of Software Systems: 129-134

    2011

  52. [60]

    Nam and Kil, H

    W. Nam and Kil, H. (2022). Formal verification of blockchain smart contracts via ATL model checking. IEEE Access, 10, 8151-8162

    2022

  53. [61]

    W. Y. B. Lim, Xiong, Z., Niyato, D., Cao, X., Miao, C., Sun, S., and Yang, Q. (2022). Realizing the metaverse with edge intelligence: A match made in heaven. IEEE Wireless Communications

    2022

  54. [62]

    World Wide Web Virtual Library on Formal Methods, http://www.cfdvs.iitb.ac.in/download/Docs/net/www.comlab.ox.ac.uk/formal- methods.html (last visited: 06-02-2023)

    2023

  55. [63]

    Sun, Khedr, H., and Shoukry, Y

    X. Sun, Khedr, H., and Shoukry, Y. (2019, April). Formal verification of neural network controlled autonomous systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (pp. 147-156)

    2019

  56. [64]

    Y. K. Dwivedi, Hughes, L., Baabdullah, A. M., Ribeiro-Navarrete, S., Giannakis, M., Al-Debei, M. M., ... and Wamba, S. F. (2022). Metaverse beyond the hype: Multidisciplinary perspectives on emerging challenges, opportunities, and agenda for research, practice and policy. Inte...

    2022

  57. [65]

    Liu and Liu, J

    Z. Liu and Liu, J. (2019, July). Formal verification of blockchain smart contract based on colored petri net models. In 2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC) (Vol. 2, pp. 555-560)

    2019

  58. [66]

    Peng, Lu, Y., Miller, A., Zhao, T., and Johnson, C

    Z. Peng, Lu, Y., Miller, A., Zhao, T., and Johnson, C. (2016). Formal specification and quantitative analysis of a constellation of navigation satellites. Quality and Reliability Engineering International, 32(2), 345-361

    2016

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.