arXiv subjects

Joel Ouaknine

Publications and source records attributed to Joel Ouaknine.

15 recordsLinked to original sources

arXiv2025

Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

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 if a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, 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 NP- and coNP-hard. We also identify natural restrictions on the graphical structure of DBNs that make the verification of structural CI properties tractable.

cs.AI↗

arXiv2025

Transcendence for Pisot Morphic Words over an Algebraic Base

It is known that for a uniform morphic sequence $\boldsymbol u = \langle u_n\rangle_{n=0}^\infty$ and an algebraic number $β$ such that $|β|>1$, the number $[\![\boldsymbol{u} ]\!]_β:=\sum_{n=0}^\infty \frac{u_n}{β^n}$ either lies in $\mathbb Q(β)$ or is transcendental. In this paper we show a similar rational-transcendental dichotomy for sequences defined by irreducible Pisot morphisms. Subject to the Pisot conjecture (an irreducible Pisot morphism has pure discrete spectrum), we generalise the latter result to arbitrary finite alphabets. In certain cases we are able to show transcendence of $[\![\boldsymbol{u}]\!]_β$ outright. In particular, for $k\geq 2$, if $\boldsymbol u$ is the $k$-bonacci word then $[\![\boldsymbol{u}]\!]_β$ is transcendental.

math.NT↗

arXiv2024

Transcendence of Hecke-Mahler Series

We prove transcendence of the Hecke-Mahler series $\sum_{n=0}^\infty f(\lfloor nθ+α\rfloor) β^{-n}$, where $f(x) \in \mathbb{Z}[x]$ is a non-constant polynomial $α$ is a real number, $θ$ is an irrational real number, and $β$ is an algebraic number such that $|β|>1$.

math.NT↗

arXiv2023

Nonnegativity Problems for Matrix Semigroups

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).

cs.LO↗

arXiv2023

Transcendence of Sturmian Numbers over an Algebraic Base

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.

cs.FL↗

arXiv2017

Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences

We consider the decidability and complexity of the Ultimate Positivity Problem, which asks whether all but finitely many terms of a given rational linear recurrence sequence (LRS) are positive. Using lower bounds in Diophantine approximation concerning sums of S-units, we show that for simple LRS (those whose characteristic polynomial has no repeated roots) the Ultimate Positivity Problem is decidable in polynomial space. If we restrict to simple LRS of a fixed order then we obtain a polynomial-time decision procedure. As a complexity lower bound we show that Ultimate Positivity for simple LRS is hard for co$\exists\mathbb{R}$, i.e., the class of problems solvable in the universal theory of the reals (which lies between coNP and PSPACE).

cs.CC↗

arXiv2016

On the Skolem Problem for Continuous Linear Dynamical Systems

The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differential equation has a zero in a given interval of real numbers. This is a fundamental reachability problem for continuous linear dynamical systems, such as linear hybrid automata and continuous-time Markov chains. Decidability of the problem is currently open---indeed decidability is open even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show decidability of the bounded problem subject to Schanuel's Conjecture, a unifying conjecture in transcendental number theory. We furthermore analyse the unbounded problem in terms of the frequencies of the differential equation, that is, the imaginary parts of the characteristic roots. We show that the unbounded problem can be reduced to the bounded problem if there is at most one rationally linearly independent frequency, or if there are two rationally linearly independent frequencies and all characteristic roots are simple. We complete the picture by showing that decidability of the unbounded problem in the case of two (or more) rationally linearly independent frequencies would entail a major new effectiveness result in Diophantine approximation, namely computability of the Diophantine-approximation types of all real algebraic numbers.

eess.SY↗

arXiv2016

On Recurrent Reachability for Continuous Linear Dynamical Systems

The continuous evolution of a wide variety of systems, including continuous-time Markov chains and linear hybrid automata, can be described in terms of linear differential equations. In this paper we study the decision problem of whether the solution $\boldsymbol{x}(t)$ of a system of linear differential equations $d\boldsymbol{x}/dt=A\boldsymbol{x}$ reaches a target halfspace infinitely often. This recurrent reachability problem can equivalently be formulated as the following Infinite Zeros Problem: does a real-valued function $f:\mathbb{R}_{\geq 0}\rightarrow\mathbb{R}$ satisfying a given linear differential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most $7$, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order $9$ (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.

eess.SY↗

arXiv2015

The Cyclic-Routing UAV Problem is PSPACE-Complete

Consider a finite set of targets, with each target assigned a relative deadline, and each pair of targets assigned a fixed transit flight time. Given a flock of identical UAVs, can one ensure that every target is repeatedly visited by some UAV at intervals of duration at most the target's relative deadline? The Cyclic-Routing UAV Problem (CR-UAV) is the question of whether this task has a solution. This problem can straightforwardly be solved in PSPACE by modelling it as a network of timed automata. The special case of there being a single UAV is claimed to be NP-complete in the literature. In this paper, we show that the CR-UAV Problem is in fact PSPACE-complete even in the single-UAV case.

cs.LO↗

arXiv2014

On the Positivity Problem for Simple Linear Recurrence Sequences

Given a linear recurrence sequence (LRS) over the integers, the Positivity Problem} asks whether all terms of the sequence are positive. We show that, for simple LRS (those whose characteristic polynomial has no repeated roots) of order 9 or less, Positivity is decidable, with complexity in the Counting Hierarchy.

cs.DM↗

arXiv2013

Positivity Problems for Low-Order Linear Recurrence Sequences

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.

cs.DM↗

arXiv2013

A Static Analysis Framework for Livelock Freedom in CSP

In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free through a static analysis of their syntax. In particular, we present a collection of rules, based on the inductive structure of terms, which guarantee livelock-freedom of the denoted process. This gives rise to an algorithm which conservatively flags processes that can potentially livelock. We illustrate our approach by applying both BDD-based and SAT-based implementations of our algorithm to a range of benchmarks, and show that our technique in general substantially outperforms the model checker FDR whilst exhibiting a low rate of inconclusive results.

cs.LO↗

arXiv2013

On the Complexity of Equivalence and Minimisation for Q-weighted Automata

This paper is concerned with the computational complexity of equivalence and minimisation for automata with transition weights in the field Q of rational numbers. We use polynomial identity testing and the Isolation Lemma to obtain complexity bounds, focussing on the class NC of problems within P solvable in polylogarithmic parallel time. For finite Q-weighted automata, we give a randomised NC procedure that either outputs that two automata are equivalent or returns a word on which they differ. We also give an NC procedure for deciding whether a given automaton is minimal, as well as a randomised NC procedure that minimises an automaton. We consider probabilistic automata with rewards, similar to Markov Decision Processes. For these automata we consider two notions of equivalence: expectation equivalence and distribution equivalence. The former requires that two automata have the same expected reward on each input word, while the latter requires that each input word induce the same distribution on rewards in each automaton. For both notions we give algorithms for deciding equivalence by reduction to equivalence of Q-weighted automata. Finally we show that the equivalence problem for Q-weighted visibly pushdown automata is logspace equivalent to the polynomial identity testing problem.

cs.FL↗

arXiv2011

On Searching for Small Kochen-Specker Vector Systems (extended version)

Kochen-Specker (KS) vector systems are sets of vectors in R^3 with the property that it is impossible to assign 0s and 1s to the vectors in such a way that no two orthogonal vectors are assigned 0 and no three mutually orthogonal vectors are assigned 1. The existence of such sets forms the basis of the Kochen-Specker and Free Will theorems. Currently, the smallest known KS vector system contains 31 vectors. In this paper, we establish a lower bound of 18 on the size of any KS vector system. This requires us to consider a mix of graph-theoretic and topological embedding problems, which we investigate both from theoretical and practical angles. We propose several algorithms to tackle these problems and report on extensive experiments. At the time of writing, a large gap remains between the best lower and upper bounds for the minimum size of KS vector systems.

quant-ph↗

arXiv2007

On the decidability and complexity of Metric Temporal Logic over finite words

Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL--which includes invariance and time-bounded response properties--is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature.

cs.LO↗