Probabilistic Program Equivalence for NetKAT

Abstract

We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language by developing an effective decision procedure based on stochastic matrices. The main challenge lies in reasoning about iteration, which we address by designing an encoding of the program semantics as a finite-state absorbing Markov chain, whose limiting distribution can be computed exactly. In an extended case study on a real-world data center network, we automatically verify various quantitative properties of interest, including resilience in the presence of failures, by analyzing the Markov chain semantics.

More by Praveen Kumar

• Model for Long-Term Monitoring of Geological Processes in Kazakhstan Using Intelligent Drone PortsJournal of Computational and Cognitive Engineering · 2026
• Wearable Gyroscope-Based Motion Tracking and Hand Gesture Recognition Using ANOVA for Feature DiscriminationJournal of Innovative Image Processing · 2026 · Citations: 3
• FINE-TUNING SMALL LANGUAGE MODELS FOR MENTAL HEALTH TEXT CLASSIFICATION: A PARAMETER-EFFICIENT APPROACH OUTPERFORMING ZERO-SHOT LARGE LANGUAGE MODELSScientific Journal of Astana IT University · 2026
• Vision-aided online A$$^*$$ path planning for efficient and safe navigation of service robotsInternational Journal of Intelligent Robotics and Applications · 2026 · Citations: 2