Scalable and Efficient Deep Reinforcement Learning-Based Model Checker for Computation Tree Logic.

Abstract

Formal verification using temporal logics such as computation tree logic (CTL) is essential for validating safety and correctness in complex systems. However, traditional model-checking techniques face severe scalability limitations due to the state explosion problem and their reliance on exhaustive symbolic traversal. Moreover, existing learning-based verification methods often lack formal guarantees and interpretability. These challenges create a pressing need for scalable, learning-based verification methods that preserve verification reliability while improving computational efficiency. This article introduces a novel deep reinforcement learning (DRL)-based model checking framework that learns to verify CTL formulas directly through interaction with system models. Unlike traditional symbolic model checkers such as NuSMV, the proposed DRL-CTL checker trained using proximal policy optimization (PPO) interprets CTL semantics over system models represented as Kripke structures without performing symbolic state-space traversal at inference time. Reward functions are designed for individual CTL operators, and fixed-point reasoning is incorporated to handle global temporal properties such as $AG(\phi)$ and $EG(\phi)$ . Experimental results show that the proposed method achieves near-constant inference time of approximately 2 ms per formula on an Intel Core i9-13900K CPU (24 cores, 3.0 GHz), 64 GB RAM, NVIDIA RTX 4090 GPU (24 GB VRAM), reduces verification time by up to 90% compared with traditional model checkers, and scales to models with more than $10^{1192}$ reachable states. The framework also produces witnesses and counterexamples and yields verification outcomes identical to those of symbolic checkers in our experiments. These results highlight the potential of DRL to serve as a scalable, efficient, and explainable alternative to classical CTL model checking.