James Worrell 0001

MFCS Conference 2025 Conference Paper

On Large Zeros of Linear Recurrence Sequences

• Florian Luca
• Joël Ouaknine
• James Worrell 0001

The Skolem Problem asks to determine whether a given integer linear recurrence sequence (LRS) has a zero term. This problem, whose decidability has been open for many decades, arises across a wide range of topics in computer science, including loop termination, formal languages, automata theory, and probabilistic model checking, amongst many others. In the present paper, we introduce a notion of "large" zeros of (non-degenerate) linear recurrence sequences, i. e. , zeros occurring at an index larger than a sixth-fold exponential of the size of the data defining the given LRS. We establish two main results. First, we show that large zeros are very sparse: the set of positive integers that can possibly arise as large zeros of some LRS has null density. This in turn immediately yields a Universal Skolem Set of density one, answering a question left open in the literature. Second, we define an infinite set of prime numbers, termed "good", having density one amongst all prime numbers, with the following property: for any large zero of a given LRS, there is an interval around the large zero together with an upper bound on the number of good primes possibly present in that interval. The bound in question is much lower than one would expect if good primes were distributed similarly as ordinary prime numbers, as per the Cramér model in number theory. We therefore conjecture that large zeros do not exist, which would entail decidability of the Skolem Problem.

SODA Conference 2025 Conference Paper

On the Decidability of Presburger Arithmetic Expanded with Powers

• Toghrul Karimov
• Florian Luca
• Joris Nieuwveld
• Joël Ouaknine
• James Worrell 0001

CSL Conference 2025 Conference Paper

Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

• Andrew Scoones
• Mahsa Shirmohammadi
• James Worrell 0001

Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are read-once variables: they do not affect the control flow of the automaton and their value is output only at the end of a run. Thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution - a result of independent interest - is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.

MFCS Conference 2022 Conference Paper

A Universal Skolem Set of Positive Lower Density

• Florian Luca
• Joël Ouaknine
• James Worrell 0001

The Skolem Problem asks to decide whether a given integer linear recurrence sequence (LRS) has a zero term. Decidability of this problem has been open for many decades, with little progress since the 1980s. Recently, a new approach was initiated via the notion of a Skolem set - a set of positive integers relative to which the Skolem Problem is decidable. More precisely, 𝒮 is a Skolem set for a class ℒ of integer LRS if there is an effective procedure that, given an LRS in ℒ, decides whether the sequence has a zero in 𝒮. A recent work exhibited a Skolem set for the class of all LRS that, while infinite, had density zero. In the present work we construct a Skolem set of positive lower density for the class of simple LRS.

MFCS Conference 2022 Conference Paper

Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set

• Julian D'Costa
• Engel Lefaucheux
• Eike Neumann
• Joël Ouaknine
• James Worrell 0001

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.

MFCS Conference 2022 Conference Paper

Skolem Meets Schanuel

• Yuri Bilu
• Florian Luca
• Joris Nieuwveld
• Joël Ouaknine
• David Purser
• James Worrell 0001

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 Skolem point to the practical applicability of this method.

MFCS Conference 2022 Conference Paper

The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems

• Julian D'Costa
• Toghrul Karimov
• Rupak Majumdar
• Joël Ouaknine
• Mahmoud Salamati
• James Worrell 0001

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

MFCS Conference 2021 Conference Paper

On Positivity and Minimality for Second-Order Holonomic Sequences

• George Kenison
• Oleksiy Klurman
• Engel Lefaucheux
• Florian Luca
• Pieter Moree
• Joël Ouaknine
• Markus A. Whiteland
• James Worrell 0001

An infinite sequence ⟨u_n⟩_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 ≥ 0, and minimal if, given any other linearly independent sequence ⟨v_n⟩_n satisfying the same recurrence relation, the ratio u_n/v_n → 0 as n → ∞. In this paper we give a Turing reduction of the problem of deciding positivity of second-order holonomic sequences to that of deciding minimality of such sequences. More specifically, we give a procedure for determining positivity of second-order holonomic sequences that terminates in all but an exceptional number of cases, and we show that in these exceptional cases positivity can be determined using an oracle for deciding minimality.

MFCS Conference 2021 Conference Paper

On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets

• Julian D'Costa
• Engel Lefaucheux
• Eike Neumann
• Joël Ouaknine
• James Worrell 0001

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

MFCS Conference 2021 Conference Paper

The Pseudo-Skolem Problem is Decidable

• Julian D'Costa
• Toghrul Karimov
• Rupak Majumdar
• Joël Ouaknine
• Mahmoud Salamati
• Sadegh Soudjani
• James Worrell 0001

We study fundamental decision problems on linear dynamical systems in discrete time. We focus on pseudo-orbits, the collection of trajectories of the dynamical system for which there is an arbitrarily small perturbation at each step. Pseudo-orbits are generalizations of orbits in the topological theory of dynamical systems. We study the pseudo-orbit problem, whether a state belongs to the pseudo-orbit of another state, and the pseudo-Skolem problem, whether a hyperplane is reachable by an ε-pseudo-orbit for every ε. These problems are analogous to the well-studied orbit problem and Skolem problem on unperturbed dynamical systems. Our main results show that the pseudo-orbit problem is decidable in polynomial time and the Skolem problem on pseudo-orbits is decidable. The former extends the seminal result of Kannan and Lipton from orbits to pseudo-orbits. The latter is in contrast to the Skolem problem for linear dynamical systems, which remains open for proper orbits.

MFCS Conference 2020 Conference Paper

On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems

• Toghrul Karimov
• Joël Ouaknine
• James Worrell 0001

Consider a discrete dynamical system given by a square matrix M ∈ ℚ^{d × d} and a starting point s ∈ ℚ^d. The orbit of such a system is the infinite trajectory ⟨ s, Ms, M²s, …⟩. Given a collection T₁, T₂, …, T_m ⊆ ℝ^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 ∈ 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.

TIME Conference 2020 Conference Paper

Parametric Model Checking Continuous-Time Markov Chains

• Catalin-Andrei Ilie
• James Worrell 0001

CSL is a well-known temporal logic for specifying properties of real-time stochastic systems, such as continuous-time Markov chains. We introduce PCSL, an extension of CSL that allows using existentially quantified parameters in timing constraints, and investigate its expressiveness and decidability over properties of continuous-time Markov chains. Assuming Schanuel’s Conjecture, we prove the decidability of model checking the one-parameter fragment of PCSL on continuous-time Markov chains. Technically, the central problem we solve (relying on Schanuel’s Conjecture) is to decide positivity of real-valued exponential polynomial functions on bounded intervals. A second contribution is to give a reduction of the Positivity Problem for matrix exponentials to the PCSL model checking problem, suggesting that it will be difficult to give an unconditional proof of the decidability of model checking PCSL.

SODA Conference 2017 Conference Paper

On Rationality of Nonnegative Matrix Factorization

• Dmitry Chistikov 0001
• Stefan Kiefer
• Ines Marusic
• Mahsa Shirmohammadi
• James Worrell 0001

Nonnegative matrix factorization ( N MF) is the problem of decomposing a given nonnegative n × m matrix M into a product of a nonnegative n × d matrix W and a nonnegative d × m matrix H. NMF has a wide variety of applications, including bioinformatics, chemometrics, communication complexity, machine learning, polyhedral combinatorics, among many others. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether every rational matrix M has an NMF with minimal d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix M for which W and H require irrational entries. As an application of this result, we show that state minimization of labeled Markov chains can require the introduction of irrational transition probabilities. We complement these irrationality results with an NP- complete version of NMF for which rational numbers suffice.

SODA Conference 2015 Conference Paper

On Termination of Integer Linear Loops

• Joël Ouaknine
• João Sousa Pinto
• James Worrell 0001

A fundamental problem in program verification concerns the termination of simple linear loops of the form: where x is a vector of variables, u, a, and c are integer vectors, and A and B are integer matrices. Assuming the matrix A is diagonalisable, we give a decision procedure for the problem of whether, for all initial integer vectors u, such a loop terminates. The correctness of our algorithm relies on sophisticated tools from algebraic and analytic number theory, Diophantine geometry, and real algebraic geometry. To the best of our knowledge, this is the first substantial advance on a 10-year-old open problem of Tiwari [38] and Braverman [8].

SODA Conference 2015 Conference Paper

The Polyhedron-Hitting Problem

• Ventsislav Chonev
• Joël Ouaknine
• James Worrell 0001

We consider polyhedral versions of Kannan and Lip-ton's Orbit Problem [14, 13]—determining whether a target polyhedron V may be reached from a starting point x under repeated applications of a linear transformation A in an ambient vector space ℚ m. In the context of program verification, very similar reachability questions were also considered and left open by Lee and Yannakakis in [15], and by Braverman in [4]. We present what amounts to a complete characterisation of the decidability landscape for the Polyhedron-Hitting Problem, expressed as a function of the dimension m of the ambient space, together with the dimension of the polyhedral target V: more precisely, for each pair of dimensions, we either establish decidability, or show hardness for longstanding number-theoretic open problems.

SODA Conference 2014 Conference Paper

Positivity Problems for Low-Order Linear Recurrence Sequences

• Joël Ouaknine
• James Worrell 0001

We consider two decision problems for linear recurrence sequences (LRS) over the integers, namely the Positivity Problem (are all terms of a given LRS positive?) and the Ultimate Positivity Problem (are all but finitely many terms of a given LRS positive?). We show decidability of both problems for LRS of order 5 or less, with complexity in the Counting Hierarchy for Positivity, and in polynomial time for Ultimate Positivity. Moreover, we show by way of hardness that extending the decidability of either problem to LRS of order 6 would entail major breakthroughs in analytic number theory, more precisely in the field of Diophantine approximation of transcendental numbers.

STOC Conference 2013 Conference Paper

The orbit problem in higher dimensions

• Ventsislav Chonev
• Joël Ouaknine
• James Worrell 0001

We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem---determining whether a target vector space V may be reached from a starting point x under repeated applications of a linear transformation A . Answering two questions posed by Kannan and Lipton in the 1980s, we show that when V has dimension one, this problem is solvable in polynomial time, and when V has dimension two or three, the problem is in NP RP .

MFCS Conference 2013 Conference Paper

Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian

• Ranko Lazic 0001
• Joël Ouaknine
• James Worrell 0001

Abstract Metric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for its safety fragment was proved decidable several years ago [18]. The problem is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, the complexity has remained elusive, except for a non-elementary lower bound. Via another equivalent problem, namely termination for a class of rational relations, we show that satisfiability for safety MTL is not primitive recursive, yet is Ackermannian, i. e. , among the simplest non-primitive recursive problems. This is surprising since decidability was originally established using Higman’s Lemma, suggesting a much higher non-multiply recursive complexity.

CSL Conference 2011 Conference Paper

The Church Synthesis Problem with Metric

• Mark Jenkins
• Joël Ouaknine
• Alexander Rabinovich
• James Worrell 0001

Church's Problem asks for the construction of a procedure which, given a logical specification S(I, O) between input strings I and output strings O, determines whether there exists an operator F that implements the specification in the sense that S(I, F(I)) holds for all inputs I. Buechi and Landweber gave a procedure to solve Church's problem for MSO specifications and operators computable by finite-state automata. We consider extensions of Church's problem in two orthogonal directions: (i) we address the problem in a more general logical setting, where not only the specifications but also the solutions are presented in a logical system; (ii) we consider not only the canonical discrete time domain of the natural numbers, but also the continuous domain of reals. We show that for every fixed bounded length interval of the reals, Church's problem is decidable when specifications and implementations are described in the monadic second-order logics over the reals with order and the +1 function.

TIME Conference 2008 Conference Paper

Real-Time Model Checking: Algorithms and Complexity

• James Worrell 0001

In this talk we describe a new automata-theoretic approach to model checking real-time systems. We show how this approach yields both upper and lower complexity bounds for various decision problems involving timed automata and temporal logics. To put these developments in context we survey some classical results concerning automata, temporal logic and monadic predicate logic over the reals.