# A Quasi-Linear Time Algorithm Deciding Whether Weak B\"uchi Automata Reading Vectors of Reals Recognize Saturated Languages

## TL;DR

This paper presents a quasi-linear time algorithm to determine if weak deterministic B"uchi automata recognize saturated languages of real vectors, improving efficiency for standard and parallel encodings.

## Contribution

It introduces a novel quasi-linear time decision procedure for recognizing saturated languages by weak B"uchi automata, applicable to multiple encoding schemes.

## Key findings

- Algorithm runs in quasi-linear time for minimal automata.
- Decides recognition of saturated languages for both sequential and parallel encodings.
- Applicable to automata reading vectors of relative reals.

## Abstract

This work considers weak deterministic B\"uchi automata reading encodings of non-negative $d$-vectors of reals in a fixed base. A saturated language is a language which contains all encoding of elements belonging to a set of $d$-vectors of reals. A Real Vector Automaton is an automaton which recognizes a saturated language. It is explained how to decide in quasi-linear time whether a minimal weak deterministic B\"uchi automaton is a Real Vector Automaton. The problem is solved both for the two standard encodings of vectors of numbers: the sequential encoding and the parallel encoding. This algorithm runs in linear time for minimal weak B\"uchi automata accepting set of reals. Finally, the same problem is also solved for parallel encoding of automata reading vectors of relative reals.