Polynomial Invariants for Affine Programs
Logic in Computer Science
2018-05-03 v2 Discrete Mathematics
Algebraic Geometry
Abstract
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.
Cite
@article{arxiv.1802.01810,
title = {Polynomial Invariants for Affine Programs},
author = {Ehud Hrushovski and Joël Ouaknine and Amaury Pouly and James Worrell},
journal= {arXiv preprint arXiv:1802.01810},
year = {2018}
}