We consider a continuous analogue of
[Babai et al. 1996]'s and
[Cai et al. 2000]'s problem of solving multiplicative
matrix equations. Given k+1 square matrices
A1, ..., Ak, C, all of the
same dimension, whose entries are real algebraic, we examine the
problem of deciding whether there exist non-negative reals
t1, ..., tk such that
exp(A1t1)...exp(Aktk)
= C.
We show that this problem is undecidable in general, but decidable
under the assumption that the matrices A1,
..., Ak 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.
Proceedings of LICS 16, 2016. 10 pages.
PDF
© 2016 IEEE Computer Society Press.