Solving $$\mathrm {LIA} ^\star $$ Using Approximations

Linear arithmetic with stars, \(\mathrm {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. \(\mathrm {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 \(\mathrm {LIA} ^\star \) that checks satisfiability of \(\mathrm {LIA} ^\star \) formulas. By refining on-demand under and over-approximations of \(\mathrm {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 \(\mathrm {LIA} ^\star \) formulas can be checked for satisfiability without computing a prohibitively large equivalent Presburger formula.