Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids

TL;DR

This paper presents a probabilistic model checking approach to optimize the deployment of wind and battery storage in smart grids, improving reliability amid forecast deviations and enabling rigorous, adaptable control strategies.

Contribution

It introduces a novel application of probabilistic model checking to the complex problem of flexible energy management in smart grids, addressing intractability with structural exploitation.

Findings

Method is feasible across various grid configurations.

Approach reduces grid frequency deviations effectively.

Iterative exploration improves computational efficiency.

Abstract

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. Our experiments show the method's feasibility and versatility across grid configurations and time scales.