Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!

TL;DR

This paper explores how formal methods like model checking can improve reinforcement learning in autonomous driving by identifying bugs early and enhancing reward function design, leading to safer and more efficient systems.

Contribution

It introduces the use of model checking for pre-analysis and reward automata in RL for autonomous driving, expanding beyond safety to improve correctness and performance.

Findings

Model checking can reveal sensor and learning step bugs before RL training.

Reward automata improve reward function design for complex objectives.

Experiments demonstrate enhanced RL performance and system understanding.

Abstract

Most reinforcement learning (RL) platforms use high-level programming languages, such as OpenAI Gymnasium using Python. These frameworks provide various API and benchmarks for testing RL algorithms in different domains, such as autonomous driving (AD) and robotics. These platforms often emphasise the design of RL algorithms and the training performance but neglect the correctness of models and reward functions, which can be crucial for the successful application of RL. This paper proposes using formal methods to model AD systems and demonstrates how model checking (MC) can be used in RL for AD. Most studies combining MC and RL focus on safety, such as safety shields. However, this paper shows different facets where MC can strengthen RL. First, an MC-based model pre-analysis can reveal bugs with respect to sensor accuracy and learning step size. This step serves as a preparation of RL, which saves time if bugs exist and deepens users' understanding of the target system. Second, reward automata can benefit the design of reward functions and greatly improve learning performance especially when the learning objectives are multiple. All these findings are supported by experiments.