We consider the decidability of the membership problem for matrix-exponential semigroups: given k ∈ N and square matrices A1, ..., Ak, C, all of the same dimension and with real algebraic entries, decide whether C is contained in the semigroup generated by the matrix exponentials exp(Ait), where i ∈ {1, ..., k} and t ≥ 0. This problem can be seen as a continuous analog of Babai et al.'s and Cai et al.'s problem of solving multiplicative matrix equations, and has applications to reachability analysis of linear hybrid automata and switching systems. Our main results are that the semigroup membership problem is undecidable in general, but decidable if we assume that A1, ..., Ak commute. The decidability proof is by reduction to a version of integer programming that has transcendental constants. We give a decision procedure for the latter using Baker's theorem on linear forms in logarithms of algebraic numbers, among other tools. The undecidability result is shown by reduction from Hilbert's Tenth Problem.
Journal of the ACM 66(2), 2019. 25 pages.
PDF
© 2019 ACM.