# Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications

## TL;DR

This paper introduces a method to simplify the proof process for system refinements in asynchronous systems, focusing on fair stuttering runs, and demonstrates its application on the Bakery Algorithm.

## Contribution

It provides a novel proof reduction technique that simplifies verification by focusing on individual steps of key state machines, improving efficiency in finite state cases.

## Key findings

- Proof reduction simplifies verification of asynchronous systems.
- Efficient explicit-state checking is possible for finite state systems.
- Application demonstrated on the Bakery Algorithm.

## Abstract

We present a series of definitions and theorems demonstrating how to reduce the requirements for proving system refinements ensuring containment of fair stuttering runs. A primary result of the work is the ability to reduce the requisite proofs on runs of a system of interacting state machines to a set of definitions and checks on single steps of a small number of state machines corresponding to the intuitive notions of freedom from starvation and deadlock. We further refine the definitions to afford an efficient explicit-state checking procedure in certain finite state cases. We demonstrate the proof reduction on versions of the Bakery Algorithm.