Transition-based vs stated-based acceptance for automata over infinite words

TL;DR

This paper analyzes the shift from state-based to transition-based acceptance in automata over infinite words, highlighting its implications and advantages in logic and formal verification.

Contribution

It advocates for transition-based acceptance, providing a comprehensive analysis of its benefits and impact compared to traditional state-based methods.

Findings

Transition-based acceptance influences problem complexity.

Transition-based methods align better with certain verification tasks.

The shift affects the formal properties of automata.

Abstract

Automata over infinite objects are a well-established model with applications in logic and formal verification. Traditionally, acceptance in such automata is defined based on the set of states visited infinitely often during a run. However, there is a growing trend towards defining acceptance based on transitions rather than states. In this survey, we analyse the reasons for this shift and advocate using transition-based acceptance in the context of automata over infinite words. We present a collection of problems where the choice of formalism has a major impact and discuss the causes of these differences.