Symbolic {\omega}-automata with obligations

TL;DR

This paper introduces obligation automata, a novel symbolic {5}-automata model that extends classical automata to recognize a broader class of languages, with practical tools for their manipulation.

Contribution

It proposes a new automata framework based on obligations, formalizes their semantics, and provides a practical implementation for automata operations.

Findings

Obligation automata recognize a strict superset of 5-regular languages.

The framework subsumes classical automata like Bbchi, Rabin, Streett, and parity automata.

A tool for automata operations and a machine-readable format are developed.

Abstract

Extensions of {\omega}-automata to infinite alphabets typically rely on symbolic guards to keep the transition relation finite, and on registers or memory cells to preserve information from past symbols. Symbolic transitions alone are ill-suited to act on this information, and register automata have intricate formal semantics and issues with tractability. We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions. Whenever a transition with an obligation is taken, the obligation is evaluated against the current symbol and yields a constraint on the next symbol that the automaton will read. We formalize obligation automata with existential and universal branching and Emerson-Lei acceptance conditions, which subsume classic families such as B\"uchi, Rabin, Strett, and parity automata. We show that these automata recognise a strict superset of {\omega}-regular languages. To illustrate the practicality of our proposal, we also introduce a machine-readable format to express obligation automata and describe a tool implementing several operations over them, including automata product and emptiness checking.