10.4121/14185139.v1
Thom S. Badings
Thom S.
Badings
0000-0002-5235-1967
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids (Artifact)
4TU.ResearchData
2023
Dataset
Computer Software
Computation Theory and Mathematics
smart grids
Markov decision process
formal methods
model-predictive control
probabilistic model checking
Radboud University Nijmegen, Department of Software Science
University of Twente, Formal Methods and Tools Group
2023-03-08
10.1007/978-3-030-76384-8_1
*.xlsx
*.py
*.txt
1
CC BY 4.0
In our paper titled "Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids", presented at the 2021 NASA Formal Methods Symposium, we study a smart grid with wind power and battery storage. Traditionally, day-ahead planning aims to balance demand and wind power, yet actual wind conditions often deviate from forecasts. Short-term flexibility in storage and generation fills potential gaps, planned on a minutes time scale for 30-60 minute horizons. Finding the optimal flexibility deployment requires solving a semi-infinite non-convex stochastic program, which is generally intractable to do exactly. Previous approaches rely on sampling, yet such critical problems call for rigorous approaches with stronger guarantees. Our method employs probabilistic model checking techniques. First, we cast the problem as a continuous-space Markov decision process with discretized control, for which an optimal deployment strategy minimizes the expected grid frequency deviation. To mitigate state space explosion, we exploit specific structural properties of the model to implement an iterative exploration method that reuses pre-computed values as wind data is updated. This artifact contains all code and data needed to reproduce the results presented in the paper. Instructions on how to install and use the code are included in the ReadMe.txt file in the artifact.
unknown
NWO OCENW.KLEIN.187
unknown
NWO NWA.1160.18.238
Dutch Research Council
639.021.754
Verification of Cyber-Physical Systems: Exploiting Uncertainty for Scalability