Solving Lia(Star) Using Approximations

Linear arithmetic with stars, LIA(star), is an extension of Presburger arithmetic that allows forming indefinite summations over values that satisfy a formula. It has found uses in decision procedures for multi-sets and for vector addition systems. LIA(star) formulas can be translated back into Presburger arithmetic, but with non-trivial space overhead. In this paper we develop a decision procedure for LIA(star) that checks satisfiability of LIA(star) formulas. By refining on-demand under and over-approximations of LIA(star) formulas, it can avoid the space overhead that is integral to previous approaches. We have implemented our procedure in a prototype and report on encouraging results that suggest that LIA(star) formulas can be checked for satisfiability without computing a prohibitively large equivalent Presburger formula.