-
On Tree Automata, Generating Functions, and Differential Equations
Authors:
Rida Ait El Manssour,
Vincent Cheval,
Mahsa Shirmohammadi,
James Worrell
Abstract:
In this paper we introduce holonomic tree automata: a common extension of weighted tree automata and holonomic recurrences. We show that the generating function of the tree series represented by such an automaton is differentially algebraic. Conversely, we give an algorithm that inputs a differentially algebraic power series, represented as a solution of a rational dynamical system, and outputs an…
▽ More
In this paper we introduce holonomic tree automata: a common extension of weighted tree automata and holonomic recurrences. We show that the generating function of the tree series represented by such an automaton is differentially algebraic. Conversely, we give an algorithm that inputs a differentially algebraic power series, represented as a solution of a rational dynamical system, and outputs an automaton whose generating function is the given series. Such an automaton yields a recurrence that can be used to compute the terms of the power series. We use the algorithm to obtain automaton representations of exponential generating functions of families of combinatorial objects given as combinatorial species. Using techniques from differential algebra, we show that it is decidable both whether two automata represent the same formal tree series and whether they have the same generating function.
△ Less
Submitted 11 July, 2024;
originally announced July 2024.
-
On the Decidability of Presburger Arithmetic Expanded with Powers
Authors:
Toghrul Karimov,
Florian Luca,
Joris Nieuwveld,
Joël Ouaknine,
James Worrell
Abstract:
We prove that for any integers $α, β> 1$, the existential fragment of the first-order theory of the structure $\langle \mathbb{Z}; 0,1,<, +, α^{\mathbb{N}}, β^{\mathbb{N}}\rangle$ is decidable (where $α^{\mathbb{N}}$ is the set of positive integer powers of $α$, and likewise for $β^{\mathbb{N}}$). On the other hand, we show by way of hardness that decidability of the existential fragment of the th…
▽ More
We prove that for any integers $α, β> 1$, the existential fragment of the first-order theory of the structure $\langle \mathbb{Z}; 0,1,<, +, α^{\mathbb{N}}, β^{\mathbb{N}}\rangle$ is decidable (where $α^{\mathbb{N}}$ is the set of positive integer powers of $α$, and likewise for $β^{\mathbb{N}}$). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of $\langle \mathbb{N}; 0,1, <, +, x\mapsto α^x, x \mapsto β^x\rangle$ for any multiplicatively independent $α,β> 1$ would lead to mathematical breakthroughs regarding base-$α$ and base-$β$ expansions of certain transcendental numbers.
△ Less
Submitted 6 July, 2024;
originally announced July 2024.
-
Determination Problems for Orbit Closures and Matrix Groups
Authors:
Rida Ait El Manssour,
George Kenison,
Mahsa Shirmohammadi,
James Worrell
Abstract:
Computational problems concerning the orbit of a point under the action of a matrix group occur in numerous subfields of computer science, including complexity theory, program analysis, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and several points and asks questions ab…
▽ More
Computational problems concerning the orbit of a point under the action of a matrix group occur in numerous subfields of computer science, including complexity theory, program analysis, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and several points and asks questions about the orbit closure of the points under the action of the group, e.g., whether two given orbit closures intersect.
In this paper we consider a collection of what we call determination problems concerning groups and orbit closures. These problems begin with a given variety and seek to understand whether and how it arises either as an algebraic group or as an orbit closure. The how question asks whether the underlying group is $s$-generated, meaning it is topologically generated by $s$ matrices for a given number $s$. Among other applications, problems of this type have recently been studied in the context of synthesising loops subject to certain specified invariants on program variables.
Our main result is a polynomial-space procedure that inputs a variety $V$ and a number $s$ and determines whether $V$ arises as an orbit closure of a point under an $s$-generated commutative matrix group. The main tools in our approach are rooted in structural properties of commutative algebraic matrix groups and lattice theory. We leave open the question of determining whether a variety is an orbit closure of a point under an algebraic matrix group (without the requirement of commutativity). In this regard, we note that a recent paper by Nosan et al. [NPSHW2021] gives an elementary procedure to compute the orbit closure of a point under finitely many matrices.
△ Less
Submitted 5 July, 2024;
originally announced July 2024.
-
The 2-Dimensional Constraint Loop Problem is Decidable
Authors:
Quentin Guilmant,
Engel Lefaucheux,
Joël Ouaknine,
James Worrell
Abstract:
A linear constraint loop is specified by a system of linear
inequalities that define the relation between the values of the
program variables before and after a single execution of the loop
body. In this paper we consider the problem of determining whether
such a loop terminates, i.e., whether all maximal executions are
finite, regardless of how the loop is initialised and how the
non-…
▽ More
A linear constraint loop is specified by a system of linear
inequalities that define the relation between the values of the
program variables before and after a single execution of the loop
body. In this paper we consider the problem of determining whether
such a loop terminates, i.e., whether all maximal executions are
finite, regardless of how the loop is initialised and how the
non-determinism in the loop body is resolved. We focus on the
variant of the termination problem in which the loop variables range
over $\mathbb{R}$. Our main result is that the termination problem
is decidable over the reals in dimension~2. A more abstract
formulation of our main result is that it is decidable whether a
binary relation on $\mathbb{R}^2$ that is given as a conjunction of
linear constraints is well-founded.
△ Less
Submitted 26 April, 2024;
originally announced May 2024.
-
On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates
Authors:
Valérie Berthé,
Toghrul Karimov,
Joris Nieuwveld,
Joël Ouaknine,
Mihir Vahanwala,
James Worrell
Abstract:
We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_k \rangle$, for various unary predicates $P_1,\ldots,P_k \subseteq \mathbb{N}$. We focus in particular on "arithmetic" predicates arising in the study of linear recurrence sequences, such as fixed-base powers $\mathsf{Pow}_k = \{k^n : n \in \mathbb{N}\}$, $k$-th powers…
▽ More
We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_k \rangle$, for various unary predicates $P_1,\ldots,P_k \subseteq \mathbb{N}$. We focus in particular on "arithmetic" predicates arising in the study of linear recurrence sequences, such as fixed-base powers $\mathsf{Pow}_k = \{k^n : n \in \mathbb{N}\}$, $k$-th powers $\mathsf{N}_k = \{n^k : n \in \mathbb{N}\}$, and the set of terms of the Fibonacci sequence $\mathsf{Fib} = \{0,1,2,3,5,8,13,\ldots\}$ (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:
$\bullet$ The MSO theory of $\langle \mathbb{N};<,\mathsf{Pow}_2, \mathsf{Fib} \rangle$ is decidable;
$\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_6 \rangle$ is decidable;
$\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_5 \rangle$ is decidable assuming Schanuel's conjecture;
$\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_4, \mathsf{N}_2 \rangle$ is decidable;
$\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{N}_2 \rangle$ is Turing-equivalent to the MSO theory of $\langle \mathbb{N};<,S \rangle$, where $S$ is the predicate corresponding to the binary expansion of $\sqrt{2}$. (As the binary expansion of $\sqrt{2}$ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.)
These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.
△ Less
Submitted 20 May, 2024; v1 submitted 13 May, 2024;
originally announced May 2024.
-
On Transcendence of Numbers Related to Sturmian and Arnoux-Rauzy Words
Authors:
Pavol Kebis,
Florian Luca,
Joel Ouaknine,
Andrew Scoones,
James Worrell
Abstract:
We consider numbers of the form $S_β(\boldsymbol{u}):=\sum_{n=0}^\infty \frac{u_n}{β^n}$, where $\boldsymbol{u}=\langle u_n \rangle_{n=0}^\infty$ is an infinite word over a finite alphabet and $β\in \mathbb{C}$ satisfies $|β|>1$. Our main contribution is to present a combinatorial criterion on $\boldsymbol u$, called echoing, that implies that $S_β(\boldsymbol{u})$ is transcendental whenever $β$ i…
▽ More
We consider numbers of the form $S_β(\boldsymbol{u}):=\sum_{n=0}^\infty \frac{u_n}{β^n}$, where $\boldsymbol{u}=\langle u_n \rangle_{n=0}^\infty$ is an infinite word over a finite alphabet and $β\in \mathbb{C}$ satisfies $|β|>1$. Our main contribution is to present a combinatorial criterion on $\boldsymbol u$, called echoing, that implies that $S_β(\boldsymbol{u})$ is transcendental whenever $β$ is algebraic. We show that every Sturmian word is echoing, as is the Tribonacci word, a leading example of an Arnoux-Rauzy word. We furthermore characterise $\overline{\mathbb{Q}}$-linear independence of sets of the form $\left\{ 1, S_β(\boldsymbol{u}_1),\ldots,S_β(\boldsymbol{u}_k) \right\}$, where $\boldsymbol{u}_1,\ldots,\boldsymbol{u}_k$ are Sturmian words having the same slope. Finally, we give an application of the above linear independence criterion to the theory of dynamical systems, showing that for a contracted rotation on the unit circle with algebraic slope, its limit set is either finite or consists exclusively of transcendental elements other than its endpoints $0$ and $1$. This confirms a conjecture of Bugeaud, Kim, Laurent, and Nogueira.
△ Less
Submitted 6 May, 2024;
originally announced May 2024.
-
On Rational Recursion for Holonomic Sequences
Authors:
Bertrand Teguia Tabuguia,
James Worrell
Abstract:
It was recently conjectured that every component of a discrete-time rational dynamical system is a solution to an algebraic difference equation that is linear in its highest-shift term (a quasi-linear equation). We prove that the conjecture holds in the special case of holonomic sequences, which can straightforwardly be represented by rational dynamical systems. We propose two algorithms for conve…
▽ More
It was recently conjectured that every component of a discrete-time rational dynamical system is a solution to an algebraic difference equation that is linear in its highest-shift term (a quasi-linear equation). We prove that the conjecture holds in the special case of holonomic sequences, which can straightforwardly be represented by rational dynamical systems. We propose two algorithms for converting holonomic recurrence equations into such quasi-linear equations. The two algorithms differ in their efficiency and the minimality of orders in their outputs.
△ Less
Submitted 15 June, 2024; v1 submitted 29 April, 2024;
originally announced April 2024.
-
Multiple Reachability in Linear Dynamical Systems
Authors:
Toghrul Karimov,
Edon Kelmendi,
Joël Ouaknine,
James Worrell
Abstract:
We consider reachability decision problems for linear dynamical systems: Given a linear map on $\mathbb{R}^d$ , together with source and target sets, determine whether there is a point in the source set whose orbit, obtained by repeatedly applying the linear map, enters the target set. When the source and target sets are semialgebraic, this problem can be reduced to a point-to-polytope reachabilit…
▽ More
We consider reachability decision problems for linear dynamical systems: Given a linear map on $\mathbb{R}^d$ , together with source and target sets, determine whether there is a point in the source set whose orbit, obtained by repeatedly applying the linear map, enters the target set. When the source and target sets are semialgebraic, this problem can be reduced to a point-to-polytope reachability question. The latter is generally believed not to be substantially harder than the well-known Skolem and Positivity Problems. The situation is markedly different for multiple reachability, i.e. the question of whether the orbit visits the target set at least m times, for some given positive integer m. In this paper, we prove that when the source set is semialgebraic and the target set consists of a hyperplane, multiple reachability is undecidable; in fact we already obtain undecidability in ambient dimension d = 10 and with fixed m = 9. Moreover, as we observe that procedures for dimensions 3 up to 9 would imply strong results pertaining to effective solutions of Diophantine equations, we mainly focus on the affine plane ($\mathbb{R}^2$). We obtain two main positive results. We show that multiple reachability is decidable for halfplane targets, and that it is also decidable for general semialgebraic targets, provided the linear map is a rotation. The latter result involves a new method, based on intersections of algebraic subgroups with subvarieties, due to Bombieri and Zannier.
△ Less
Submitted 11 March, 2024;
originally announced March 2024.
-
Twisted rational zeros of linear recurrence sequences
Authors:
Yuri Bilu,
Florian Luca,
Joris Nieuwveld,
Joël Ouaknine,
James Worrell
Abstract:
We introduce the notion of a twisted rational zero of a non-degenerate linear recurrence sequence (LRS). We show that any non-degenerate LRS has only finitely many such twisted rational zeros. In the particular case of the Tribonacci sequence, we show that $1/3$ and $-5/3$ are the only twisted rational zeros which are not integral zeros.
We introduce the notion of a twisted rational zero of a non-degenerate linear recurrence sequence (LRS). We show that any non-degenerate LRS has only finitely many such twisted rational zeros. In the particular case of the Tribonacci sequence, we show that $1/3$ and $-5/3$ are the only twisted rational zeros which are not integral zeros.
△ Less
Submitted 12 January, 2024;
originally announced January 2024.
-
Nonnegativity Problems for Matrix Semigroups
Authors:
Julian D'Costa,
Joel Ouaknine,
James Worrell
Abstract:
The matrix semigroup membership problem asks, given square matrices $M,M_1,\ldots,M_k$ of the same dimension, whether $M$ lies in the semigroup generated by $M_1,\ldots,M_k$. It is classical that this problem is undecidable in general but decidable in case $M_1,\ldots,M_k$ commute. In this paper we consider the problem of whether, given $M_1,\ldots,M_k$, the semigroup generated by…
▽ More
The matrix semigroup membership problem asks, given square matrices $M,M_1,\ldots,M_k$ of the same dimension, whether $M$ lies in the semigroup generated by $M_1,\ldots,M_k$. It is classical that this problem is undecidable in general but decidable in case $M_1,\ldots,M_k$ commute. In this paper we consider the problem of whether, given $M_1,\ldots,M_k$, the semigroup generated by $M_1,\ldots,M_k$ contains a non-negative matrix. We show that in case $M_1,\ldots,M_k$ commute, this problem is decidable subject to Schanuel's Conjecture. We show also that the problem is undecidable if the commutativity assumption is dropped. A key lemma in our decidability result is a procedure to determine, given a matrix $M$, whether the sequence of matrices $(M^n)_{n\geq 0}$ is ultimately nonnegative. This answers a problem posed by S. Akshay (arXiv:2205.09190). The latter result is in stark contrast to the notorious fact that it is not known how to determine effectively whether for any specific matrix index $(i,j)$ the sequence $(M^n)_{i,j}$ is ultimately nonnegative (which is a formulation of the Ultimate Positivity Problem for linear recurrence sequences).
△ Less
Submitted 10 November, 2023;
originally announced November 2023.
-
The Monadic Theory of Toric Words
Authors:
Valérie Berthé,
Toghrul Karimov,
Joël Ouaknine,
Mihir Vahanwala,
James Worrell
Abstract:
For which unary predicates $P_1, \ldots, P_m$ is the MSO theory of the structure $\langle \mathbb{N}; <, P_1, \ldots, P_m \rangle$ decidable? We survey the state of the art, leading us to investigate combinatorial properties of almost-periodic, morphic, and toric words. In doing so, we show that if each $P_i$ can be generated by a toric dynamical system of a certain kind, then the attendant MSO th…
▽ More
For which unary predicates $P_1, \ldots, P_m$ is the MSO theory of the structure $\langle \mathbb{N}; <, P_1, \ldots, P_m \rangle$ decidable? We survey the state of the art, leading us to investigate combinatorial properties of almost-periodic, morphic, and toric words. In doing so, we show that if each $P_i$ can be generated by a toric dynamical system of a certain kind, then the attendant MSO theory is decidable.
△ Less
Submitted 15 December, 2023; v1 submitted 8 November, 2023;
originally announced November 2023.
-
On Learning Polynomial Recursive Programs
Authors:
Alex Buna-Marginean,
Vincent Cheval,
Mahsa Shirmohammadi,
James Worrell
Abstract:
We introduce the class of P-finite automata. These are a generalisation of weighted automata, in which the weights of transitions can depend polynomially on the length of the input word. P-finite automata can also be viewed as simple tail-recursive programs in which the arguments of recursive calls can non-linearly refer to a variable that counts the number of recursive calls. The nomenclature is…
▽ More
We introduce the class of P-finite automata. These are a generalisation of weighted automata, in which the weights of transitions can depend polynomially on the length of the input word. P-finite automata can also be viewed as simple tail-recursive programs in which the arguments of recursive calls can non-linearly refer to a variable that counts the number of recursive calls. The nomenclature is motivated by the fact that over a unary alphabet P-finite automata compute so-called P-finite sequences, that is, sequences that satisfy a linear recurrence with polynomial coefficients. Our main result shows that P-finite automata can be learned in polynomial time in Angluin's MAT exact learning model. This generalises the classical results that deterministic finite automata and weighted automata over a field are respectively polynomial-time learnable in the MAT model.
△ Less
Submitted 23 October, 2023;
originally announced October 2023.
-
Transcendence of Sturmian Numbers over an Algebraic Base
Authors:
Florian Luca,
Joel Ouaknine,
James Worrell
Abstract:
We consider numbers of the form
$S_β(\boldsymbol{u}):=\sum_{n=0}^\infty \frac{u_n}{β^n}$ for
$\boldsymbol{u}=\langle u_n \rangle_{n=0}^\infty$ a Sturmian
sequence over a binary alphabet and $β$ an algebraic number with
$|β|>1$. We show that every such number is transcendental.
More generally, for a given base~$β$ and given irrational
number~$θ$ we characterise the…
▽ More
We consider numbers of the form
$S_β(\boldsymbol{u}):=\sum_{n=0}^\infty \frac{u_n}{β^n}$ for
$\boldsymbol{u}=\langle u_n \rangle_{n=0}^\infty$ a Sturmian
sequence over a binary alphabet and $β$ an algebraic number with
$|β|>1$. We show that every such number is transcendental.
More generally, for a given base~$β$ and given irrational
number~$θ$ we characterise the
$\overline{\mathbb{Q}}$-linear independence of sets of the form
$\left\{ 1,
S_β(\boldsymbol{u}^{(1)}),\ldots,S_β(\boldsymbol{u}^{(k)})
\right\}$, where $\boldsymbol{u}^{(1)},\ldots,\boldsymbol{u}^{(k)}$ are
Sturmian sequences having slope $θ$.
We give an application of our main result to the theory of dynamical
systems, showing that for a contracted rotation on the unit circle
with algebraic slope, its limit set is either finite or consists
exclusively of transcendental elements other than its endpoints $0$
and $1$. This confirms a conjecture of Bugeaud, Kim, Laurent, and
Nogueira.
△ Less
Submitted 25 August, 2023;
originally announced August 2023.
-
Skolem Meets Bateman-Horn
Authors:
Florian Luca,
James Maynard,
Armand Noubissie,
Joël Ouaknine,
James Worrell
Abstract:
The Skolem Problem asks to determine whether a given integer linear recurrence sequence has a zero term. This problem arises across a wide range of topics in computer science, including loop termination, formal languages, automata theory, and control theory, amongst many others. Decidability of the Skolem Problem is notoriously open. The state of the art is a decision procedure for recurrences of…
▽ More
The Skolem Problem asks to determine whether a given integer linear recurrence sequence has a zero term. This problem arises across a wide range of topics in computer science, including loop termination, formal languages, automata theory, and control theory, amongst many others. Decidability of the Skolem Problem is notoriously open. The state of the art is a decision procedure for recurrences of order at most 4: an advance achieved some 40 years ago, based on Baker's theorem on linear forms in logarithms of algebraic numbers.
A new approach to the Skolem Problem was recently initiated via the notion of a Universal Skolem Set: a set $S$ of positive integers such that it is decidable whether a given non-degenerate linear recurrence sequence has a zero in $S$. Clearly, proving decidability of the Skolem Problem is equivalent to showing that $\mathbb{N}$ itself is a Universal Skolem Set. The main contribution of the present paper is to construct a Universal Skolem Set that has lower density at least $0.29$. We show moreover that this set has density one subject to the Bateman-Horn conjecture. The latter is a central unifying hypothesis concerning the frequency of prime numbers among the values of systems of polynomials.
△ Less
Submitted 20 February, 2024; v1 submitted 2 August, 2023;
originally announced August 2023.
-
Multiplicity Problems on Algebraic Series and Context-Free Grammars
Authors:
Nikhil Balaji,
Lorenzo Clemente,
Klara Nosan,
Mahsa Shirmohammadi,
James Worrell
Abstract:
In this paper we obtain complexity bounds for computational problems on algebraic power series over several commuting variables. The power series are specified by systems of polynomial equations: a formalism closely related to weighted context-free grammars. We focus on three problems -- decide whether a given algebraic series is identically zero, determine whether all but finitely many coefficien…
▽ More
In this paper we obtain complexity bounds for computational problems on algebraic power series over several commuting variables. The power series are specified by systems of polynomial equations: a formalism closely related to weighted context-free grammars. We focus on three problems -- decide whether a given algebraic series is identically zero, determine whether all but finitely many coefficients are zero, and compute the coefficient of a specific monomial. We relate these questions to well-known computational problems on arithmetic circuits and thereby show that all three problems lie in the counting hierarchy. Our main result improves the best known complexity bound on deciding zeroness of an algebraic series. This problem is known to lie in PSPACE by reduction to the decision problem for the existential fragment of the theory of real closed fields. Here we show that the problem lies in the counting hierarchy by reduction to the problem of computing the degree of a polynomial given by an arithmetic circuit. As a corollary we obtain new complexity bounds on multiplicity equivalence of context-free grammars restricted to a bounded language, language inclusion of a nondeterministic finite automaton in an unambiguous context-free grammar, and language inclusion of a non-deterministic context-free grammar in an unambiguous finite automaton.
△ Less
Submitted 28 April, 2023; v1 submitted 27 April, 2023;
originally announced April 2023.
-
The Membership Problem for Hypergeometric Sequences with Quadratic Parameters
Authors:
George Kenison,
Klara Nosan,
Mahsa Shirmohammadi,
James Worrell
Abstract:
Hypergeometric sequences are rational-valued sequences that satisfy first-order linear recurrence relations with polynomial coefficients; that is, a hypergeometric sequence $\langle u_n \rangle_{n=0}^{\infty}$ is one that satisfies a recurrence of the form $f(n)u_n = g(n)u_{n-1}$ where $f,g \in \mathbb{Z}[x]$.
In this paper, we consider the Membership Problem for hypergeometric sequences: given…
▽ More
Hypergeometric sequences are rational-valued sequences that satisfy first-order linear recurrence relations with polynomial coefficients; that is, a hypergeometric sequence $\langle u_n \rangle_{n=0}^{\infty}$ is one that satisfies a recurrence of the form $f(n)u_n = g(n)u_{n-1}$ where $f,g \in \mathbb{Z}[x]$.
In this paper, we consider the Membership Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n \rangle_{n=0}^{\infty}$ and a target value $t\in \mathbb{Q}$, determine whether $u_n=t$ for some index $n$. We establish decidability of the Membership Problem under the assumption that either (i) $f$ and $g$ have distinct splitting fields or (ii) $f$ and $g$ are monic polynomials that both split over a quadratic extension of $\mathbb{Q}$. Our results are based on an analysis of the prime divisors of polynomial sequences $\langle f(n) \rangle_{n=1}^\infty$ and $\langle g(n) \rangle_{n=1}^\infty$ appearing in the recurrence relation.
△ Less
Submitted 23 May, 2023; v1 submitted 16 March, 2023;
originally announced March 2023.
-
On the $p$-adic zeros of the Tribonacci sequence
Authors:
Yuri Bilu,
Florian Luca,
Joris Nieuwveld,
Jöel Ouaknine,
James Worrell
Abstract:
In this paper, we refute some conjectures of Marques and Lengyel concerning the $p$-adic valuations of members of the Tribonacci sequence.
In this paper, we refute some conjectures of Marques and Lengyel concerning the $p$-adic valuations of members of the Tribonacci sequence.
△ Less
Submitted 30 October, 2022;
originally announced October 2022.
-
When are Local Queries Useful for Robust Learning?
Authors:
Pascale Gourdeau,
Varun Kanade,
Marta Kwiatkowska,
James Worrell
Abstract:
Distributional assumptions have been shown to be necessary for the robust learnability of concept classes when considering the exact-in-the-ball robust risk and access to random examples by Gourdeau et al. (2019). In this paper, we study learning models where the learner is given more power through the use of local queries, and give the first distribution-free algorithms that perform robust empiri…
▽ More
Distributional assumptions have been shown to be necessary for the robust learnability of concept classes when considering the exact-in-the-ball robust risk and access to random examples by Gourdeau et al. (2019). In this paper, we study learning models where the learner is given more power through the use of local queries, and give the first distribution-free algorithms that perform robust empirical risk minimization (ERM) for this notion of robustness. The first learning model we consider uses local membership queries (LMQ), where the learner can query the label of points near the training sample. We show that, under the uniform distribution, LMQs do not increase the robustness threshold of conjunctions and any superclass, e.g., decision lists and halfspaces. Faced with this negative result, we introduce the local equivalence query ($\mathsf{LEQ}$) oracle, which returns whether the hypothesis and target concept agree in the perturbation region around a point in the training sample, as well as a counterexample if it exists. We show a separation result: on the one hand, if the query radius $λ$ is strictly smaller than the adversary's perturbation budget $ρ$, then distribution-free robust learning is impossible for a wide variety of concept classes; on the other hand, the setting $λ=ρ$ allows us to develop robust ERM algorithms. We then bound the query complexity of these algorithms based on online learning guarantees and further improve these bounds for the special case of conjunctions. We finish by giving robust learning algorithms for halfspaces on $\{0,1\}^n$ and then obtaining robustness guarantees for halfspaces in $\mathbb{R}^n$ against precision-bounded adversaries.
△ Less
Submitted 20 July, 2023; v1 submitted 12 October, 2022;
originally announced October 2022.
-
Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set
Authors:
Julian D'Costa,
Engel Lefaucheux,
Eike Neumann,
Joël Ouaknine,
James Worrell
Abstract:
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to de…
▽ More
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to define the semialgebraic set, and singly exponential in the bitsize of the coefficients of these polynomials and the bitsize of the matrix entries. We show that our bound is tight by providing a matching lower bound.
△ Less
Submitted 5 August, 2022; v1 submitted 4 July, 2022;
originally announced July 2022.
-
What's Decidable about Discrete Linear Dynamical Systems?
Authors:
Toghrul Karimov,
Edon Kelmendi,
Joël Ouaknine,
James Worrell
Abstract:
We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem.
We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem.
△ Less
Submitted 19 September, 2022; v1 submitted 22 June, 2022;
originally announced June 2022.
-
Probabilistic Automata of Bounded Ambiguity
Authors:
Nathanaël Fijalkow,
Cristian Riveros,
James Worrell
Abstract:
Probabilistic automata are an extension of nondeterministic finite automata in which transitions are annotated with probabilities. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are undecidable. In this work we focus on the emptiness problem (and its variant the value problem), which asks whether a given probabilistic automaton accepts some w…
▽ More
Probabilistic automata are an extension of nondeterministic finite automata in which transitions are annotated with probabilities. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are undecidable. In this work we focus on the emptiness problem (and its variant the value problem), which asks whether a given probabilistic automaton accepts some word with probability greater than a given threshold. We consider a natural and well-studied structural restriction on automata, namely the degree of ambiguity, which is defined as the maximum number of accepting runs over all words. The known undecidability proofs exploits infinite ambiguity and so we focus on the case of finitely ambiguous probabilistic automata. Our main contributions are to construct efficient algorithms for analysing finitely ambiguous probabilistic automata through a reduction to a multi-objective optimisation problem called the stochastic path problem. We obtain a polynomial time algorithm for approximating the value of probabilistic automata of fixed ambiguity and a quasi-polynomial time algorithm for the emptiness problem for 2-ambiguous probabilistic automata. We complement these positive results by an inapproximability result stating that the value of finitely ambiguous probabilistic automata cannot be approximated unless PTIME = NP.
△ Less
Submitted 19 May, 2022; v1 submitted 17 May, 2022;
originally announced May 2022.
-
Sample Complexity Bounds for Robustly Learning Decision Lists against Evasion Attacks
Authors:
Pascale Gourdeau,
Varun Kanade,
Marta Kwiatkowska,
James Worrell
Abstract:
A fundamental problem in adversarial machine learning is to quantify how much training data is needed in the presence of evasion attacks. In this paper we address this issue within the framework of PAC learning, focusing on the class of decision lists. Given that distributional assumptions are essential in the adversarial setting, we work with probability distributions on the input data that satis…
▽ More
A fundamental problem in adversarial machine learning is to quantify how much training data is needed in the presence of evasion attacks. In this paper we address this issue within the framework of PAC learning, focusing on the class of decision lists. Given that distributional assumptions are essential in the adversarial setting, we work with probability distributions on the input data that satisfy a Lipschitz condition: nearby points have similar probability. Our key results illustrate that the adversary's budget (that is, the number of bits it can perturb on each input) is a fundamental quantity in determining the sample complexity of robust learning. Our first main result is a sample-complexity lower bound: the class of monotone conjunctions (essentially the simplest non-trivial hypothesis class on the Boolean hypercube) and any superclass has sample complexity at least exponential in the adversary's budget. Our second main result is a corresponding upper bound: for every fixed $k$ the class of $k$-decision lists has polynomial sample complexity against a $\log(n)$-bounded adversary. This sheds further light on the question of whether an efficient PAC learning algorithm can always be used as an efficient $\log(n)$-robust learning algorithm under the uniform distribution.
△ Less
Submitted 12 May, 2022;
originally announced May 2022.
-
Skolem Meets Schanuel
Authors:
Yuri Bilu,
Florian Luca,
Joris Nieuwveld,
Joël Ouaknine,
David Purser,
James Worrell
Abstract:
The celebrated Skolem-Mahler-Lech Theorem states that the set of zeros of a linear recurrence sequence is the union of a finite set and finitely many arithmetic progressions. The corresponding computational question, the Skolem Problem, asks to determine whether a given linear recurrence sequence has a zero term. Although the Skolem-Mahler-Lech Theorem is almost 90 years old, decidability of the S…
▽ More
The celebrated Skolem-Mahler-Lech Theorem states that the set of zeros of a linear recurrence sequence is the union of a finite set and finitely many arithmetic progressions. The corresponding computational question, the Skolem Problem, asks to determine whether a given linear recurrence sequence has a zero term. Although the Skolem-Mahler-Lech Theorem is almost 90 years old, decidability of the Skolem Problem remains open. The main contribution of this paper is an algorithm to solve the Skolem Problem for simple linear recurrence sequences (those with simple characteristic roots). Whenever the algorithm terminates, it produces a stand-alone certificate that its output is correct -- a set of zeros together with a collection of witnesses that no further zeros exist. We give a proof that the algorithm always terminates assuming two classical number-theoretic conjectures: the Skolem Conjecture (also known as the Exponential Local-Global Principle) and the $p$-adic Schanuel Conjecture. Preliminary experiments with an implementation of this algorithm within the tool \textsc{Skolem} point to the practical applicability of this method.
△ Less
Submitted 28 April, 2022;
originally announced April 2022.
-
The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems
Authors:
Julian D'Costa,
Toghrul Karimov,
Rupak Majumdar,
Joël Ouaknine,
Mahmoud Salamati,
James Worrell
Abstract:
We study fundamental reachability problems on pseudo-orbits of linear dynamical systems. Pseudo-orbits can be viewed as a model of computation with limited precision and pseudo-reachability can be thought of as a robust version of classical reachability. Using an approach based on $o$-minimality of $\reals_{\exp}$ we prove decidability of the discrete-time pseudo-reachability problem with arbitrar…
▽ More
We study fundamental reachability problems on pseudo-orbits of linear dynamical systems. Pseudo-orbits can be viewed as a model of computation with limited precision and pseudo-reachability can be thought of as a robust version of classical reachability. Using an approach based on $o$-minimality of $\reals_{\exp}$ we prove decidability of the discrete-time pseudo-reachability problem with arbitrary semialgebraic targets for diagonalisable linear dynamical systems. We also show that our method can be used to reduce the continuous-time pseudo-reachability problem to the (classical) time-bounded reachability problem, which is known to be conditionally decidable.
△ Less
Submitted 5 July, 2022; v1 submitted 26 April, 2022;
originally announced April 2022.
-
On the transcendence of a series related to Sturmian words
Authors:
Florian Luca,
Joël Ouaknine,
James Worrell
Abstract:
Let $b$ be an algebraic number with $|b|>1$ and $\mathcal{H}$ a finite set of algebraic numbers. We study the transcendence of numbers of the form $\sum_{n=0}^\infty \frac{a_n}{b^n}$ where $a_n \in \mathcal{H}$ for all $n\in\mathbb{N}$. We assume that the sequence $(a_n)_{n=0}^\infty$ is generated by coding the orbit of a point under an irrational rotation of the unit circle. In particular, this a…
▽ More
Let $b$ be an algebraic number with $|b|>1$ and $\mathcal{H}$ a finite set of algebraic numbers. We study the transcendence of numbers of the form $\sum_{n=0}^\infty \frac{a_n}{b^n}$ where $a_n \in \mathcal{H}$ for all $n\in\mathbb{N}$. We assume that the sequence $(a_n)_{n=0}^\infty$ is generated by coding the orbit of a point under an irrational rotation of the unit circle. In particular, this assumption holds whenever the sequence is Sturmian. Our main result shows that all numbers of the above form are transcendental. We moreover give sufficient conditions for a finite set of such numbers to be linearly independent over~$\bar{\mathbb{Q}}$.
△ Less
Submitted 10 June, 2022; v1 submitted 18 April, 2022;
originally announced April 2022.
-
Identity Testing for Radical Expressions
Authors:
Nikhil Balaji,
Klara Nosan,
Mahsa Shirmohammadi,
James Worrell
Abstract:
We study the Radical Identity Testing problem (RIT): Given an algebraic circuit representing a polynomial $f\in \mathbb{Z}[x_1, \ldots, x_k]$ and nonnegative integers $a_1, \ldots, a_k$ and $d_1, \ldots,$ $d_k$, written in binary, test whether the polynomial vanishes at the real radicals $\sqrt[d_1]{a_1}, \ldots,\sqrt[d_k]{a_k}$, i.e., test whether $f(\sqrt[d_1]{a_1}, \ldots,\sqrt[d_k]{a_k}) = 0$.…
▽ More
We study the Radical Identity Testing problem (RIT): Given an algebraic circuit representing a polynomial $f\in \mathbb{Z}[x_1, \ldots, x_k]$ and nonnegative integers $a_1, \ldots, a_k$ and $d_1, \ldots,$ $d_k$, written in binary, test whether the polynomial vanishes at the real radicals $\sqrt[d_1]{a_1}, \ldots,\sqrt[d_k]{a_k}$, i.e., test whether $f(\sqrt[d_1]{a_1}, \ldots,\sqrt[d_k]{a_k}) = 0$. We place the problem in coNP assuming the Generalised Riemann Hypothesis (GRH), improving on the straightforward PSPACE upper bound obtained by reduction to the existential theory of reals. Next we consider a restricted version, called $2$-RIT, where the radicals are square roots of prime numbers, written in binary. It was known since the work of Chen and Kao that $2$-RIT is at least as hard as the polynomial identity testing problem, however no better upper bound than PSPACE was known prior to our work. We show that $2$-RIT is in coRP assuming GRH and in coNP unconditionally. Our proof relies on theorems from algebraic and analytic number theory, such as the Chebotarev density theorem and quadratic reciprocity.
△ Less
Submitted 1 June, 2022; v1 submitted 16 February, 2022;
originally announced February 2022.
-
The Membership Problem for Hypergeometric Sequences with Rational Parameters
Authors:
Klara Nosan,
Amaury Pouly,
Mahsa Shirmohammadi,
James Worrell
Abstract:
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…
▽ More
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.
△ Less
Submitted 24 May, 2022; v1 submitted 15 February, 2022;
originally announced February 2022.
-
On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets
Authors:
Julian D'Costa,
Engel Lefaucheux,
Eike Neumann,
Joël Ouaknine,
James Worrell
Abstract:
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent chara…
▽ More
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.
△ Less
Submitted 5 July, 2021;
originally announced July 2021.
-
On the Computation of the Zariski Closure of Finitely Generated Groups of Matrices
Authors:
Klara Nosan,
Amaury Pouly,
Sylvain Schmitz,
Mahsa Shirmohammadi,
James Worrell
Abstract:
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 th…
▽ More
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.
△ Less
Submitted 7 June, 2022; v1 submitted 3 June, 2021;
originally announced June 2021.
-
Porous Invariants
Authors:
Engel Lefaucheux,
Joël Ouaknine,
David Purser,
James Worrell
Abstract:
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many 'holes'. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting clas…
▽ More
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many 'holes'. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets.
△ Less
Submitted 1 June, 2021;
originally announced June 2021.
-
The Orbit Problem for Parametric Linear Dynamical Systems
Authors:
Christel Baier,
Florian Funke,
Simon Jantsch,
Toghrul Karimov,
Engel Lefaucheux,
Florian Luca,
Joël Ouaknine,
David Purser,
Markus A. Whiteland,
James Worrell
Abstract:
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters.
More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric poi…
▽ More
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters.
More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix $N \in \mathbb{R}^{d\times d}$, and a positive integer $n\in \mathbb{N}$, such that $N^nu = v$.
We show decidability for the case in which $M$ depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.
△ Less
Submitted 13 August, 2021; v1 submitted 21 April, 2021;
originally announced April 2021.
-
Deciding $ω$-Regular Properties on Linear Recurrence Sequences
Authors:
Shaull Almagor,
Toghrul Karimov,
Edon Kelmendi,
Jöel Ouaknine,
James Worrell
Abstract:
We consider the problem of deciding $ω$-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent $ω$-regular property and a sequence of numbers satisfying a linear recurre…
▽ More
We consider the problem of deciding $ω$-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent $ω$-regular property and a sequence of numbers satisfying a linear recurrence, and determines whether the sign description of the sequence (obtained by replacing each positive entry with "$+$", each negative entry with "$-$", and each zero entry with "$0$") satisfies the given property. Our procedure requires that the recurrence be simple, \ie, that the update matrix of the underlying loop be diagonalisable. This assumption is instrumental in proving our key technical lemma: namely that the sign description of a simple linear recurrence sequence is almost periodic in the sense of Muchnik, Semënov, and Ushakov. To complement this lemma, we give an example of a linear recurrence sequence whose sign description fails to be almost periodic. Generalising from sign descriptions, we also consider the verification of properties involving semi-algebraic predicates on program variables.
△ Less
Submitted 27 October, 2020;
originally announced October 2020.
-
Cyclotomic Identity Testing and Applications
Authors:
Nikhil Balaji,
Sylvain Perifel,
Mahsa Shirmohammadi,
James Worrell
Abstract:
We consider the cyclotomic identity testing (CIT) problem: given a polynomial $f(x_1,\ldots,x_k)$, decide whether $f(ζ_n^{e_1},\ldots,ζ_n^{e_k})$ is zero, where $ζ_n = e^{2πi/n}$ is a primitive complex $n$-th root of unity and $e_1,\ldots,e_k$ are integers, represented in binary. When $f$ is given by an algebraic circuit, we give a randomized polynomial-time algorithm for CIT assuming the generali…
▽ More
We consider the cyclotomic identity testing (CIT) problem: given a polynomial $f(x_1,\ldots,x_k)$, decide whether $f(ζ_n^{e_1},\ldots,ζ_n^{e_k})$ is zero, where $ζ_n = e^{2πi/n}$ is a primitive complex $n$-th root of unity and $e_1,\ldots,e_k$ are integers, represented in binary. When $f$ is given by an algebraic circuit, we give a randomized polynomial-time algorithm for CIT assuming the generalised Riemann hypothesis (GRH), and show that the problem is in coNP unconditionally. When $f$ is given by a circuit of polynomially bounded degree, we give a randomized NC algorithm. In case $f$ is a linear form we show that the problem lies in NC. Towards understanding when CIT can be solved in deterministic polynomial-time, we consider so-called diagonal depth-3 circuits, i.e., polynomials $f=\sum_{i=1}^m g_i^{d_i}$, where $g_i$ is a linear form and $d_i$ a positive integer given in unary. We observe that a polynomial-time algorithm for CIT on this class would yield a sub-exponential-time algorithm for polynomial identity testing. However, assuming GRH, we show that if the linear forms~$g_i$ are all identical then CIT can be solved in polynomial time. Finally, we use our results to give a new proof that equality of compressed strings, i.e., strings presented using context-free grammars, can be decided in randomized NC.
△ Less
Submitted 4 May, 2021; v1 submitted 26 July, 2020;
originally announced July 2020.
-
On Positivity and Minimality for Second-Order Holonomic Sequences
Authors:
George Kenison,
Oleksiy Klurman,
Engel Lefaucheux,
Florian Luca,
Pieter Moree,
Joël Ouaknine,
Markus A. Whiteland,
James Worrell
Abstract:
An infinite sequence $\langle{u_n}\rangle_{n\in\mathbb{N}}$ of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle{v_n}\rangle_{n \in\mathbb{N}}$ satisfying the same recurrence re…
▽ More
An infinite sequence $\langle{u_n}\rangle_{n\in\mathbb{N}}$ of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle{v_n}\rangle_{n \in\mathbb{N}}$ satisfying the same recurrence relation, the ratio $u_n/v_n$ converges to $0$. In this paper, we focus on holonomic sequences satisfying a second-order recurrence $g_3(n)u_n = g_2(n)u_{n-1} + g_1(n)u_{n-2}$, where each coefficient $g_3, g_2,g_1 \in \mathbb{Q}[n]$ is a polynomial of degree at most $1$. We establish two main results. First, we show that deciding positivity for such sequences reduces to deciding minimality. And second, we prove that deciding minimality is equivalent to determining whether certain numerical expressions (known as periods, exponential periods, and period-like integrals) are equal to zero. Periods and related expressions are classical objects of study in algebraic geometry and number theory, and several established conjectures (notably those of Kontsevich and Zagier) imply that they have a decidable equality problem, which in turn would entail decidability of Positivity and Minimality for a large class of second-order holonomic sequences.
△ Less
Submitted 23 July, 2020;
originally announced July 2020.
-
On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems
Authors:
Toghrul Karimov,
Joël Ouaknine,
James Worrell
Abstract:
Consider a discrete dynamical system given by a square matrix $M \in \mathbb{Q}^{d \times d}$ and a starting point $s \in \mathbb{Q}^d$. The orbit of such a system is the infinite trajectory $\langle s, Ms, M^2s, \ldots\rangle$. Given a collection $T_1, T_2, \ldots, T_m \subseteq \mathbb{R}^d$ of semialgebraic sets, we can associate with each $T_i$ an atomic proposition $P_i$ which evaluates to tr…
▽ More
Consider a discrete dynamical system given by a square matrix $M \in \mathbb{Q}^{d \times d}$ and a starting point $s \in \mathbb{Q}^d$. The orbit of such a system is the infinite trajectory $\langle s, Ms, M^2s, \ldots\rangle$. Given a collection $T_1, T_2, \ldots, T_m \subseteq \mathbb{R}^d$ of semialgebraic sets, we can associate with each $T_i$ an atomic proposition $P_i$ which evaluates to true at time $n$ if, and only if, $M^ns \in T_i$. This gives rise to the LTL Model-Checking Problem for discrete linear dynamical systems: given such a system $(M,s)$ and an LTL formula over such atomic propositions, determine whether the orbit satisfies the formula. The main contribution of the present paper is to show that the LTL Model-Checking Problem for discrete linear dynamical systems is decidable in dimension 3 or less.
△ Less
Submitted 9 July, 2020; v1 submitted 6 July, 2020;
originally announced July 2020.
-
On the Skolem Problem and Prime Powers
Authors:
George Kenison,
Richard Lipton,
Joël Ouaknine,
James Worrell
Abstract:
The Skolem Problem asks, given a linear recurrence sequence $(u_n)$, whether there exists $n\in\mathbb{N}$ such that $u_n=0$. In this paper we consider the following specialisation of the problem: given in addition $c\in\mathbb{N}$, determine whether there exists $n\in\mathbb{N}$ of the form $n=lp^k$, with $k,l\leq c$ and $p$ any prime number, such that $u_n=0$.
The Skolem Problem asks, given a linear recurrence sequence $(u_n)$, whether there exists $n\in\mathbb{N}$ such that $u_n=0$. In this paper we consider the following specialisation of the problem: given in addition $c\in\mathbb{N}$, determine whether there exists $n\in\mathbb{N}$ of the form $n=lp^k$, with $k,l\leq c$ and $p$ any prime number, such that $u_n=0$.
△ Less
Submitted 12 June, 2020;
originally announced June 2020.
-
Invariants for Continuous Linear Dynamical Systems
Authors:
Shaull Almagor,
Edon Kelmendi,
Joël Ouaknine,
James Worrell
Abstract:
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of…
▽ More
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel's conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel's conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.
△ Less
Submitted 28 April, 2020; v1 submitted 24 April, 2020;
originally announced April 2020.
-
How Fast Can You Escape a Compact Polytope?
Authors:
Julian D'Costa,
Engel Lefaucheux,
Joël Ouaknine,
James Worrell
Abstract:
The Continuous Polytope Escape Problem (CPEP) asks whether every trajectory of a linear differential equation initialised within a convex polytope eventually escapes the polytope. We provide a polynomial-time algorithm to decide CPEP for compact polytopes. We also establish a quantitative uniform upper bound on the time required for every trajectory to escape the given polytope. In addition, we es…
▽ More
The Continuous Polytope Escape Problem (CPEP) asks whether every trajectory of a linear differential equation initialised within a convex polytope eventually escapes the polytope. We provide a polynomial-time algorithm to decide CPEP for compact polytopes. We also establish a quantitative uniform upper bound on the time required for every trajectory to escape the given polytope. In addition, we establish iteration bounds for termination of discrete linear loops via reduction to the continuous case.
△ Less
Submitted 14 January, 2020;
originally announced January 2020.
-
On the Hardness of Robust Classification
Authors:
Pascale Gourdeau,
Varun Kanade,
Marta Kwiatkowska,
James Worrell
Abstract:
It is becoming increasingly important to understand the vulnerability of machine learning models to adversarial attacks. In this paper we study the feasibility of robust learning from the perspective of computational learning theory, considering both sample and computational complexity. In particular, our definition of robust learnability requires polynomial sample complexity. We start with two ne…
▽ More
It is becoming increasingly important to understand the vulnerability of machine learning models to adversarial attacks. In this paper we study the feasibility of robust learning from the perspective of computational learning theory, considering both sample and computational complexity. In particular, our definition of robust learnability requires polynomial sample complexity. We start with two negative results. We show that no non-trivial concept class can be robustly learned in the distribution-free setting against an adversary who can perturb just a single input bit. We show moreover that the class of monotone conjunctions cannot be robustly learned under the uniform distribution against an adversary who can perturb $ω(\log n)$ input bits. However if the adversary is restricted to perturbing $O(\log n)$ bits, then the class of monotone conjunctions can be robustly learned with respect to a general class of distributions (that includes the uniform distribution). Finally, we provide a simple proof of the computational hardness of robust learning on the boolean hypercube. Unlike previous results of this nature, our result does not rely on another computational model (e.g. the statistical query model) nor on any hardness assumption other than the existence of a hard learning problem in the PAC framework.
△ Less
Submitted 12 September, 2019;
originally announced September 2019.
-
On the Monniaux Problem in Abstract Interpretation
Authors:
Nathanaël Fijalkow,
Engel Lefaucheux,
Pierre Ohlmann,
Joël Ouaknine,
Amaury Pouly,
James Worrell
Abstract:
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 $\varphi$, 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 $\varphi$. The Monniaux Probl…
▽ More
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 $\varphi$, 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 $\varphi$. 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.
△ Less
Submitted 18 July, 2019;
originally announced July 2019.
-
Effective Definability of the Reachability Relation in Timed Automata
Authors:
Martin Fränzle,
Karin Quaas,
Mahsa Shirmohammadi,
James Worrell
Abstract:
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.
△ Less
Submitted 23 March, 2019;
originally announced March 2019.
-
Algebraic Invariants for Linear Hybrid Automata
Authors:
Rupak Majumdar,
Joël Ouaknine,
Amaury Pouly,
James Worrell
Abstract:
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 resu…
▽ More
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.
△ Less
Submitted 27 February, 2019;
originally announced February 2019.
-
On Reachability Problems for Low-Dimensional Matrix Semigroups
Authors:
Thomas Colcombet,
Joël Ouaknine,
Pavel Semukhin,
James Worrell
Abstract:
We consider the Membership and the Half-Space Reachability problems for matrices in dimensions two and three. Our first main result is that the Membership Problem is decidable for finitely generated sub-semigroups of the Heisenberg group over rational numbers. Furthermore, we prove two decidability results for the Half-Space Reachability Problem. Namely, we show that this problem is decidable for…
▽ More
We consider the Membership and the Half-Space Reachability problems for matrices in dimensions two and three. Our first main result is that the Membership Problem is decidable for finitely generated sub-semigroups of the Heisenberg group over rational numbers. Furthermore, we prove two decidability results for the Half-Space Reachability Problem. Namely, we show that this problem is decidable for sub-semigroups of $\mathrm{GL}(2,\mathbb{Z})$ and of the Heisenberg group over rational numbers.
△ Less
Submitted 29 April, 2019; v1 submitted 25 February, 2019;
originally announced February 2019.
-
Termination of Linear Loops over the Integers
Authors:
Mehran Hosseini,
Joël Ouaknine,
James Worrell
Abstract:
We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable, but the general case has remained open since being conjectured decidable…
▽ More
We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable, but the general case has remained open since being conjectured decidable by Tiwari in 2004. In this paper we show decidability of determining termination for arbitrary update matrices, confirming Tiwari's conjecture. For the class of loops considered in this paper, the question of deciding termination on a specific initial value is a longstanding open problem in number theory. The key to our decision procedure is in showing how to circumvent the difficulties inherent in deciding termination on a fixed initial value.
△ Less
Submitted 20 November, 2021; v1 submitted 20 February, 2019;
originally announced February 2019.
-
Coverability in 1-VASS with Disequality Tests
Authors:
Shaull Almagor,
Nathann Cohen,
Guillermo A. Pérez,
Mahsa Shirmohammadi,
James Worrell
Abstract:
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the…
▽ More
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.
△ Less
Submitted 7 September, 2020; v1 submitted 18 February, 2019;
originally announced February 2019.
-
The Semialgebraic Orbit Problem
Authors:
Shaull Almagor,
Joël Oukanine,
James Worrell
Abstract:
The Semialgebraic Orbit Problem is a fundamental reachability question that arises in the analysis of discrete-time linear dynamical systems such as automata, Markov chains, recurrence sequences, and linear while loops. An instance of the problem comprises a dimension $d\in\mathbb{N}$, a square matrix $A\in\mathbb{Q}^{d\times d}$, and semialgebraic source and target sets…
▽ More
The Semialgebraic Orbit Problem is a fundamental reachability question that arises in the analysis of discrete-time linear dynamical systems such as automata, Markov chains, recurrence sequences, and linear while loops. An instance of the problem comprises a dimension $d\in\mathbb{N}$, a square matrix $A\in\mathbb{Q}^{d\times d}$, and semialgebraic source and target sets $S,T\subseteq \mathbb{R}^d$. The question is whether there exists $x\in S$ and $n\in\mathbb{N}$ such that $A^nx \in T$. The main result of this paper is that the Semialgebraic Orbit Problem is decidable for dimension $d\leq 3$. Our decision procedure relies on separation bounds for algebraic numbers as well as a classical result of transcendental number theory---Baker's theorem on linear forms in logarithms of algebraic numbers. We moreover argue that our main result represents a natural limit to what can be decided (with respect to reachability) about the orbit of a single matrix. On the one hand, semialgebraic sets are arguably the largest general class of subsets of $\mathbb{R}^d$ for which membership is decidable. On the other hand, previous work has shown that in dimension $d=4$, giving a decision procedure for the special case of the Orbit Problem with singleton source set $S$ and polytope target set $T$ would entail major breakthroughs in Diophantine approximation.
△ Less
Submitted 30 January, 2019;
originally announced January 2019.
-
Effective Divergence Analysis for Linear Recurrence Sequences
Authors:
Shaull Almagor,
Brynmor Chapman,
Mehran Hosseini,
Joël Ouaknine,
James Worrell
Abstract:
We study the growth behaviour of rational linear recurrence sequences. We show that for low-order sequences, divergence is decidable in polynomial time. We also exhibit a polynomial-time algorithm which takes as input a divergent rational linear recurrence sequence and computes effective fine-grained lower bounds on the growth rate of the sequence.
We study the growth behaviour of rational linear recurrence sequences. We show that for low-order sequences, divergence is decidable in polynomial time. We also exhibit a polynomial-time algorithm which takes as input a divergent rational linear recurrence sequence and computes effective fine-grained lower bounds on the growth rate of the sequence.
△ Less
Submitted 19 November, 2021; v1 submitted 20 June, 2018;
originally announced June 2018.
-
When is Containment Decidable for Probabilistic Automata?
Authors:
Laure Daviaud,
Marcin Jurdziński,
Ranko Lazić,
Filip Mazowiecki,
Guillermo A. Pérez,
James Worrell
Abstract:
The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable. In this paper we provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the…
▽ More
The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable. In this paper we provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the emptiness problem (that is known be undecidable in general) becomes decidable for automata of polynomial ambiguity. We complement this positive result by showing that the emptiness problem remains undecidable even when restricted to automata of linear ambiguity. We then turn to finitely ambiguous automata. Here we show decidability of containment in case one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Our proof of this last result relies on the decidability of the theory of real exponentiation, which has been shown, subject to Schanuel's Conjecture, by Macintyre and Wilkie.
△ Less
Submitted 29 March, 2020; v1 submitted 24 April, 2018;
originally announced April 2018.
-
On the Expressiveness and Monitoring of Metric Temporal Logic
Authors:
Hsi-Ming Ho,
Joël Ouaknine,
James Worrell
Abstract:
It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this remains true even when the time domain is bounded a priori. In this work, we present an extension of MTL with the same expressive power as FO[<, +1] over bounded timed words (and also, trivially, over time-bounded signal…
▽ More
It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this remains true even when the time domain is bounded a priori. In this work, we present an extension of MTL with the same expressive power as FO[<, +1] over bounded timed words (and also, trivially, over time-bounded signals). We then show that expressive completeness also holds in the general (time-unbounded) case if we allow the use of rational constants $q \in \mathbb{Q}$ in formulas. This extended version of MTL therefore yields a definitive real-time analogue of Kamp's theorem. As an application, we propose a trace-length independent monitoring procedure for our extension of MTL, the first such procedure in a dense real-time setting.
△ Less
Submitted 9 May, 2019; v1 submitted 7 March, 2018;
originally announced March 2018.
-
Costs and Rewards in Priced Timed Automata
Authors:
Martin Fränzle,
Mahsa Shirmohammadi,
Mani Swaminathan,
James Worrell
Abstract:
We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA.
We study the Pareto Domination Problem, which asks whether it is possi…
▽ More
We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA.
We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers.
We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.
△ Less
Submitted 15 May, 2018; v1 submitted 5 March, 2018;
originally announced March 2018.
