Search
Workshop

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

  • Amaury Pouly (Universite de Paris, CNRS, IRIF, France)
E1 05 (Leibniz-Saal)

Abstract

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.

Saskia Gutzschebauch

Max Planck Institute for Mathematics in the Sciences Contact via Mail

Rida Ait El Manssour

Max Planck Institute for Mathematics in the Sciences

Marc Härkönen

Georgia Institute of Technology

Bernd Sturmfels

Max Planck Institute for Mathematics in the Sciences