RL-based Heuristics Learning for Model Checking


Introduction

Model checking is a powerful graph search technique used to verify system properties and detect bugs. However, as the complexity of a system increases, the state space grows exponentially, rendering exhaustive search methods impractical. Our research addresses this challenge by using reinforcement learning to learn effective search heuristics. This approach is inspired by directed model checking, where heuristics are given, not learned.

Framework and Methodology

Our framework is built on reinforcement learning, specifically employing Q-learning to learn and refine search heuristics for model checking.

Preliminary Experiment

Setup:

Results Summary:

OTR Configuration Baseline (BFS) RL w/ PA RL with PA2
OTR(3/5) Timeout 8444 265
OTR(3/6) Timeout 96360 446
OTR(4/6) Timeout Timeout 109330
OTR(4/7) Timeout Timeout 38092

Future Work

Future research will focus on:

References

To be added.

Examples

To be added.

Contact

Byoungho Son byhoson (at) postech.ac.kr


Last modified: 2024/10/5 02:40:42 (Byoungho Son)