On strongest algebraic program invariants

Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell

We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. An affine program is one in which all assignments are given by affine expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant in one that is defined by polynomial equations over the program variables. In this paper we exhibit an algorithm to compute the strongest algebraic invariants that hold at each location of a given affine program. Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. We further show that if one generalises from affine programs to programs with polynomial updates, then it is no longer possible to compute strongest algebraic invariants, answering a 15-year-old question posed by Müller-Olm and Seidl.

Submitted, 2019. 17 pages.

PDF © 2019 Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell.



Imprint / Data Protection