Weak Mso with the Unbounding Quantifier

TL;DR

This paper introduces max-regular languages, extending omega-regular languages, with automata and logical characterizations, and provides effective translations between these representations.

Contribution

It defines max-regular languages and establishes their equivalence with automata and logical descriptions, expanding the class of omega-regular languages.

Findings

Max-regular languages extend omega-regular languages.

Effective translation algorithms between automata and logic.

Automata are deterministic counter automata.

Abstract

A new class of languages of infinite words is introduced, called the max-regular languages, extending the class of $\omega$-regular languages. The class has two equivalent descriptions: in terms of automata (a type of deterministic counter automaton), and in terms of logic (weak monadic second-order logic with a bounding quantifier). Effective translations between the logic and automata are given.