-
Model Checking Markov Chains as Distribution Transformers
Authors:
Rajab Aghamov,
Christel Baier,
Toghrul Karimov,
Joris Nieuwveld,
Joël Ouaknine,
Jakob Piribauer,
Mihir Vahanwala
Abstract:
The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50\% chance of rain? The conventional perspective is ill-equipped to decide s…
▽ More
The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50\% chance of rain? The conventional perspective is ill-equipped to decide such problems regarding the evolution of the initial distribution. The alternate perspective we consider views Markov chains as distribution transformers: the focus is on the sequence of distributions on states at each step, where the evolution is driven by the underlying stochastic transition matrix. More precisely, given an initial distribution vector $μ$, a stochastic update transition matrix $M$, we ask whether the ensuing sequence of distributions $(μ, Mμ, M^2μ, \dots)$ satisfies a given temporal property. This is a special case of the model-checking problem for linear dynamical systems, which is not known to be decidable in full generality. The goal of this article is to delineate the classes of instances for which this problem can be solved, under the assumption that the dynamics is governed by stochastic matrices.
△ Less
Submitted 21 June, 2024;
originally announced June 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.
-
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.
-
On the Counting Complexity of the Skolem Problem
Authors:
Gorav **dal,
Joël Ouaknine
Abstract:
The Skolem Problem asks, given an integer linear recurrence sequence (LRS), to determine whether the sequence contains a zero term or not. Its decidability is a longstanding open problem in theoretical computer science and automata theory. Currently, decidability is only known for LRS of order at most 4. On the other hand, the sole known complexity result is NP-hardness, due to Blondel and Portier…
▽ More
The Skolem Problem asks, given an integer linear recurrence sequence (LRS), to determine whether the sequence contains a zero term or not. Its decidability is a longstanding open problem in theoretical computer science and automata theory. Currently, decidability is only known for LRS of order at most 4. On the other hand, the sole known complexity result is NP-hardness, due to Blondel and Portier.
A fundamental result in this area is the celebrated Skolem-Mahler-Lech theorem, which asserts that the zero set of any LRS is the union of a finite set and finitely many arithmetic progressions. This paper focuses on a computational perspective of the Skolem-Mahler-Lech theorem: we show that the problem of counting the zeros of a given LRS is #P-hard, and in fact #P-complete for the instances generated in our reduction.
△ Less
Submitted 29 February, 2024;
originally announced March 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.
-
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.
-
Reachability in Injective Piecewise Affine Maps
Authors:
Faraz Ghahremani,
Edon Kelmendi,
Joël Ouaknine
Abstract:
One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is decidable. We also study various related problems, in each case either establishing decidability, or showing that they are closely connected to Diophantine proper…
▽ More
One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is decidable. We also study various related problems, in each case either establishing decidability, or showing that they are closely connected to Diophantine properties of certain transcendental numbers, analogous to the positivity problem for linear recurrence sequences. Lastly, we consider topological properties of orbits of one-dimensional piecewise affine maps, not necessarily with two intervals, and negatively answer a question of Bournez, Kurganskyy, and Potapov, about the set of orbits in expanding maps.
△ Less
Submitted 17 March, 2023; v1 submitted 23 January, 2023;
originally announced January 2023.
-
Model Checking Linear Dynamical Systems under Floating-point Rounding
Authors:
Engel Lefaucheux,
Joël Ouaknine,
David Purser,
Mohammadamin Sharifi
Abstract:
We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point representation after each step (i.e., stored as a fixed-precision mantissa and an exponent). The approach more faithfully models realistic implementations of linear loops, compared to the exact arbitrary-precision setting…
▽ More
We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point representation after each step (i.e., stored as a fixed-precision mantissa and an exponent). The approach more faithfully models realistic implementations of linear loops, compared to the exact arbitrary-precision setting often employed in the study of linear dynamical systems.
Our results are twofold: We show that for non-negative matrices there is a special structure to the sequence of vectors generated by the system: the mantissas are periodic and the exponents grow linearly. We leverage this to show decidability of $ω$-regular temporal model checking against semialgebraic predicates. This contrasts with the unrounded setting, where even the non-negative case encompasses the long-standing open Skolem and Positivity problems.
On the other hand, when negative numbers are allowed in the matrix, we show that the reachability problem is undecidable by encoding a two-counter machine. Again, this is in contrast with the unrounded setting where point-to-point reachability is known to be decidable in polynomial time.
△ Less
Submitted 27 January, 2023; v1 submitted 8 November, 2022;
originally announced November 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.
-
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 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.
-
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.
-
Reachability in Dynamical Systems with Rounding
Authors:
Christel Baier,
Florian Funke,
Simon Jantsch,
Toghrul Karimov,
Engel Lefaucheux,
Joël Ouaknine,
Amaury Pouly,
David Purser,
Markus A. Whiteland
Abstract:
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose ever…
▽ More
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose every entry is a multiple of $g$, we are interested in the behaviour of the orbit $\mathcal{O}={<}[x], [M[x]],[M[M[x]]],\dots{>}$, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability---whether a given target $y \in\mathbb{Q}^{d}$ belongs to $\mathcal{O}$---is PSPACE-complete for hyperbolic systems (when no eigenvalue of $M$ has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.
△ Less
Submitted 28 September, 2020;
originally announced September 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.
-
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.
-
Sequential Relational Decomposition
Authors:
Dror Fried,
Axel Legay,
Joël Ouaknine,
Moshe Y. Vardi
Abstract:
The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in which a task is decomposed into two sequential sub-tasks, with the first sub-task to be executed befo…
▽ More
The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in which a task is decomposed into two sequential sub-tasks, with the first sub-task to be executed before the second sub-task is executed. These tasks are specified by means of input/output relations. We define and study decomposition problems, which is to decide whether a given specification can be sequentially decomposed. Our main result is that decomposition itself is a difficult computational problem. More specifically, we study decomposition problems in three settings: where the input task is specified explicitly, by means of Boolean circuits, and by means of automatic relations. We show that in the first setting decomposition is NP-complete, in the second setting it is NEXPTIME-complete, and in the third setting there is evidence to suggest that it is undecidable. Our results indicate that the intuitive idea of decomposition as a system-design approach requires further investigation. In particular, we show that adding a human to the loop by asking for a decomposition hint lowers the complexity of decomposition problems considerably.
△ Less
Submitted 2 March, 2022; v1 submitted 4 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.
-
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.
-
Convex Language Semantics for Nondeterministic Probabilistic Automata
Authors:
Gerco van Heerdt,
Justin Hsu,
Joël Ouaknine,
Alexandra Silva
Abstract:
We explore language semantics for automata combining probabilistic and nondeterministic behavior. 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 undecidab…
▽ More
We explore language semantics for automata combining probabilistic and nondeterministic behavior. 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.
△ Less
Submitted 29 May, 2018;
originally announced May 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.
-
O-Minimal Invariants for Discrete-Time Dynamical Systems
Authors:
Shaull Almagor,
Dmitry Chistikov,
Joël Ouaknine,
James Worrell
Abstract:
Termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachabili…
▽ More
Termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of \emph{o-minimal invariants}, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory.
△ Less
Submitted 11 May, 2020; v1 submitted 26 February, 2018;
originally announced February 2018.
-
On the Decidability of Reachability in Linear Time-Invariant Systems
Authors:
Nathanaël Fijalkow,
Joël Ouaknine,
Amaury Pouly,
João Sousa-Pinto,
James Worrell
Abstract:
We consider the decidability of state-to-state reachability in linear time-invariant control systems over discrete time. We analyse this problem with respect to the allowable control sets, which in general are assumed to be defined by boolean combinations of linear inequalities. Decidability of the version of the reachability problem in which control sets are affine subspaces of $\mathbb{R}^n$ is…
▽ More
We consider the decidability of state-to-state reachability in linear time-invariant control systems over discrete time. We analyse this problem with respect to the allowable control sets, which in general are assumed to be defined by boolean combinations of linear inequalities. Decidability of the version of the reachability problem in which control sets are affine subspaces of $\mathbb{R}^n$ is a fundamental result in control theory. Our first result is that reachability is undecidable if the set of controls is a finite union of affine subspaces. We also consider versions of the reachability problem in which (i)~the set of controls consists of a single affine subspace together with the origin and (ii)~the set of controls is a convex polytope. In these two cases we respectively show that the reachability problem is as hard as Skolem's Problem and the Positivity Problem for linear recurrence sequences (whose decidability has been open for several decades). Our main contribution is to show decidability of a version of the reachability problem in which control sets are convex polytopes, under certain spectral assumptions on the transition matrix.
△ Less
Submitted 18 February, 2019; v1 submitted 19 February, 2018;
originally announced February 2018.
-
Polynomial Invariants for Affine Programs
Authors:
Ehud Hrushovski,
Joël Ouaknine,
Amaury Pouly,
James Worrell
Abstract:
We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of t…
▽ More
We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.
△ Less
Submitted 2 May, 2018; v1 submitted 6 February, 2018;
originally announced February 2018.
-
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
Authors:
Nathanaël Fijalkow,
Pierre Ohlmann,
Joël Ouaknine,
Amaury Pouly,
James Worrell
Abstract:
The \emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $\mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s.
In this paper, we are concerned with the problem of synthesising suitable \emph{invariants}…
▽ More
The \emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $\mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s.
In this paper, we are concerned with the problem of synthesising suitable \emph{invariants} $\mathcal{P} \subseteq \mathbb{R}^d$, \emph{i.e.}, sets that are stable under $A$ and contain $x$ and not $y$, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size.
It is worth noting that the existence of \emph{semilinear} invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
△ Less
Submitted 9 January, 2017;
originally announced January 2017.
-
The Polytope-Collision Problem
Authors:
Shaull Almagor,
Joël Ouaknine,
James Worrell
Abstract:
The Orbit Problem consists of determining, given a matrix $A\in \mathbb{R}^{d\times d}$ and vectors $x,y\in \mathbb{R}^d$, whether there exists $n\in \mathbb{N}$ such that $A^n=y$. This problem was shown to be decidable in a seminal work of Kannan and Lipton in the 1980s. Subsequently, Kannan and Lipton noted that the Orbit Problem becomes considerably harder when the target $y$ is replaced with a…
▽ More
The Orbit Problem consists of determining, given a matrix $A\in \mathbb{R}^{d\times d}$ and vectors $x,y\in \mathbb{R}^d$, whether there exists $n\in \mathbb{N}$ such that $A^n=y$. This problem was shown to be decidable in a seminal work of Kannan and Lipton in the 1980s. Subsequently, Kannan and Lipton noted that the Orbit Problem becomes considerably harder when the target $y$ is replaced with a subspace of $\mathbb{R}^d$. Recently, it was shown that the problem is decidable for vector-space targets of dimension at most three, followed by another development showing that the problem is in PSPACE for polytope targets of dimension at most three. In this work, we take a dual look at the problem, and consider the case where the initial vector $x$ is replaced with a polytope $P_1$, and the target is a polytope $P_2$. Then, the question is whether there exists $n\in \mathbb{N}$ such that $A^n P_1\cap P_2\neq \emptyset$. We show that the problem can be decided in PSPACE for dimension at most three. As in previous works, decidability in the case of higher dimensions is left open, as the problem is known to be hard for long-standing number-theoretic open problems.
Our proof begins by formulating the problem as the satisfiability of a parametrized family of sentences in the existential first-order theory of real-closed fields. Then, after removing quantifiers, we are left with instances of simultaneous positivity of sums of exponentials. Using techniques from transcendental number theory, and separation bounds on algebraic numbers, we are able to solve such instances in PSPACE.
△ Less
Submitted 4 November, 2016;
originally announced November 2016.
-
Model Checking Flat Freeze LTL on One-Counter Automata
Authors:
Antonia Lechner,
Richard Mayr,
Joël Ouaknine,
Amaury Pouly,
James Worrell
Abstract:
Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in general and PSPACE-complete for the special case of deterministic one-counter automata. Several years ago, Demri and Sangnier investigated the model checking probl…
▽ More
Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in general and PSPACE-complete for the special case of deterministic one-counter automata. Several years ago, Demri and Sangnier investigated the model checking problem for the flat fragment of Freeze LTL on several classes of counter automata and posed the decidability of model checking flat Freeze LTL on one-counter automata as an open problem. In this paper we resolve this problem positively, utilising a known reduction to a reachability problem on one-counter automata with parameterised equality and disequality tests. Our main technical contribution is to show decidability of the latter problem by translation to Presburger arithmetic.
△ Less
Submitted 6 December, 2018; v1 submitted 8 June, 2016;
originally announced June 2016.
-
Solvability of Matrix-Exponential Equations
Authors:
Joël Ouaknine,
Amaury Pouly,
João Sousa-Pinto,
James Worrell
Abstract:
We consider a continuous analogue of Babai et al.'s and Cai et al.'s problem of solving multiplicative matrix equations. Given $k+1$ square matrices $A_{1}, \ldots, A_{k}, C$, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals $t_{1}, \ldots, t_{k}$ such that \begin{align*} \prod \limits_{i=1}^{k} \exp(A_{i} t_{i})…
▽ More
We consider a continuous analogue of Babai et al.'s and Cai et al.'s problem of solving multiplicative matrix equations. Given $k+1$ square matrices $A_{1}, \ldots, A_{k}, C$, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals $t_{1}, \ldots, t_{k}$ such that \begin{align*} \prod \limits_{i=1}^{k} \exp(A_{i} t_{i}) = C . \end{align*} We show that this problem is undecidable in general, but decidable under the assumption that the matrices $A_{1}, \ldots, A_{k}$ commute. Our results have applications to reachability problems for linear hybrid automata. Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert's Tenth Problem.
△ Less
Submitted 15 May, 2016; v1 submitted 19 January, 2016;
originally announced January 2016.
-
On the Polytope Escape Problem for Continuous Linear Dynamical Systems
Authors:
Joël Ouaknine,
João Sousa-Pinto,
James Worrell
Abstract:
The Polyhedral Escape Problem for continuous linear dynamical systems consists of deciding, given an affine function $f: \mathbb{R}^{d} \rightarrow \mathbb{R}^{d}$ and a convex polyhedron $\mathcal{P} \subseteq \mathbb{R}^{d}$, whether, for some initial point $\boldsymbol{x}_{0}$ in $\mathcal{P}$, the trajectory of the unique solution to the differential equation…
▽ More
The Polyhedral Escape Problem for continuous linear dynamical systems consists of deciding, given an affine function $f: \mathbb{R}^{d} \rightarrow \mathbb{R}^{d}$ and a convex polyhedron $\mathcal{P} \subseteq \mathbb{R}^{d}$, whether, for some initial point $\boldsymbol{x}_{0}$ in $\mathcal{P}$, the trajectory of the unique solution to the differential equation $\dot{\boldsymbol{x}}(t)=f(\boldsymbol{x}(t))$, $\boldsymbol{x}(0)=\boldsymbol{x}_{0}$, is entirely contained in $\mathcal{P}$. We show that this problem is decidable, by reducing it in polynomial time to the decision version of linear programming with real algebraic coefficients, thus placing it in $\exists \mathbb{R}$, which lies between NP and PSPACE. Our algorithm makes use of spectral techniques and relies among others on tools from Diophantine approximation.
△ Less
Submitted 10 February, 2017; v1 submitted 11 July, 2015;
originally announced July 2015.
-
On the Skolem Problem for Continuous Linear Dynamical Systems
Authors:
Ventsislav Chonev,
Joel Ouaknine,
James Worrell
Abstract:
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-p…
▽ More
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.
△ Less
Submitted 10 May, 2016; v1 submitted 1 June, 2015;
originally announced June 2015.
-
Proving the Herman-Protocol Conjecture
Authors:
Maria Bruna,
Radu Grigore,
Stefan Kiefer,
Joël Ouaknine,
James Worrell
Abstract:
Herman's self-stabilisation algorithm, introduced 25 years ago, is a well-studied synchronous randomised protocol for enabling a ring of $N$ processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilisation is the central outstanding open problem about this protocol. It is known that there is a…
▽ More
Herman's self-stabilisation algorithm, introduced 25 years ago, is a well-studied synchronous randomised protocol for enabling a ring of $N$ processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilisation is the central outstanding open problem about this protocol. It is known that there is a constant $h$ such that any initial configuration has expected stabilisation time at most $h N^2$. Ten years ago, McIver and Morgan established a lower bound of $4/27 \approx 0.148$ for $h$, achieved with three equally-spaced tokens, and conjectured this to be the optimal value of $h$. A series of papers over the last decade gradually reduced the upper bound on $h$, with the present record (achieved in 2014) standing at approximately $0.156$. In this paper, we prove McIver and Morgan's conjecture and establish that $h = 4/27$ is indeed optimal.
△ Less
Submitted 27 April, 2016; v1 submitted 5 April, 2015;
originally announced April 2015.
-
The Cyclic-Routing UAV Problem is PSPACE-Complete
Authors:
Hsi-Ming Ho,
Joel Ouaknine
Abstract:
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…
▽ More
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.
△ Less
Submitted 22 January, 2015; v1 submitted 9 November, 2014;
originally announced November 2014.
-
On Termination of Integer Linear Loops
Authors:
Joël Ouaknine,
João Sousa Pinto,
James Worrell
Abstract:
A fundamental problem in program verification concerns the termination of simple linear loops of the form x := u ; while Bx >= b do {x := Ax + a} 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 terminat…
▽ More
A fundamental problem in program verification concerns the termination of simple linear loops of the form x := u ; while Bx >= b do {x := Ax + a} 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 (2004) and Braverman (2006).
△ Less
Submitted 13 October, 2014; v1 submitted 7 July, 2014;
originally announced July 2014.
-
The Polyhedron-Hitting Problem
Authors:
Ventsislav Chonev,
Joël Ouaknine,
James Worrell
Abstract:
We consider polyhedral versions of Kannan and Lipton's Orbit Problem (STOC '80 and JACM '86)---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 Q^m. In the context of program verification, very similar reachability questions were also considered and left open by Lee and Yannakakis in…
▽ More
We consider polyhedral versions of Kannan and Lipton's Orbit Problem (STOC '80 and JACM '86)---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 Q^m. In the context of program verification, very similar reachability questions were also considered and left open by Lee and Yannakakis in (STOC '92). 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.
△ Less
Submitted 12 October, 2014; v1 submitted 7 July, 2014;
originally announced July 2014.
-
On the Complexity of Temporal-Logic Path Checking
Authors:
Daniel Bundala,
Joël Ouaknine
Abstract:
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 finite word. For LTL, the complexity of this task was recently shown to be in NC. In this paper, we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an NCC algorithm for UTL, the unary fragment of LTL. At the time of writing, MTL…
▽ More
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 finite word. For LTL, the complexity of this task was recently shown to be in NC. In this paper, we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an NCC algorithm for UTL, the unary fragment of LTL. At the time of writing, MTL is the most expressive logic with an NC path-checking algorithm, and UTL is the most expressive fragment of LTL with a more efficient path-checking algorithm than for full LTL (subject to standard complexity-theoretic assumptions). We then establish a connection between LTL path checking and planar circuits, which we exploit to show that any further progress in determining the precise complexity of LTL path checking would immediately entail more efficient evaluation algorithms than are known for a certain class of planar circuits. The connection further implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem.
△ Less
Submitted 28 April, 2014; v1 submitted 29 December, 2013;
originally announced December 2013.
-
Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences
Authors:
Joel Ouaknine,
James Worrell
Abstract:
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 decid…
▽ More
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).
△ Less
Submitted 5 April, 2017; v1 submitted 7 September, 2013;
originally announced September 2013.
-
On the Positivity Problem for Simple Linear Recurrence Sequences
Authors:
Joel Ouaknine,
James Worrell
Abstract:
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.
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.
△ Less
Submitted 28 April, 2014; v1 submitted 6 September, 2013;
originally announced September 2013.
-
Positivity Problems for Low-Order Linear Recurrence Sequences
Authors:
Joel Ouaknine,
James Worrell
Abstract:
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…
▽ More
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.
△ Less
Submitted 9 October, 2013; v1 submitted 10 July, 2013;
originally announced July 2013.
