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

Area of Science:

• Computer Science
• Artificial Intelligence
• Formal Methods

Background:

• Formal verification is crucial for complex systems, but traditional model checking faces scalability issues.
• Existing learning-based methods lack formal guarantees and interpretability.
• There's a need for efficient, scalable, and reliable learning-based verification techniques.

Purpose of the Study:

• To introduce a novel deep reinforcement learning (DRL)-based model checking framework for verifying computation tree logic (CTL) formulas.
• To develop a scalable and efficient alternative to traditional symbolic model checking.

Main Methods:

• A deep reinforcement learning (DRL) framework using proximal policy optimization (PPO) was developed.
• The framework interprets CTL semantics on Kripke structures without symbolic state-space traversal.
• Reward functions were designed for CTL operators, incorporating fixed-point reasoning for global properties.

Main Results:

• The DRL-CTL checker achieved near-constant inference time (approx. 2 ms per formula).
• Verification time was reduced by up to 90% compared to traditional model checkers.
• The method scales to models with over 10^1192 states and provides identical verification outcomes.

Conclusions:

• Deep reinforcement learning (DRL) presents a scalable, efficient, and explainable alternative for CTL model checking.
• The proposed framework overcomes the limitations of traditional symbolic methods.
• DRL-based verification offers significant improvements in computational efficiency and scalability.