Model Checking · PRISM

Formal Analysis of Weather Forecasting Models

Applying probabilistic model checking to weather forecasting — modeling weather states as Discrete-time Markov Chains and verifying forecast properties with the PRISM model checker.

Abstract

Accurate weather forecasting plays a critical role in timely decision-making for public safety, agriculture, and operational planning. Traditional forecasting models — numerical simulations and machine-learning approaches — often face limitations in accuracy, transparency, computational efficiency, and formal correctness.

We propose formal verification, specifically model checking, to analyze weather forecasting models with mathematical rigor: developing Discrete-time Markov Chains (DTMCs) of weather states, using ERA5 reanalysis meteorological data for Islamabad and Swat, Pakistan, to compute transitional probabilities. Forecast properties are modeled in Probabilistic Computational Tree Logic (PCTL) and verified with the PRISM model checker. The verified probabilistic predictions closely agree with observed weather conditions, while maintaining low computational overhead and formal interpretability.

Framework