Minimization of semilinear automata

TL;DR

This paper develops a minimization procedure for semilinear automata over non-homogeneous atomic sets, using decidability results from Presburger arithmetic with divisibility, and shows standard methods may not terminate.

Contribution

It introduces a novel minimization method for semilinear automata, diverging from standard partition refinement, and leverages decidability of Presburger arithmetic with divisibility.

Findings

A minimization procedure for semilinear automata is established.

Standard partition refinement may not terminate for these automata.

Decidability of Presburger arithmetic with divisibility predicates is crucial.

Abstract

We investigate finite deterministic automata in sets with non-homogeneous atoms: integers with successor. As there are uncount- ably many deterministic finite automata in this setting, we restrict our attention to automata with semilinear transition function. The main re- sults is a minimization procedure for semilinear automata. The proof is subtle and refers to decidability of existential Presburger arithmetic with divisibility predicates. Interestingly, the minimization is not obtained by the standard partition refinement procedure, and we demonstrate that this procedure does not necessarily terminate for semilinear automata.