• Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in general and PSPACE-complete for the special case of deterministic one-counter automata. Several years ago, Demri and Sangnier investigated the model checking problem for the flat fragment of Freeze LTL on several classes of counter automata and posed the decidability of model checking flat Freeze LTL on one-counter automata as an open problem. In this paper we resolve this problem positively, utilising a known reduction to a reachability problem on one-counter automata with parameterised equality and disequality tests. Our main technical contribution is to show decidability of the latter problem by translation to Presburger arithmetic.
  • We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.
  • An astonishing fact was established by Lee A. Rubel (1981): there exists a fixed non-trivial fourth-order polynomial differential algebraic equation (DAE) such that for any positive continuous function $\varphi$ on the reals, and for any positive continuous function $\epsilon(t)$, it has a $\mathcal{C}^\infty$ solution with $| y(t) - \varphi(t) | < \epsilon(t)$ for all $t$. Lee A. Rubel provided an explicit example of such a polynomial DAE. Other examples of universal DAE have later been proposed by other authors. However, Rubel's DAE \emph{never} has a unique solution, even with a finite number of conditions of the form $y^{(k_i)}(a_i)=b_i$. The question whether one can require the solution that approximates $\varphi$ to be the unique solution for a given initial data is a well known open problem [Rubel 1981, page 2], [Boshernitzan 1986, Conjecture 6.2]. In this article, we solve it and show that Rubel's statement holds for polynomial ordinary differential equations (ODEs), and since polynomial ODEs have a unique solution given an initial data, this positively answers Rubel's open problem. More precisely, we show that there exists a \textbf{fixed} polynomial ODE such that for any $\varphi$ and $\epsilon(t)$ there exists some initial condition that yields a solution that is $\epsilon$-close to $\varphi$ at all times. In particular, the solution to the ODE is necessarily analytic, and we show that the initial condition is computable from the target function and error function.
  • We consider the decidability of state-to-state reachability in linear time-invariant control systems, with control sets defined by boolean combinations of linear inequalities. Decidability of the sub-problem in which control sets are linear subspaces is a fundamental result in control theory. We first show that reachability is undecidable if the set of controls is a finite union of affine subspaces. We then consider two simple subclasses of control sets---unions of two affine subspaces and bounded convex polytopes respectively---and show that in these two cases the reachability problem for LTI systems is as hard as certain longstanding open decision problems concerning linear recurrence sequences. Finally we present some spectral assumptions on the transition matrix of an LTI system under which reachability becomes decidable with bounded convex polytopes as control sets.
  • We consider the General Purpose Analog Computer (GPAC), introduced by Claude Shannon in 1941 as a mathematical model of Differential Analysers, that is to say as a model of continuous-time analog (mechanical, and later one electronic) machines of that time. We extend the model properly to a model of computation not restricted to univariate functions (i.e. functions $f: \mathbb{R} \to \mathbb{R}$) but also to the multivariate case of (i.e. functions $f: \mathbb{R}^n \to \mathbb{R}^m$), and establish some basic properties. In particular, we prove that a very wide class of (continuous and discontinuous) functions can be uniformly approximated over their full domain. Technically: we generalize some known results about the GPAC to the multidimensional case: we extend naturally the notion of \emph{generable} function, from the unidimensional to the multidimensional case. We prove a few stability properties of this class, mostly stability by arithmetic operations, composition and ODE solving. We establish that generable functions are always analytic. We prove that generable functions include some basic (useful) generable functions, and that we can (uniformly) approximate a wide range of functions this way. This extends some of the results from \cite{Sha41} to the multidimensional case, and this also strengths the approximation result from \cite{Sha41} over a compact domain to a uniform approximation result over unbounded domains. We also discuss the issue of constants, and we prove that involved constants can basically assumed to always be polynomial time computable numbers.
  • The outcomes of this paper are twofold. Implicit complexity. We provide an implicit characterization of polynomial time computation in terms of ordinary differential equations: we characterize the class PTIME of languages computable in polynomial time in terms of differential equations with polynomial right-hand side. This result gives a purely continuous elegant and simple characterization of PTIME. We believe it is the first time complexity classes are characterized using only ordinary differential equations. Our characterization extends to functions computable in polynomial time over the reals in the sense of computable analysis. Our results may provide a new perspective on classical complexity, by giving a way to define complexity classes, like PTIME, in a very simple way, without any reference to a notion of (discrete) machine. This may also provide ways to state classical questions about computational complexity via ordinary differential equations. Continuous-Time Models of Computation. Our results can also be interpreted in terms of analog computers or analog models of computation: As a side effect, we get that the 1941 General Purpose Analog Computer (GPAC) of Claude Shannon is provably equivalent to Turing machines both in terms of computability and complexity, a fact that has never been established before. This result provides arguments in favour of a generalised form of the Church-Turing Hypothesis, which states that any physically realistic (macroscopic) computer is equivalent to Turing machines both in terms of computability and complexity.
  • Reachability for piecewise affine systems is known to be undecidable, starting from dimension $2$. In this paper we investigate the exact complexity of several decidable variants of reachability and control questions for piecewise affine systems. We show in particular that the region to region bounded time versions leads to $NP$-complete or co-$NP$-complete problems, starting from dimension $2$. We also prove that a bounded precision version leads to $PSPACE$-complete problems.
  • The \emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $\mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable \emph{invariants} $\mathcal{P} \subseteq \mathbb{R}^d$, \emph{i.e.}, sets that are stable under $A$ and contain $x$ and not $y$, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of \emph{semilinear} invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
  • In 1941, Claude Shannon introduced the General Purpose Analog Computer(GPAC) as a mathematical model of Differential Analysers, that is to say as a model of continuous-time analog (mechanical, and later one electronic) machines of that time. Following Shannon's arguments, functions generated by GPACs must be differentially algebraic. As it is known that some computable functions like Euler's $\Gamma(x)=\int_{0}^{\infty}t^{x-1}e^{-t}dt$ or Riemann's Zeta function $\zeta(x)=\sum_{k=0}^\infty \frac1{k^x}$ are not differentially algebraic, this argument has been often used to demonstrate in the past that the GPAC is less powerful than digital computation. It was proved in JOC2007, that if a more modern notion of computation is considered, i.e. in particular if computability is not restricted to real-time generation of functions, the GPAC is actually equivalent to Turing machines. Our purpose is first to discuss the robustness of the notion of computation involved in JOC2007, by establishing that natural variants of the notion of computation from this paper leads to the same computability result. Second, to go considerations about (time) complexity, we explore several natural variants for measuring time/space complexity of a computation. Rather surprisingly, whereas defining a robust time complexity for general continuous time systems is a well known open problem, we prove that all variants are actually equivalent even at the complexity level. As a consequence, it seems that a robust and well defined notion of time complexity exists for the GPAC, or equivalently for computations by polynomial ordinary differential equations. Another side effect of our proof is also that we show in some way that polynomial ordinary differential equations can be used as a kind of programming model, and that there is a rather nice and robust notion of ODE programming.
  • In this note, we extend the result of \cite{PoulyG16} about the complexity of solving polynomial differential equations over unbounded domains to work with non-rational input. In order to deal with arbitrary input, we phrase the result in framework of Conputable Analysis \cite{Ko91}. As a side result, we also get a uniform result about complexity of the operator, and not just about the solution.
  • We consider a continuous analogue of Babai et al.'s and Cai et al.'s problem of solving multiplicative matrix equations. Given $k+1$ square matrices $A_{1}, \ldots, 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}, \ldots, t_{k}$ such that \begin{align*} \prod \limits_{i=1}^{k} \exp(A_{i} t_{i}) = C . \end{align*} We show that this problem is undecidable in general, but decidable under the assumption that the matrices $A_{1}, \ldots, 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.
  • In this paper we investigate the computational complexity of solving ordinary differential equations (ODEs) $y^{\prime}=p(y)$ over \emph{unbounded time domains}, where $p$ is a vector of polynomials. Contrarily to the bounded (compact) time case, this problem has not been well-studied, apparently due to the "intuition" that it can always be reduced to the bounded case by using rescaling techniques. However, as we show in this paper, rescaling techniques do not seem to provide meaningful insights on the complexity of this problem, since the use of such techniques introduces a dependence on parameters which are hard to compute. We present algorithms which numerically solve these ODEs over unbounded time domains. These algorithms have guaranteed accuracy, i.e. given some arbitrarily large time $t$ and error bound $\varepsilon$ as input, they will output a value $\tilde{y}$ which satisfies $\|y(t)-\tilde{y}\|\leq\varepsilon$. We analyze the complexity of these algorithms and show that they compute $\tilde{y}$ in time polynomial in several quantities including the time $t$, the accuracy of the output $\varepsilon$ and the length of the curve $y$ from $0$ to $t$, assuming it exists until time $t$. We consider both algebraic complexity and bit complexity.
  • We provide an implicit characterization of polynomial time computation in terms of ordinary differential equations: we characterize the class $\operatorname{PTIME}$ of languages computable in polynomial time in terms of differential equations with polynomial right-hand side. This result gives a purely continuous (time and space) elegant and simple characterization of $\operatorname{PTIME}$. This is the first time such classes are characterized using only ordinary differential equations. Our characterization extends to functions computable in polynomial time over the reals in the sense of computable analysis. This extends to deterministic complexity classes above polynomial time. This may provide a new perspective on classical complexity, by giving a way to define complexity classes, like $\operatorname{PTIME}$, in a very simple way, without any reference to a notion of (discrete) machine. This may also provide ways to state classical questions about computational complexity via ordinary differential equations, i.e.~by using the framework of analysis.
  • The Church-Turing thesis states that any sufficiently powerful computational model which captures the notion of algorithm is computationally equivalent to the Turing machine. This equivalence usually holds both at a computability level and at a computational complexity level modulo polynomial reductions. However, the situation is less clear in what concerns models of computation using real numbers, and no analog of the Church-Turing thesis exists for this case. Recently it was shown that some models of computation with real numbers were equivalent from a computability perspective. In particular it was shown that Shannon's General Purpose Analog Computer (GPAC) is equivalent to Computable Analysis. However, little is known about what happens at a computational complexity level. In this paper we shed some light on the connections between this two models, from a computational complexity level, by showing that, modulo polynomial reductions, computations of Turing machines can be simulated by GPACs, without the need of using more (space) resources than those used in the original Turing computation, as long as we are talking about bounded computations. In other words, computations done by the GPAC are as space-efficient as computations done in the context of Computable Analysis.
  • In this paper we prove that computing the solution of an initial-value problem $\dot{y}=p(y)$ with initial condition $y(t_0)=y_0\in\R^d$ at time $t_0+T$ with precision $e^{-\mu}$ where $p$ is a vector of polynomials can be done in time polynomial in the value of $T$, $\mu$ and $Y=\sup_{t_0\leqslant u\leqslant T}\infnorm{y(u)}$. Contrary to existing results, our algorithm works for any vector of polynomials $p$ over any bounded or unbounded domain and has a guaranteed complexity and precision. In particular we do not assume $p$ to be fixed, nor the solution to lie in a compact domain, nor we assume that $p$ has a Lipschitz constant.