Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids (Artifact)

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.