Joël Ouaknine

AAAI Conference 2026 Conference Paper

Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

• Rajab Aghamov
• Christel Baier
• Joël Ouaknine
• Jakob Piribauer
• Mihir Vahanwala
• Isa Vialard

Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding whether a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, which is a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is hard for both NP and coNP. We also identify natural restrictions on the graphical structure of the DBN that make the verification of structural CI properties tractable.

TCS Journal 2025 Journal Article

Convex language semantics for nondeterministic probabilistic automata

• Gerco van Heerdt
• Justin Hsu
• Joël Ouaknine
• Alexandra Silva

We explore language semantics for automata combining probabilistic and nondeterministic behaviors. We first show that there are precisely two natural semantics for probabilistic automata with nondeterminism. For both choices, we show that these automata are strictly more expressive than deterministic probabilistic automata, and we prove that the problem of checking language equivalence is undecidable by reduction from the threshold problem. However, we provide a discounted metric that can be computed to arbitrarily high precision.

KR Conference 2025 Conference Paper

Model Checking Linear Temporal Logic with Standpoint Modalities

• Rajab Aghamov
• Christel Baier
• Toghrul Karimov
• Rupak Majumdar
• Joël Ouaknine
• Jakob Piribauer
• Timm Spork

Standpoint linear temporal logic (SLTL) is a recently introduced extension of classical linear temporal logic (LTL) with standpoint modalities. Intuitively, these modalities allow to express that, from agent a's standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to SLTL under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the SLTL satisfiability problem.

MFCS Conference 2025 Conference Paper

On Expansions of Monadic Second-Order Logic with Dynamical Predicates

• Joris Nieuwveld
• Joël Ouaknine

Expansions of the monadic second-order (MSO) theory of the structure ⟨ℕ; <⟩ have been a fertile and active area of research ever since the publication of the seminal papers of Büchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of ⟨ℕ; <, P⟩, where P ranges over a large class of unary "dynamical" predicates, i. e. , sets of non-negative values assumed by certain integer linear recurrence sequences. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield.

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.

Highlights Conference 2025 Conference Abstract

On large zeros of linear recurrence sequences

• Joël Ouaknine

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

TCS Journal 2025 Journal Article

The monadic theory of toric words

• Valérie Berthé
• Toghrul Karimov
• Joris Nieuwveld
• Joël Ouaknine
• Mihir Vahanwala
• James Worrell

For which unary predicates P 1, …, P m is the MSO theory of the structure 〈 N; <, P 1, …, P m 〉 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. We give various applications of toric words, including the recent result of [1] that the MSO theory of 〈 N; <, { 2 n: n ∈ N }, { 3 n: n ∈ N } 〉 is decidable.

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.

Highlights Conference 2021 Conference Abstract

Holonomic Techniques, Periods, and Decision Problems

• Joël Ouaknine

Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I give an overview of the area, and in particular present a select survey of known and original results on decision problems for holonomic sequences and functions. I also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.

MFCS Conference 2021 Conference Paper

Holonomic Techniques, Periods, and Decision Problems (Invited Talk)

• Joël Ouaknine

Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades (see, e. g. , [Doron Zeilberger, 1990; Petkovšek et al. , 1997]). In this talk, I give an overview of the area, and in particular present a select survey of known and original results on decision problems for holonomic sequences and functions. I also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier. Parts of this exposition draws upon [George Kenison et al. , 2021].

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.

TCS Journal 2018 Journal Article

Reachability Problems 2014: Special issue

• Joël Ouaknine
• Igor Potapov
• James Worrell

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.

Highlights Conference 2013 Conference Abstract

On the complexity of path checking in temporal logics

• Daniel Bundala
• Joël Ouaknine

Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given word. For LTL, the complexity of this task was recently shown to be in NC hierarchy. In this paper, we establish a connection between LTL path checking and planar circuits. We use the connection to show that the path-checking problem for LTL extended with exclusive or is already P-hard. We then present an NC algorithm for MTL, a quantitative (or metric) extension of LTL and give an AC-1 algorithm for UTL, the unary fragment of LTL.

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.

TCS Journal 2005 Journal Article

Domain theory, testing and simulation for labelled Markov processes

• Franck van Breugel
• Michael Mislove
• Joël Ouaknine
• James Worrell

This paper presents a fundamental study of similarity and bisimilarity for labelled Markov processes (LMPs). The main results characterize similarity as a testing preorder and bisimilarity as a testing equivalence. In general, LMPs are not required to satisfy a finite-branching condition—indeed the state space may be a continuum, with the transitions given by arbitrary probability measures. Nevertheless we show that to characterize bisimilarity it suffices to use finitely-branching labelled trees as tests. Our results involve an interaction between domain theory and measure theory. One of the main technical contributions is to show that a final object in a suitable category of LMPs can be constructed by solving a domain equation D ≅ V ( D ) Act, where V is the probabilistic powerdomain. Given an LMP whose state space is an analytic space, bisimilarity arises as the kernel of the unique map to the final LMP. We also show that the metric for approximate bisimilarity introduced by Desharnais, Gupta, Jagadeesan and Panangaden generates the Lawson topology on the domain D.