salle A. Turing CE4
24 mars 2016 - 14h00
Solvability of Matrix-Exponential Equations
par Amaury Pouly de Oxford University, Dept. of Computer Science
Abstract: We consider a continuous analogue of Babai, Lipton et al's problem of solving multiplicative matrix equations. Given k+1 square matrices A_1,..., A_k, C, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals t_1, ..., t_k such that
exp(A_1 t_1)exp(A_2 t_2)...exp(A_n t_n) = C.
We show that this problem is undecidable in general, but decidable under the assumption that the matrices A_1, ..., A_k commute. Our results have applications to reachability problems for linear hybrid automata.
Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert's Tenth Problem.
