Statistical Verification of Medium-Access Parameterization for Power-Grid Edge Ad Hoc Sensor Networks
Haitian Wang, Xia Cheng, Yiren Wang, Xinyu Wang, Zichen Geng, Xian Zhang, and Yihao Ding

TL;DR
This paper presents a formal verification framework using statistical model checking to optimize CSMA/CA parameters in power-grid sensor networks, ensuring reliability, efficiency, and adherence to grid constraints.
Contribution
It introduces a novel verification approach combining stochastic hybrid automata and SMC to certify robust, equilibrium-based CSMA/CA configurations for power-grid sensor networks.
Findings
Certified equilibrium strategies improve utility and delivery ratio.
Energy consumption is reduced while maintaining delivery performance.
Configurations meet latency, reliability, and energy constraints with high robustness.
Abstract
The widespread deployment of power grid ad hoc sensor networks based on IEEE 802.15.4 raises reliability challenges when nodes selfishly adapt CSMA/CA parameters to maximize individual performance. Such behavior degrades reliability, energy efficiency, and compliance with strict grid constraints. Existing analytical and simulation approaches often fail to rigorously evaluate configurations under asynchronous, event-driven, and resource-limited conditions. We develop a verification framework that integrates stochastic timed hybrid automata with statistical model checking (SMC) with confidence bounds to formally assess CSMA/CA parameterizations under grid workloads. By encoding node- and system-level objectives in temporal logic and automating protocol screening via large-scale statistical evaluation, the method certifies Nash equilibrium strategies that remain robust to unilateral…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
