Algebraic closure of finitely generated groups of matrices, with application to invariants synthesis for affine programs and linear hybrid automata

I will present some results on how 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. I will then explain how this result can be extended to linear hybrid automata which contain a mixture of linear discrete and continuous (ODE) dynamics. Finally, I will mention some recent results on the complexity of computing those invariants and obtaining bounds on the degree of the algebraic closure of finitely generated groups of matrices.