{"id":"ffad01b4-4b8b-415f-b2a1-093c70a0d1d7","arxiv_id":"2509.10936","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":2,"one_line_summary":"The paper defines a hierarchical colored Petri net framework for Metaverse applications and reports verified liveness, reachability, and boundedness for an ATC Metaverse case study, but the verification evidence is internally inconsistent.","lead":"This paper proposes a framework for formally modeling Metaverse applications with hierarchical colored Petri nets, and demonstrates it on an air-traffic-control case study. A generalist might read it to see whether formal verification can bring safety guarantees to Metaverse systems, and to learn where such claims currently fall short.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The verification evidence is internally inconsistent and technically invalid, so the framework's central claim is unsupported.","rationale":"The reader's weakest_assumption highlights model fidelity, which is a legitimate concern: without an abstraction or refinement relation, even a sound verification of the CPN model would not necessarily say anything about the real ATC Metaverse. However, the more immediate and decisive problem is that the verification results are internally inconsistent and misuse fundamental CPN concepts. The state-space size discrepancy alone undermines the reproducibility of the results, while the liveness and boundedness analyses are based on incorrect definitions: dead transitions are presented as dead markings, and a bound of zero is described as 'unbounded'. The reachability check is tautological because any state in the generated state space is reachable by construction. These are load-bearing defects because they affect the core contribution, namely the claim that the framework provides mathematical verification. If these checks were corrected and the model artifacts supplied, the framework might be salvageable, but in its current form the verification evidence does not support the central claim. Since the reader already recommends REJECT, my analysis does not change the verdict.","tokens_in":22732,"tokens_out":3483,"duration_ms":39575,"concrete_test":"Obtain the CPN Tools model from the GitHub repository referenced in [23], re-run the state-space analysis with the initial marking corresponding to Input 0 in Table 5, and compare the generated node/arc counts and the set of dead markings with Section 5.2.1 and Table 5. If the counts differ from the reported 210/553 or 2235/7571, or if the entries listed as 'dead states' are not actual dead markings in the generated state space, the verification evidence is invalidated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that the hierarchical CPN framework can serve as a template for mathematical verification, supported by the ATC case study. That claim requires the state-space analysis to constitute genuine verification of liveness, boundedness, and reachability. The weakest load-bearing point is that the verification evidence itself is not sound, independent of model fidelity. Section 5.2.1 reports a state space of 210 nodes and 553 arcs, but Table 5 lists 2235/7571, 1515/4754, 2235/7061, and 1305/4083 nodes/arcs for the same model under different inputs; a single CPN model has one full state space, so these counts cannot all be correct. The liveness analysis in Table 5 labels transitions such as 'Caching' and 'Get Tutorials' as 'dead states' and justifies them as logically dead because a particular input does not exercise them, which conflates dead transitions with dead markings and does not constitute a liveness proof. The boundedness analysis states that unreachable subnets 'remained unbounded with a value 0'; an unreachable place with zero tokens has an upper bound of 0, which is bounded, not unbounded. The reachability property is checked by asking whether there exists a path to a state that is already in the reachability graph; such a check cannot fail and is vacuous. These are not typographical slips: they mean the reported verification does not establish the claimed properties. If the verification evidence is invalid, the template claim is unsupported regardless of whether the model faithfully represents the ATC Metaverse.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":23030,"tokens_out":6733,"duration_ms":66478,"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":[{"comment":"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.","section":"§5.2.1 and Table 5"},{"comment":"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.","section":"§5.2.2 and Table 5"},{"comment":"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.","section":"§5.2.3 and Table 6"},{"comment":"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.","section":"§4.3–§4.6"},{"comment":"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.","section":"§5.1.1"}],"minor_comments":[{"comment":"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.","section":"§5.2.4(c)"},{"comment":"'CNP combines Petri Nets with a programming language' — 'CNP' should be 'CPN'. The paper also switches inconsistently between 'colored' and 'coloured'.","section":"§6"},{"comment":"The initialization function is written as Ii = {(pi1, PACKET} with an unmatched brace; the notation needs fixing.","section":"§4.6"},{"comment":"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.","section":"§5.2.4"},{"comment":"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.","section":"§5.2.1, Figure 12"}],"recommendation":"reject","confidential_remarks":"The formal verification core is the main advertised contribution, and it is not sound in its current form. The state-space counts are inconsistent, the liveness and boundedness arguments confuse basic Petri net notions, and the formal model definitions do not specify a concrete net. These are not local presentation issues; a correct version would require redoing the case study and formalization. If the GitHub repository contains a complete, executable CPN model, that could be the basis for a substantially revised submission."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper has a legitimate new application—hierarchical coloured Petri nets to a Metaverse ATC system—but the verification evidence as presented is internally inconsistent and does not support the central claim. The framework idea is reasonable; the execution is not.\n\nWhat is genuinely new: applying HCPNs to a Metaverse ATC application, the PACKET colour set, and the layer-wise subnet decomposition. The architecture extends Xu et al. with formal modelling/verification and security/privacy pillars. The case study is detailed, with subnets for the ATC controller, B5G network, Metaverse engine, virtual environment, physical world, and cloud server. The literature gap discussion is solid and honest.\n\nThe soft spots are load-bearing. Section 4's formal definitions are placeholders: sets like {pw1,…,pwn} with n unspecified do not define a concrete net. More seriously, the state-space numbers contradict each other: Section 5.2.1 reports 210 nodes and 553 arcs, while Table 5 lists 2235/7571, 1515/4754, 2235/7061, and 1305/4083 for the same model under different inputs. A single CPN model has one full state space; these counts cannot all be correct. The liveness analysis labels transitions like Caching and Get Tutorials as \"dead states\" and justifies them as logically dead because a particular input does not exercise them—but dead transitions are not dead markings, and this does not constitute a liveness proof. The boundedness analysis says unreachable subnets \"remained unbounded with a value 0.\" An unreachable place with zero tokens has upper bound 0, which is bounded, not unbounded. The reachability check appears vacuous if it merely asks whether there is a path to a state already in the reachability graph. Finally, there is no refinement or abstraction relation between the real ATC Metaverse and the net; the paper asserts model fidelity rather than arguing for it. The abstract's \"any complexity\" claim is an overclaim unsupported by one small model.\n\nCredit where due: the paper is transparent about the state explosion limitation, and the architectural framing is clear. This is a salvageable paper if the authors provide the CPN artifacts, fix the numeric inconsistency, and redo the liveness, boundedness, and reachability analysis properly.\n\nThis is for readers interested in formal methods applied to Metaverse, especially CPN modelling. It deserves a serious referee, but with major revision and access to the model artifacts.","headline":"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.","tokens_in":23566,"tokens_out":2742,"would_cite":false,"duration_ms":31584,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Metaverse","Formal modelling","Formal verification","Hierarchical colored Petri nets","Air traffic control","State-space analysis","Liveness/reachability/boundedness","Model checking"],"falsifier":"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.","tokens_in":22562,"feed_emoji":"✈️","tokens_out":10423,"duration_ms":106935,"temperature":0.7,"pith_summary":"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.","feed_headline":"Formal model verifies a Metaverse air-traffic control system","feed_subtitle":"The same hierarchical Petri-net template could catch design flaws in other safety-critical Metaverse applications before deployment.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Petri-net template verifies any Metaverse app, from ATC to more","Formal modelling catches Metaverse design flaws before launch","One hierarchical Petri net to model any Metaverse application","Framework verifies correctness of Metaverse apps with Petri nets","Metaverse safety: formal model template for air-traffic control"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Petri-net template verifies any Metaverse app, from ATC to more","Formal modelling catches Metaverse design flaws before launch","One hierarchical Petri net to model any Metaverse application","Framework verifies correctness of Metaverse apps with Petri nets","Metaverse safety: formal model template for air-traffic control"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000399,"raw_usage":{"total_tokens":1947,"prompt_tokens":792,"completion_tokens":1155,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":536,"completion_tokens_details":{"reasoning_tokens":1070}},"tokens_in":536,"tokens_out":1155,"duration_ms":11133,"temperature":1.0,"reasoning_tokens":1070,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T17:21:31.791125+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}