## 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