Polynomial Invariants for Affine Programs

Author: 

Hrushovski, E
Ouaknine, J
Pouly, A
Worrell, J

Publication Date: 

1 January 2018

Journal: 

CoRR

Last Updated: 

2021-06-21T08:45:40.29+01:00

Volume: 

abs/1802.01810

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.

Symplectic id: 

937964

Submitted to ORA: 

Submitted

Publication Type: 

Conference Paper