An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables

TL;DR

This paper introduces a simplified automata-based decision procedure for linear arithmetic involving real and integer variables, leveraging topological arguments to reduce complexity and improve implementability.

Contribution

It demonstrates that a restricted class of automata suffices for decision procedures, enabling simpler algorithms for mixed linear arithmetic.

Findings

Simpler automata algorithms successfully implemented

Reduced complexity in decision procedures

Effective handling of real and integer linear arithmetic

Abstract

This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on infinite words, but this involves some difficult and delicate to implement algorithms. The contribution of this paper is to show, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms, which have been successfully implemented.