pith. sign in

arxiv: 2604.08244 · v1 · submitted 2026-04-09 · 💻 cs.NI · cs.SY· eess.SY

FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services

Debarpita Banerjee , Sumana Ghosh , Snigdha Das , Shilpa Budhkar , Rana Pratap Sircar This is my paper

Pith reviewed 2026-05-10 17:32 UTC · model grok-4.3

classification 💻 cs.NI cs.SYeess.SY
keywords network slicingPRB allocationformal methodsSMT5G RANfairnessresource optimizationhierarchical partitioning
0
0 comments X

The pith

An SMT-encoded 3-layered model verifies fairness and minimal PRB waste when slicing 5G RAN resources for multiple services.

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

The paper sets out to replace ad-hoc AI solutions for radio resource allocation with a formal method that guarantees two properties: every service type receives its required share of physical resource blocks even under prioritization, and unused blocks are minimized. It does so by casting the allocation task as a satisfiability-modulo-theories problem over a fixed 3-layer hierarchy of partitions. A sympathetic reader would care because the resulting procedure is automated, works for any compatible 3-layer configuration, and supplies a machine-checkable proof that the chosen allocations meet the fairness and optimality criteria.

Core claim

By encoding the 3-layered hierarchical PRB-partitioning problem together with explicit fairness and PRB-optimality constraints into an SMT formula, the authors obtain an automated solver that returns allocations satisfying both properties for any valid network structure; formal verification then confirms that the model itself enforces these properties, yielding measurable gains over a baseline method.

What carries the argument

The FORSLICE SMT encoding of the 3-layered PRB hierarchy together with the fairness and optimality predicates, which the solver uses to produce and verify allocations.

If this is right

  • Any 3-layer network structure can be handled without redesigning the solver or the property definitions.
  • Fairness holds even after one service type is given priority, while still keeping unused PRBs low.
  • The same formal model can be re-run whenever the set of active services or their priority ordering changes.
  • System-level simulations or testbeds can use the SMT output directly as the allocation schedule.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the SMT instances remain tractable at scale, operators could recompute allocations on the order of seconds rather than relying on pre-computed tables.
  • The same layering-plus-SMT pattern could be reused for other hierarchical resource problems such as core-network slice isolation or edge-computing task placement.
  • A natural next step would be to embed the SMT model inside a closed-loop controller that reacts to measured channel quality indicators.

Load-bearing premise

The particular definitions of fairness and optimality chosen for the SMT constraints, together with the 3-layer hierarchy itself, are faithful enough to real RAN traffic and channel conditions that the returned allocations remain useful when deployed.

What would settle it

Execute the SMT solver on a concrete 3-layer configuration whose size matches a live small-cell deployment, then measure whether the produced PRB counts produce the claimed throughput ranges for each service type under realistic interference and mobility traces.

Figures

Figures reproduced from arXiv: 2604.08244 by Debarpita Banerjee, Rana Pratap Sircar, Shilpa Budhkar, Snigdha Das, Sumana Ghosh.

Figure 1
Figure 1. Figure 1: RAN slicing scenario [5QI: 5G quality identifier] In this work, we follow Ericsson’s PRB-partitioning technique [9] for RAN slicing, that divides the RAN into physical partitions, where a partition is a configured share of radio resources within a cell dedicated to spe￾cific user categories. Each partition is further comprised of logical or virtual segments called slices based on the user category. For exa… view at source ↗
Figure 2
Figure 2. Figure 2: 3-layered hierarchical network structure for the RAN-slicing scenario portrayed in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The proposed 3-layered framework, FORSLICE, for the sample example of 3 service types, 2 partitions and 2 slices per partition [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: FORSLICE: Automated design workflow Moreover, for modeling purposes, we make a key assump￾tion: we scale the user count to a unit range in our model as￾suming transition of at most one user (i.e., one UE can enter or leave a slice) per timestep 𝑡. This simplification is essential for model abstraction, functioning similarly to how we might scale large data inputs (e.g., aggregating 1000 users into a sin￾gl… view at source ↗
Figure 5
Figure 5. Figure 5: The final residual partition share for different PRB counts in four (𝒮,𝒦,𝒩) configurations, for 30 timesteps It is clearly evident from the figure that with an increase in the number of slices and partitions, the PRB utilization is greater (due to the larger number of users assigned to the slices) and therefore the PRB-share of the residual par￾tition gradually drops. Furthermore, for all four configura￾ti… view at source ↗
Figure 6
Figure 6. Figure 6: Comparing % of PRB-share in eMBB Premium slices with Convergence In contrast, the proposed formal framework, FORSLICE, is generic and automated, and successfully computes PRB￾allocations for any configuration of services, partitions and slices. Moreover, our work addresses residual-partition share management in order to serve the best-effort services, which is not accounted for in [15]. To demonstrate the … view at source ↗
Figure 7
Figure 7. Figure 7: Network configuration (3, 3, 7): service types eMBB Premium, Normal and fixed wireless traffic; slices Pre1 and Norm1 in Partition 1; Pre2, Norm2 and FWA1 in Partition 2; Pre3 and FWA2 in Partition 3 Based on the user categories and resource demands, we have considered 3 partitions with the slice types as eMBB Premium, eMBB Normal and FWA. Specifically, we obtain the (3, 3, 7) network configuration: 3 serv… view at source ↗
Figure 8
Figure 8. Figure 8: Throughput: offered (FORSLICE) vs obtained (NS3-5Glena) Now, we consider a network simulation for the (3, 3, 7) configuration, to demonstrate the network per￾formance of FORSLICE, measured in terms of the aver￾age throughput per slice over all the timesteps. Specifi￾cally, we show that the throughput achieved by the PRB￾allocations and de-allocations in FORSLICE is almost sim￾ilar to the throughput observe… view at source ↗
read the original abstract

Network slicing is a modern 5G technology that provides efficient network experience for diverse use cases. It is a technique for partitioning a single physical network infrastructure into multiple virtual networks, called slices, each equipped for specific services and requirements. In this work, we particularly deal with radio access network (RAN) slicing and resource allocation to RAN slices. In 5G, physical resource blocks (PRBs) being the fundamental units of radio resources, our main focus is to allocate PRBs to the slices efficiently. While addressing a spectrum of needs for multiple services or the same services with multi-priorities, we need to ensure two vital system properties: i) fairness to every service type (i.e., providing the required resources and a desired range of throughput) even after prioritizing a particular service type, and ii) PRB-optimality or minimizing the unused PRBs in slices. These serve as the core performance evaluation metrics for PRB-allocation in our work. We adopt the 3-layered hierarchical PRB-partitioning technique for allocating PRBs to network slices. The case-specific, AI-based solution of the state-of-the-art method lacks sufficient correctness to ensure consistent system performance. To achieve guaranteed correctness and completeness, we leverage formal methods and propose the first approach for a fair and optimal PRB distribution to RAN slices. We formally model the PRB-allocation problem as a 3-layered framework, FORSLICE, specifically by employing satisfiability modulo theories. Next, we apply formal verification to ensure that the desired system properties: fairness and PRB-optimality, are satisfied by the model. The proposed method offers an efficient, versatile and automated approach compatible with all 3-layered hierarchical network structure configurations, yielding significant system property improvements compared to the baseline.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes FORSLICE, a 3-layered SMT-based formal framework for modeling PRB allocation to RAN slices in 5G network slicing. It encodes the hierarchical partitioning to enforce two properties—fairness (providing required resources and throughput ranges even under prioritization) and PRB-optimality (minimizing unused blocks)—via satisfiability modulo theories, applies formal verification to confirm these properties hold, and claims the resulting approach is efficient, automated, versatile across all 3-layer configurations, and superior to AI-based baselines.

Significance. If the encoding is faithful to RAN dynamics and the solver produces complete solutions at practical scales, the work would supply machine-checked guarantees on fairness and optimality for multi-service slicing, a clear advance over heuristic or learned allocators that lack such assurances. The emphasis on a parameter-free formal model and compatibility with arbitrary hierarchical structures is a potential strength.

major comments (2)
  1. [Abstract] Abstract: the central claim that 'formal verification ensures that the desired system properties: fairness and PRB-optimality, are satisfied by the model' is unsupported because the abstract (and, per the reader's report, the visible text) supplies no model equations, constraint definitions, verification outcomes, solver statistics, or instance sizes. This is load-bearing for the assertions of 'guaranteed correctness and completeness' and 'efficient, versatile and automated approach'.
  2. [Evaluation] Evaluation section (or §4–5): the claim of 'significant system property improvements compared to the baseline' and scalability to 'practical network sizes' requires concrete data on PRB counts, number of slices, solving times, timeout rates, and success without approximations. The absence of such evidence leaves the 'efficient' and 'guaranteed' assertions unverified for realistic 5G RAN deployments (hundreds of PRBs, multiple priority slices), directly undermining the weakest assumption identified in the stress test.
minor comments (2)
  1. [Abstract] The abstract would be strengthened by naming the SMT solver, the specific fairness metric (e.g., max-min, proportional), and at least one illustrative constraint size or runtime figure.
  2. Notation for the three layers and the PRB-optimality objective should be introduced with a small example before the general claims.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback highlighting areas where the abstract and evaluation require greater substantiation. We address each major comment below and will revise the manuscript to incorporate the requested details while preserving the core contributions of the SMT-based FORSLICE framework.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that 'formal verification ensures that the desired system properties: fairness and PRB-optimality, are satisfied by the model' is unsupported because the abstract (and, per the reader's report, the visible text) supplies no model equations, constraint definitions, verification outcomes, solver statistics, or instance sizes. This is load-bearing for the assertions of 'guaranteed correctness and completeness' and 'efficient, versatile and automated approach'.

    Authors: We agree that the current abstract is too concise to fully support the central claims. In the revised version, we will expand the abstract to include a brief outline of the 3-layered SMT encoding, the key constraints used to enforce fairness (ensuring required resources and throughput ranges under prioritization) and PRB-optimality (minimizing unused blocks), along with high-level verification outcomes such as satisfiability results and solver statistics for representative instance sizes. This will directly substantiate the assertions of guaranteed correctness, completeness, efficiency, and versatility without altering the abstract's length constraints. revision: yes

  2. Referee: [Evaluation] Evaluation section (or §4–5): the claim of 'significant system property improvements compared to the baseline' and scalability to 'practical network sizes' requires concrete data on PRB counts, number of slices, solving times, timeout rates, and success without approximations. The absence of such evidence leaves the 'efficient' and 'guaranteed' assertions unverified for realistic 5G RAN deployments (hundreds of PRBs, multiple priority slices), directly undermining the weakest assumption identified in the stress test.

    Authors: We acknowledge the need for more explicit quantitative evidence in the evaluation. The revised manuscript will expand §4–5 with additional tables and text providing: PRB counts up to hundreds (covering practical 5G scales), varying numbers of slices and priority levels, measured solving times, timeout rates (zero in our tested configurations as all instances were solved completely), and direct metric improvements over the AI baseline without approximations. We will also clarify how the formal model addresses assumptions in the stress test. These additions will verify the efficiency and guaranteed properties for realistic deployments. revision: yes

Circularity Check

0 steps flagged

No circularity: FORSLICE is a direct SMT encoding plus verification with independent claims

full rationale

The paper's derivation consists of defining a 3-layered hierarchical PRB allocation problem, encoding it directly in SMT, and then verifying the fairness and PRB-optimality properties on that encoding. No equations, definitions, or results are shown to reduce to fitted parameters, self-referential citations, or renamed inputs by construction. The abstract and structure present the model and verification steps as the source of the claimed guarantees and improvements, without any load-bearing self-citation chains or ansatzes smuggled from prior work. This is a standard formal-methods modeling paper whose central claims remain independent of the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Only abstract available; no explicit free parameters, invented entities, or detailed axioms are stated. The framework rests on the domain assumption that a 3-layer hierarchy plus SMT encoding suffices to capture fairness and optimality.

axioms (1)
  • domain assumption A 3-layered hierarchical PRB-partitioning technique accurately represents the requirements of RAN slicing for multiple services.
    Invoked when the problem is modeled as a 3-layered framework.

pith-pipeline@v0.9.0 · 5656 in / 1338 out tokens · 46615 ms · 2026-05-10T17:32:06.364564+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    [n. d.]. Open-source 5G new radio (NR) network simulator. https://5g-lena.cttc.es/

    work page

  2. [2]

    3GPP. 2022. System architecture for the 5G system (5GS) (Release 17). In ETSI TS 23.501 V17.5.0 (2022-07)

    work page 2022

  3. [3]

    3GPP. 2024. 3rd Generation Partnership Project; Technical specification group radio access network; NR; User equipment (UE) radio access capabilities (Release 18). In TS 38.306 V18.2.0 (2024-06)

    work page 2024

  4. [4]

    3GPP. 2024. System architecture for the 5G System (5GS) (Release 18). In TS 23.501 V18.5.0 (2024-05)

    work page 2024

  5. [5]

    Megha Ajit, Sriram Sankaran, and Kurunandan Jain. 2021. Formal verification of 5G EAP-AKA protocol. In Proc. International Telecommunication Networks and Applications Conference. 140–146

    work page 2021

  6. [6]

    Sihem Bakri, Pantelis A Frangoudis, and Adlen Ksentini. 2019. Dynamic slicing of RAN resources for heterogeneous coexisting 5G services. In Proc. Global Communications Conference . 1–6

    work page 2019

  7. [7]

    Debarpita Banerjee, Parasara Sridhar Duggirala, Bineet Ghosh, and Sumana Ghosh. 2025. A Formal approach towards safe and stable schedule synthesis in weakly hard control systems. ACM Transactions on Embedded Computing Systems (TECS) 24, 5s (2025)

    work page 2025

  8. [8]

    Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking. MIT Press

    work page 2018

  9. [9]

    Ericsson. 2020. 5G RAN slicing. https://www.ericsson.com/4addb2/assets/local/networks-slicing/docs/ericsson-5g-ran-slicing.pdf

    work page 2020

  10. [10]

    Devleena Ghosh, Sumana Ghosh, Raj Kumar Gajavelly, and Ansuman Banerjee. 2023. Harnessing multiple BMC engines together for efficient formal verification. In Proc. Formal Methods and Models for System Design . 71–81

    work page 2023

  11. [11]

    Sumana Ghosh, Soumyajit Dey, and Pallab Dasgupta. 2019. Performance and energy aware robust specification of control execution patterns under dropped samples. IET Computers & Digital Techniques (2019)

    work page 2019

  12. [12]

    Sumana Ghosh, Soumyajit Dey, and Pallab Dasgupta. 2020. Pattern guided integrated scheduling and routing in multi-hop control networks. ACM Transactions on Embedded Computing Systems 19, 2 (2020), 1–28

    work page 2020

  13. [13]

    Fengchen Gong et al. 2023. Towards integrating formal methods into ML-based systems for networking. In Proc. ACM Workshop on Hot Topics in Networks. 48–55

    work page 2023

  14. [14]

    Maroua Idi, Sana Younès, and Riadh Robbana. 2022. Performance evaluation of call admission control strategy in cloud radio access network using formal methods. In Proc. International Conference on Software Technologies . 630–640. 30 D. Banerjee et al

    work page 2022

  15. [15]

    Ajay Kattepur et al. 2024. Convergence: Cognitive intent driven 5G radio access network slice assurance. In Proc. Wireless Communications and Networking Conference. 01–06

    work page 2024

  16. [16]

    Moez Krichen. 2023. A survey on formal verification and validation techniques for internet of things. Applied Sciences 13, 14 (2023), 8122

    work page 2023

  17. [17]

    A Kunnappilly, P Backeman, and C Seceleanu. 2021. From UML modeling to UPPAAL model checking of 5G dynamic service orchestration. In Proc. Engineering of Computer Based Systems . 1–10

    work page 2021

  18. [18]

    Sergey Litvinyuk, Pavel Pilyugin, and Andrey Petukhov. 2024. Formal methods for building network-level information security policies . In Proc. Modern Computer Network Technologies. 1–5

    work page 2024

  19. [19]

    Mojdeh Karbalaee Motalleb, Vahid Shah-Mansouri, Saeedeh Parsaeefard, and Onel Luis Alcaraz López. 2022. Resource allocation in an open RAN system using network slicing. IEEE Transactions on Network and Service Management 20, 1 (2022), 471–485

    work page 2022

  20. [20]

    Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proc. Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340

    work page 2008

  21. [21]

    L. O. Ostrowsky, N. L. S. da Fonseca, and C. A. V. Melo. 2007. A Traffic Model for UDP Flows. In Proc. International Conference on Communications . 217–222

    work page 2007

  22. [22]

    Mehdi Setayesh, Shahab Bahrami, and Vincent WS Wong. 2020. Joint PRB and power allocation for slicing eMBB and URLLC services in 5G C-RAN. In Proc. Global Communications Conference . 1–6

    work page 2020

  23. [23]

    Alireza Souri, Nima Jafari Navimipour, and Amir Masoud Rahmani. 2018. Formal verification approaches and standards in the cloud computing: a comprehensive and systematic review. Computer Standards & Interfaces 58 (2018), 1–22

    work page 2018

  24. [24]

    Hao Yin, Lyutianyang Zhang, and Sumit Roy. 2020. Multiplexing URLLC traffic within eMBB services in 5G NR: Fair scheduling. IEEE Transactions on Communications 69, 2 (2020), 1080–1093

    work page 2020