Abstract

Accurate weather forecasting plays a critical role in timely decision-making for public safety, agriculture and operational planning. Traditional forecasting models, such as numerical simulations and machine learning approaches, often face limitations in accuracy, transparency, computational efficiency and formal correctness. To address these challenges, we propose the use of formal verification methods, specifically model checking, to analyze weather forecasting models with mathematical rigor. Model checking, by developing a state-space model and systematically verifying key properties, provides a mathematically grounded approach that enhances the accuracy, transparency and efficiency of forecast evaluation. In this paper, we present a model checking-based framework to formally analyze weather forecasting models by first developing Discrete-time Markov Chains (DTMCs) of weather states. To illustrate the practical effectiveness of this approach, meteorological data from the ERA5 reanalysis dataset, focusing on Islamabad and Swat in Pakistan, is used to compute the transitional probabilities for these models. Relevant forecast properties are modeled using Probabilistic Computational Tree Logic (PCTL) and verified using the PRISM model checker. The experimental results demonstrate that the proposed DTMC framework effectively captures temporal weather dynamics while maintaining low computational overhead and formal interpretability. The close agreement between the verified probabilistic predictions and observed weather conditions highlights the potential of formal methods as a complementary and explainable approach for weather forecasting and forecast validation.

Different weather conditions of consecutive days

People

• Adnan Rashid, SEECS, NUST, Pakistan
• Sohail Iqbal, SEECS, NUST, Pakistan
• Asad Ahmed, SEECS, NUST, Pakistan
• Osman Hasan, SEECS, NUST, Pakistan
• Sa'ed Abed, Kuwait University, Kuwait

Publications

1. A. Rashid, S. Abed and O. Hasan, “Enhancing Forecast Reliability through Formal Verification: A Model Checking Approach for Weather Prediction Models”, Journal of Engineering Research, Elsevier (Accepted in July 2026).
2. A. Ahmed, A. Rashid and S. Iqbal, “Formal Analysis of Weather Forecasting Model in PRISM”, Frontiers of Information Technology (FIT), IEEE, pp: 355-360, Islamabad, Pakistan, 2014.