FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services
2026-04-09 • Networking and Internet Architecture
Networking and Internet Architecture
AI summaryⓘ
The authors study how to fairly and efficiently share 5G radio resources called physical resource blocks (PRBs) among different virtual network slices. They focus on making sure each service gets the right amount of resources while minimizing waste. To solve this, they create a formal, mathematically verified method named FORSLICE that guarantees fairness and optimal use of PRBs. Their approach improves on previous AI-based methods by providing more reliable and automated resource allocation in a structured 3-layer network setup.
Network slicing5GRadio access network (RAN)Physical resource blocks (PRBs)Resource allocationFairnessPRB-optimalityHierarchical partitioningFormal methodsSatisfiability modulo theories (SMT)
Authors
Debarpita Banerjee, Sumana Ghosh, Snigdha Das, Shilpa Budhkar, Rana Pratap Sircar
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.