arXiv subjects

Amaury Pouly

Publications and source records attributed to Amaury Pouly.

At least 19 recordsLinked to original sources

arXiv2026

On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories

This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1--31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time. We give two further examples of instantiations of our framework, showing polynomial-time decidability of the fixed negation fragments of weak linear real arithmetic and of the restriction of Presburger arithmetic in which each inequality contains at most one variable.

cs.LO↗

arXiv2025

Positivity of Nearly Linearly Recurrent Sequences

Nearly linear recurrences generalise linear recurrences and can be represented as special cases of both linear time-invariant systems in control theory and linear-constraint loops in program analysis. We formulate the Positivity Problem for such recurrences: given a recurrence and initial values, decide whether every sequence satisfying the recurrence is termwise nonnegative. This problem generalises Positivity for linear recurrence sequences and is a special case of halfspace non-reachability for linear time-invariant systems. Our main result is a decision procedure for order-2 recurrences. The termination of the procedure relies on a transcendence theorem of independent interest: we prove that certain convergent series obtained by summing the absolute values of terms of algebraic linear recurrence sequences are transcendental.

math.DS↗

arXiv2025

On the Computation of the Zariski Closure of Finitely Generated Groups of Matrices

We investigate the complexity of computing the Zariski closure of a finitely generated group of matrices. The Zariski closure was previously shown to be computable by Derksen, Jeandel, and Koiran, but the termination argument for their algorithm appears not to yield any complexity bound. In this paper we follow a different approach and obtain a bound on the degree of the polynomials that define the closure. Our bound shows that the closure can be computed in elementary time. We also obtain upper bounds on the length of chains of linear algebraic groups, where all the groups are generated over a fixed number field.

cs.CC↗

arXiv2022

The Membership Problem for Hypergeometric Sequences with Rational Parameters

We investigate the Membership Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n \rangle_{n=0}^\infty$ of rational numbers and a target $t \in \mathbb{Q}$, decide whether $t$ occurs in the sequence. We show decidability of this problem under the assumption that in the defining recurrence $p(n)u_{n}=q(n)u_{n-1}$, the roots of the polynomials $p(x)$ and $q(x)$ are all rational numbers. Our proof relies on bounds on the density of primes in arithmetic progressions. We also observe a relationship between the decidability of the Membership problem (and variants) and the Rohrlich-Lang conjecture in transcendence theory.

cs.LO↗

arXiv2021

On the Decidability of Reachability in Continuous Time Linear Time-Invariant Systems

We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyse this problem with respect to the allowable control sets, which are assumed to be the image under a linear map of the unit hypercube. This naturally models bounded (sometimes called saturated) controls. Decidability of the version of the reachability problem in which control sets are affine subspaces of $\mathbb{R}^n$ is a fundamental result in control theory. Our first result is decidability in two dimensions ($n=2$) if the matrix $A$ satisfies some spectral conditions, and conditional decidablility in general. If the transformation matrix $A$ is diagonal with rational entries (or rational multiples of the same algebraic number) then the reachability problem is decidable. If the transformation matrix $A$ only has real eigenvalues, the reachability problem is conditionally decidable. The time-bounded reachability problem is conditionally decidable, and unconditionally decidable in two dimensions. Some of our decidability results are conditional in that they rely on the decidability of certain mathematical theories, namely the theory of the reals with exponential ($\mathfrak{R}_{\exp}$) and with bounded sine ($\mathfrak{R}_{\exp,\sin}$). We also obtain a hardness result for a mild generalization of the problem where the target is simple set (hypercube of dimension $n-1$ or hyperplane) instead of a point, and the control set is a convex bounded polytope. In this case, we show that the problem is at least as hard as the \emph{Continuous Positivity problem} or the \emph{Nontangential Continuous Positivity problem}.

math.OC↗

arXiv2020

Reachability in Dynamical Systems with Rounding

We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose every entry is a multiple of $g$, we are interested in the behaviour of the orbit $\mathcal{O}={<}[x], [M[x]],[M[M[x]]],\dots{>}$, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability---whether a given target $y \in\mathbb{Q}^{d}$ belongs to $\mathcal{O}$---is PSPACE-complete for hyperbolic systems (when no eigenvalue of $M$ has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.

cs.CC↗

arXiv2019

On the Monniaux Problem in Abstract Interpretation

The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program $P$, a safety (\emph{e.g.}, non-reachability) specification $φ$, and an abstract domain of invariants $\mathcal{D}$, does there exist an inductive invariant $I$ in $\mathcal{D}$ guaranteeing that program $P$ meets its specification $φ$. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.

cs.LO↗

arXiv2019

Algebraic Invariants for Linear Hybrid Automata

We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given unguarded linear hybrid automaton (i.e., a hybrid automaton having only unguarded transitions, all of whose assignments are given by affine expressions, and all of whose continuous dynamics are given by linear differential equations). Our main tool is a control-theoretic result of independent interest: given such a linear hybrid automaton, we show how to discretise the continuous dynamics in such a way that the resulting automaton has precisely the same algebraic invariants.

cs.LO↗

arXiv2018

Model Checking Flat Freeze LTL on One-Counter Automata

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.

cs.LO↗

arXiv2018

A Survey on Analog Models of Computation

We present a survey on analog models of computations. Analog can be understood both as computing by analogy, or as working on the continuum. We consider both approaches, often intertwined, with a point of view mostly oriented by computation theory.

cs.CC↗

arXiv2018

Polynomial Invariants for Affine Programs

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.

cs.LO↗

arXiv2018

On the Decidability of Reachability in Linear Time-Invariant Systems

We consider the decidability of state-to-state reachability in linear time-invariant control systems over discrete time. We analyse this problem with respect to the allowable control sets, which in general are assumed to be defined by boolean combinations of linear inequalities. Decidability of the version of the reachability problem in which control sets are affine subspaces of $\mathbb{R}^n$ is a fundamental result in control theory. Our first result is that reachability is undecidable if the set of controls is a finite union of affine subspaces. We also consider versions of the reachability problem in which (i)~the set of controls consists of a single affine subspace together with the origin and (ii)~the set of controls is a convex polytope. In these two cases we respectively show that the reachability problem is as hard as Skolem's Problem and the Positivity Problem for linear recurrence sequences (whose decidability has been open for several decades). Our main contribution is to show decidability of a version of the reachability problem in which control sets are convex polytopes, under certain spectral assumptions on the transition matrix.

math.OC↗

arXiv2018

On the Functions Generated by the General Purpose Analog Computer

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.

cs.CC↗

arXiv2017

Explicit Error Bounds for Carleman Linearization

We revisit the method of Carleman linearization for systems of ordinary differential equations with polynomial right-hand sides. This transformation provides an approximate linearization in a higher-dimensional space through the exact embedding of polynomial nonlinearities into an infinite-dimensional linear system, which is then truncated to obtain a finite-dimensional representation with an additive error. To the best of our knowledge, no explicit calculation of the error bound has been studied. In this paper, we propose two strategies to obtain a time-dependent function that locally bounds the truncation error. In the first approach, we proceed by iterative backwards-integration of the truncated system. However, the resulting error bound requires an a priori estimate of the norm of the exact solution for the given time horizon. To overcome this difficulty, we construct a combinatorial approach and solve it using generating functions, obtaining a local error bound that can be computed effectively.

math.NA↗

arXiv2017

Polynomial Time Corresponds to Solutions of Polynomial Ordinary Differential Equations of Polynomial Length (Journal version)

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.

cs.CC↗

arXiv2017

A Universal Ordinary Differential Equation

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.

math.CA↗

arXiv2017

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

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.

cs.CC↗

arXiv2016

Computing with Polynomial Ordinary Differential Equations

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 $Γ(x)=\int_{0}^{\infty}t^{x-1}e^{-t}dt$ or Riemann's Zeta function $ζ(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.

cs.CC↗