Decidability of the Zero Problem for Exponential Polynomials

We consider the decision problem of determining whether an exponential
polynomial has a real zero.  This is motivated by reachability questions
for continuous-time linear dynamical systems, where exponential
polynomials naturally arise as solutions of linear differential equations.

The decidability of the Zero Problem is open in general and our results
concern restricted versions.  We show decidability of a bounded
variant---asking for a zero in a given bounded interval---subject to
Schanuel's conjecture.  In the unbounded case, we obtain partial
decidability results, using Baker's Theorem on linear forms in logarithms
as a key tool.  We show also that decidability of the Zero Problem in full
generality would entail powerful new effectiveness results concerning
Diophantine approximation of algebraic numbers.

This is joint work with Ventsislav Chonev and Joel Ouaknine.