Stop It, and Be Stubborn!

TL;DR

This paper advocates making models AG EF terminating to improve verification by catching errors and enabling effective stubborn set reduction, demonstrated through an example involving mutual exclusion algorithms.

Contribution

It introduces a method to ensure AG EF termination in models, enhancing error detection and state space reduction without extra conditions.

Findings

Adding an alternative first action can make models AG EF terminating.

AG EF termination can be checked efficiently from reduced state space.

Ensures safety and progress properties are preserved in stubborn set methods.

Abstract

A system is AG EF terminating, if and only if from every reachable state, a terminal state is reachable. This publication argues that it is beneficial for both catching non-progress errors and stubborn set state space reduction to try to make verification models AG EF terminating. An incorrect mutual exclusion algorithm is used as an example. The error does not manifest itself, unless the first action of the customers is modelled differently from other actions. An appropriate method is to add an alternative first action that models the customer stopping for good. This method typically makes the model AG EF terminating. If the model is AG EF terminating, then the basic strong stubborn set method preserves safety and some progress properties without any additional condition for solving the ignoring problem. Furthermore, whether the model is AG EF terminating can be checked efficiently from the reduced state space.