Visible to the public Biblio

Filters: Author is Ouaknine, Joel  [Clear All Filters]
2018-09-28
Ouaknine, Joel, Sousa-Pinto, Joao, Worrell, James.  2017.  On the Polytope Escape Problem for Continuous Linear Dynamical Systems. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. :11–17.
The Polytope Escape Problem for continuous linear dynamical systems consists of deciding, given an affine function f:Rd -\textbackslashtextgreater Rd and a convex polytope P⊆ Rd, both with rational descriptions, whether there exists an initial point x0 in P such that the trajectory of the unique solution to the differential equation: ·x(t)=f(x(t)) x 0= x0 is entirely contained in P. We show that this problem is reducible in polynomial time to the decision version of linear programming with real algebraic coefficients. The latter is a special case of the decision problem for the existential theory of real closed fields, which is known to lie between NP and PSPACE. Our algorithm makes use of spectral techniques and relies, among others, on tools from Diophantine approximation.
2017-05-17
Ouaknine, Joel, Pouly, Amaury, Sousa-Pinto, Joao, Worrell, James.  2016.  Solvability of Matrix-Exponential Equations. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. :798–806.

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 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.