
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 onecounter automata. This problem is known to be undecidable in
general and PSPACEcomplete for the special case of deterministic onecounter
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
onecounter automata as an open problem. In this paper we resolve this problem
positively, utilising a known reduction to a reachability problem on
onecounter 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 nondeterministic (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 nontrivial fourthorder 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 statetostate reachability in linear
timeinvariant control systems, with control sets defined by boolean
combinations of linear inequalities. Decidability of the subproblem 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
setsunions of two affine subspaces and bounded convex polytopes
respectivelyand 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 continuoustime 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 righthand 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.
ContinuousTime 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 ChurchTuring 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 nonreachability. 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
continuoustime 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^{x1}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 realtime
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
nonrational 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 nonnegative 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
linearalgebraic results, including the MinkowskiWeyl 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 wellstudied, 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 righthand 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 ChurchTuring 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 ChurchTuring 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
spaceefficient as computations done in the context of Computable Analysis.

In this paper we prove that computing the solution of an initialvalue
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.