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.

在2021年NASA形式化方法研讨会（NASA Formal Methods Symposium）上发表的题为《平衡风电与电池：迈向智能电网的预测验证》（"Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids"）的论文中，我们研究了包含风电与电池储能的智能电网系统。传统上，日前规划（day-ahead planning）旨在平衡电力需求与风电供给，但实际风况往往与预测存在偏差。储能与发电环节的短期灵活性可填补潜在缺口，其规划时间尺度为分钟级，覆盖30至60分钟的时间范围。寻找灵活性部署的最优方案需要求解半无限非凸随机规划（semi-infinite non-convex stochastic program），这类问题通常难以精确求解。现有方法依赖于采样技术，但此类关键问题需要更严格且具有更强保证性的方法。我们的方法采用概率模型检测（probabilistic model checking）技术。首先，我们将该问题转化为带离散控制的连续空间马尔可夫决策过程（continuous-space Markov decision process with discretized control），其最优部署策略旨在最小化电网频率的期望偏差。为缓解状态空间爆炸（state space explosion）问题，我们利用模型的特定结构特性实现了一种迭代探索方法，该方法可在风电数据更新时复用预计算值。本数据集包含复现论文结果所需的全部代码与数据，关于代码安装及使用的说明见数据集中的ReadMe.txt文件。