User-Driven Abstraction for Model Checking

TL;DR

This paper introduces a user-driven abstraction technique that simplifies system models before checking, significantly reducing state space and aiding in understanding system properties, demonstrated on examples like Dekker's algorithm.

Contribution

It presents a novel abstraction method allowing users to simplify models prior to checking, improving efficiency and interpretability in model checking.

Findings

Reduces state space size in model checking

Helps understand why systems satisfy properties

Effective on examples like Dekker's mutual exclusion

Abstract

Model checking has found a role in the engineering of reactive systems. However, model checkers are still strongly limited by the size of the system description they can check. Here we present a technique in which a system is simplified prior to model checking by the application of abstraction rules. The rules can greatly reduce the state space of a system description and help in understanding why a system satisfies a property. We illustrate the use of the technique on examples, including Dekker's mutual exclusion algorithm.