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.
Alex: Welcome to another episode of ResearchPod. Today we're diving into a paper on making 5G networks work better for everyone. Sam, what is this one about?
Sam: The paper is called FORSLICE, from researchers at Indian Statistical Institute and Ericsson. It tackles how to divide up the radio resources in 5G networks fairly and without waste, for different services like video streaming and IoT devices. The central claim is that current AI methods often fail to guarantee fairness or efficiency, so they propose the first math-based system that proves both properties hold true.
Alex: So this paper is basically asking how to split those radio resources evenly across services without shortchanging anyone or leaving a lot unused?
Sam: Yes, exactly. In 5G, the network has to handle everything from high-speed video for premium users to low-data sensors for machines, all sharing the same radio waves. The problem is peak times overload one service—like video streaming—while starving others, and past AI approaches waste about 44% more resources than needed because they can't prove fairness or full efficiency. They model it as a three-layered setup: slices at the bottom for specific services, partitions grouping them in the middle, and a top layer overseeing everything plus leftovers for basic tasks like email.
Alex: Hold on—these layers sound like dividing a shared resource step by step. But why three specifically, and what's the big issue with AI methods right now?
Sam: Picture the network like a big pizza to share among groups with different appetites. First layer: cut slices tailored to each group's needs, like big pieces for video fans. Middle layer: group related slices into sections, adjusting within groups. Top layer: balance sections overall and save scraps for casual eaters. AI tries guessing these cuts but can't always prove no group starves or too much goes to waste—especially prioritizing premium video. This paper uses exact math checks to guarantee it works for any setup.
Alex: Right, so the core problem is unreliable splitting in busy 5G networks. And they fix it with proven math instead of guesses.
Sam: Precisely. It ensures every service gets its share of throughput and minimizes unused resources, a clear improvement over the baseline AI method.
Alex: Okay, so the math checks everything holds up. But walk me through how these three layers actually talk to each other—like, what do the bottom slices do to kick things off?
Sam: At the bottom, each slice watches its own users over a set time period, like checking your snack supply every hour during a party. If more people show up and it runs low, it sends a request for extra resources; if some leave and there's extra, it signals to give some back. Researchers call these a 'top-up signal' for needing more and a 'ramp-down signal' for returning extras—never both at once, since that wouldn't make sense.
Alex: Got it, so slices flag when they're short or have surplus after their check-in window. Then the middle layer steps in for groups of slices?
Sam: Right. The middle layer has a monitoring agent per group of slices, or partition. It looks at all the signals from its slices—for two slices, there are nine possible combos, like both needing more, one needing and one giving back, or neither. It adjusts within the group first: shift resources from a slice with extras to one that's short, only pulling from outside if needed. That keeps things balanced locally without waste.
Alex: Makes sense for inside a group. But with multiple groups, how does the top avoid one partition hogging everything?
Sam: The top central agent oversees all partitions plus the leftover resources for basic tasks. It sees the net needs across groups—again, nine scenarios like both wanting more or one giving and one taking—and shifts between them or dips into leftovers carefully. It also assigns new users evenly to premium slices across groups, preventing crowds in one spot that could overload it. All this gets modeled as math rules fed to a solver that exhaustively checks every possibility works.
Alex: So the signals bubble up, adjustments happen layer by layer from local to global, and the solver proves no fairness breaks or waste. And prioritizing premium video fits right in?
Sam: Exactly. Premium gets smaller check windows and higher resource per user, so it stays ahead—throughput ties directly to resources used, making the guarantees real. The paper shows this setup achieves the goals where AI guesses fall short.
Alex: So the guarantees come from tying throughput straight to allocated resources. But how did they test if this setup actually holds up in practice—like with different network sizes or user patterns?
Sam: They ran simulations across four setups, varying the number of service types, partitions, and slices—like starting small with three services, two partitions, four slices, then scaling up to five services, four partitions, thirteen slices. For each, they generated user arrivals and leaves based on real patterns: video streaming has bursty crowds, like lognormal distribution where most times are quiet but peaks hit hard; home internet follows a steadier Poisson pattern, arrivals spread evenly like raindrops. The Z3 solver then crunches the constraints over thirty minutes, outputting allocations if everything checks out.
Alex: So user patterns mimic real 5G services, feeding the model step by step. And the services—what kinds exactly?
Sam: The five include enhanced mobile broadband for fast data—split into premium for top video and normal; fixed wireless access for steady home links; ultra-reliable low-latency for critical timing like remote surgery; and massive machine-type for hordes of sensors. They tested if fairness holds: residual pool for basics like email stays over half full in every case, even as slices grow and users multiply—achieved by inter-group shifts and even spreads stopping overuse.
Alex: Does that specifically help those no-frills services?
Sam: Yes—top-ups only fire if reserves exceed half, ramp-downs feed extras back, and group trades often refill without dipping deep. This leaves ample for best-effort without starving premiums. Execution scales reasonably too: under thirty seconds minimum for small cases over thirty steps, averaging minutes even larger.
Alex: So across sizes, it balances guarantees with low overhead. How does it stack up against other methods out there—like the AI ones you mentioned earlier?
Sam: The paper compares it directly to an AI planning method called Convergence, the closest prior work. That approach handles just one small setup—three services, two partitions, four slices—and over-allocates resources to premium video slices by at least 44% more than FORSLICE does. FORSLICE matches fairness and priority but uses fewer resources overall, leaving more for basics like email in the leftovers.
Alex: So it prioritizes premium without the waste. Any real-world tie-in, beyond simulations?
Sam: Yes—they apply it to Ericsson's setup in Saltlake Kolkata, with peak evening video demands from offices alongside steady home links. For a three-partition, seven-slice network matching local services, they fed allocations into NS3-5Glena—a detailed 5G simulator that models base stations, user devices, and traffic flows. The predicted throughput per slice closely matched what the simulator actually delivered, confirming the allocations perform as expected in a realistic environment.
Alex: That validation bridges theory to practice nicely. Though with bigger networks or longer runs, does the solving time become an issue?
Sam: It does scale with size—for the largest tested case over thirty minutes with thirteen slices, it took up to about half an hour total. They discretized time into steps and grouped users per block to keep it tractable for the solver, which works for planning but might need incremental updates for true real-time tweaks in live networks.
Alex: Fair point—the discretization and time make it viable now, but live ops could push for faster variants. Overall, though, swapping AI guesses for proven math seems like a meaningful step for reliable slicing.
Sam: It is—the first to bring formal verification to RAN resource splits, ensuring fairness, priority, and low waste hold across setups. Experiments confirm better efficiency than baselines and real throughput in simulations, pointing toward dependable automation in diverse 5G scenarios.
Alex: That's a grounded advance. Thanks, Sam—this has been a clear look at how math can steady the 5G resource game. Thanks for listening to ResearchPod.