11institutetext: Max Planck Institute for Software Systems, Saarland
Informatics Campus, Germany 22institutetext: Department of Computer Science,
Oxford University, UK

# What’s Decidable about Discrete
Linear Dynamical Systems?

Toghrul Karimov 11 Edon Kelmendi 11 Joël Ouaknine Also affiliated with Keble
College, Oxford as emmy.network Fellow, and supported by DFG grant 389792660
as part of TRR 248 (see https://perspicuous-computing.science).11 James
Worrell 22

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

###### Keywords:

Discrete Linear Dynamical Systems Model Checking Invariant Generation Orbit
Problem Linear Recurrence Sequences Skolem Problem

##  1 Introduction

Dynamical systems are a fundamental modelling paradigm in many branches of
science, and have been the subject of extensive research for many decades. A
_(rational) discrete linear dynamical system (LDS)_ in ambient space
$\mathbb{R}^{d}$ is given by a square $d\times d$ matrix $M$ with rational
entries, together with a starting point $x\in\mathbb{Q}^{d}$.111All of the
results we present in this paper carry over to the more general setting of
_real-algebraic_ LDS, whose entries are allowed to be real algebraic numbers.
Nevertheless, we stick here to rationals for simplicity of exposition. The
orbit of $(M,x)$ is the infinite trajectory $\mathcal{O}(M,x):=\langle
x,Mx,M^{2}x,\dots\rangle$. An example of a four-dimensional LDS is given in
Figure 1. Our main focus in the present paper is on delineating the class of
assertions on the orbits of LDS that can be algorithmically decided.

$M\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\begin{pmatrix}3&2&0&-5\\\ 0&1&0&3\\\ 0&4&3&13\\\
3&11&6&24\end{pmatrix}\quad\quad\quad
x\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}\begin{pmatrix}1\\\
-1\\\ 2\\\ 0\end{pmatrix}$ Figure 1: A four-dimensional discrete linear
dynamical system.

One of the most natural and fundamental computational questions concerning
linear dynamical systems is the _Point-to-Point Reachability Problem_ , also
known as the _Kannan-Lipton Orbit Problem_ : given a $d$-dimensional LDS
$(M,x)$ together with a point target $y\in\mathbb{Q}^{d}$, does the orbit of
the LDS ever hit the target? The decidability of this question was settled
affirmatively in the 1980s in the seminal work of Kannan and Lipton [35, 36].
In fact, Kannan and Lipton showed that this problem is solvable in polynomial
time, answering an earlier open problem of Harrison from the 1960s on
reachability for linear sequential machines [33].

Interestingly, one of Kannan and Lipton’s motivations was to propose a line of
attack to the well-known _Skolem Problem_ , which had itself been famously
open since the 1930s. The Skolem Problem remains unsolved to this day,
although substantial advances have recently been made—more on this shortly.
Phrased in the language of linear dynamical systems, the Skolem Problem asks
whether it is decidable, given $(M,x)$ as above, together with a
$(d-1)$-dimensional subspace $H$ of $\mathbb{R}^{d}$, to determine if the
orbit of $(M,x)$ ever hits $H$. Kannan and Lipton suggested that, in ambient
space $\mathbb{R}^{d}$ of arbitrary dimension, the problem of hitting a low-
dimensional subspace might be decidable. Indeed, this was eventually
substantiated by Chonev _et al._ for linear subspaces of dimension at most $3$
[21, 23].

Subsequent research focussed on the decidability of hitting targets of
increasing complexity, such as half-spaces [32, 39, 47, 46, 48], polytopes
[52, 22, 5], and semialgebraic sets [6, 7]. It is also worth noting that
discrete linear dynamical systems can equivalently be viewed as linear (or
affine) simple, branching-free while loops, where reachability corresponds to
loop termination. There is a voluminous literature on the topic, albeit
largely focussing on heuristics and semi-algorithms (via spectral methods or
the synthesis of ranking functions, in particular), rather than exact
decidability results. Relevant papers include [54, 19, 11, 12, 18, 20, 24, 50,
51, 34, 13, 10]. Several of these approaches have moreover been implemented in
software verification tools, such as Microsoft’s Terminator [26, 27].

In recent years, motivated in part by verification questions for stochastic
systems and linear loops, researchers have begun investigating more
sophisticated decision problems than mere reachability: for example, the paper
[1] studies approximate LTL model checking of Markov chains (which themselves
can be viewed as particular kinds of linear dynamical systems), whereas [38]
focusses on LTL model checking of low-dimensional linear dynamical systems
with semialgebraic predicates.222Semialgebraic predicates are Boolean
combinations of polynomial equalities and inequalities. In [4], the authors
solve the semialgebraic model-checking problem for diagonalisable linear
dynamical systems in arbitrary dimension against prefix-independent
MSO333Monadic Second-Order Logic (MSO) is a highly expressive specification
formalism that subsumes the vast majority of temporal logics employed in the
field of automated verification, such as Linear Temporal Logic (LTL). “Prefix
independence” is a quality of properties that are _asymptotic_ in nature—we
provide a precise definition shortly. properties, whereas [37] investigates
semialgebraic MSO model checking of linear dynamical systems in which the
dimensions of predicates are constrained. To illustrate this last approach,
recall the dynamical system $(M,x)$ from Figure 1, and consider the following
three semialgebraic predicates:

$\displaystyle
P_{1}(x_{1},x_{2},x_{3},x_{4})\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}x_{1}+x_{2}+x_{3}-x_{4}=0\land(x_{1}^{3}=x_{2}^{2}\lor x_{4}\geq
3x_{1}^{2}+x_{2})$ $\displaystyle
P_{2}(x_{1},x_{2},x_{3},x_{4})\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}x_{1}+x_{2}+2x_{3}-2x_{4}=0\land x_{1}^{3}+x_{3}^{2}+x_{3}>x_{4}$
$\displaystyle
P_{3}(x_{1},x_{2},x_{3},x_{4})\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}x_{1}^{4}-x_{2}^{2}=3\land 2x_{3}^{2}=x_{4}\land
x_{1}^{2}-2x_{2}^{3}=4x_{3}\,.$

Recall that the ambient space is $\mathbb{R}^{4}$. We identify the above
predicates with the corresponding subsets of $\mathbb{R}^{4}$, and wish to
express assertions about the orbit of $(M,x)$ as it traces a trajectory
through $\mathbb{R}^{4}$. For example (in LTL notation),

$\mathbf{G}(P_{1}\Rightarrow\mathbf{F}\lnot
P_{2})\land\mathbf{F}(P_{3}\lor\lnot P_{1})$

asserts that whenever the orbit visits $P_{1}$, then it must eventually
subsequently visit the complement of $P_{2}$, and moreover that the orbit will
eventually either visit $P_{3}$ or the complement of $P_{1}$. The reader will
probably agree that whether or not the above assertion holds for our LDS
$(M,x)$ is not immediately obvious to determine (even, arguably, in
principle). Nevertheless, this example falls within the scope of [37], as the
semialgebraic predicates $P_{1}$, $P_{2}$, and $P_{3}$ are each either
contained in some three-dimensional subspace (this is the case for $P_{1}$ and
$P_{2}$), or have intrinsic dimension at most $1$ (this is the case of
$P_{3}$, which is ‘string-like’, or a curve, as a subset of $\mathbb{R}^{4}$).
Naturally, we shall return to these notions in due course, and articulate the
relevant results in full details.

A recent and closely related line of inquiry concerns the study of algebraic
model checking of linear dynamical systems [42]. The setting is similar to the
above, the only difference being that the allowable predicates are the
_constructible_ ones, i.e., built from _algebraic_ sets444Algebraic sets
correspond to positive Boolean combinations of polynomial equalities. using
arbitrary Boolean operations (including complementation). The paper [42]
introduces in addition the key notion of _Skolem oracle_ , which we discuss
next.

###  1.1 Skolem Oracles

There is an intimate connection between linear dynamical systems and linear
recurrence sequences. An _(integer) linear recurrence sequence (LRS)_
$\boldsymbol{u}=\langle u_{n}\rangle_{n=0}^{\infty}$ is an infinite sequence
of integers satisfying

$u_{n+d}=c_{1}u_{n+d-1}+\cdots+c_{d-1}u_{n+1}+c_{d}u_{n}$ (1)

for all $n\in\mathbb{N}$, where the coefficients $c_{1},\ldots,c_{d}$ are
integers and $c_{d}\neq 0$. We say that the above recurrence has _order_ $d$.
We moreover say that an LRS is _simple_ if the characteristic polynomial555The
characteristic polynomial associated with recurrence (1) is
$X^{d}-c_{1}X^{d-1}-\ldots-c_{d}$. of its minimal-order recurrence has no
repeated roots. The sequence of Fibonacci numbers $\langle
f_{n}\rangle_{n=0}^{\infty}=\langle 0,1,1,2,3,5,\ldots\rangle$, which obeys
the recurrence $f_{n+2}=f_{n+1}+f_{n}$, is perhaps the most emblematic LRS,
and also happens to be simple.

The celebrated theorem of Skolem, Mahler, and Lech (see [31]) describes the
structure of the set $\\{n\in\mathbb{N}:u_{n}=0\\}$ of zero terms of an LRS as
follows:

###### Theorem 1.1

Given a linear recurrence sequence $\boldsymbol{u}=\langle
u_{n}\rangle_{n=0}^{\infty}$, its set of zero terms is a semilinear set, i.e.,
it consists of a union of finitely many full arithmetic progressions,666A full
arithmetic progression is a set of non-negative integers of the form
$\\{a+bm:m\in\mathbb{N}\\}$, with $a,b\in\mathbb{N}$ and $a<b$. together with
a finite set.

As shown by Berstel and Mignotte [14], in the above one can effectively
extract all of the arithmetic progressions; we refer herein to the
corresponding procedure as the ‘Berstel-Mignotte algorithm’. Nevertheless, how
to compute the leftover finite set of zeros remains open, and is easily seen
to be equivalent to the _Skolem Problem_ : given an LRS $\boldsymbol{u}$, does
$\boldsymbol{u}$ contain a zero term?

The paper [42] therefore introduces the notion of a _Skolem oracle_ : given an
LRS $\boldsymbol{u}=\langle u_{n}\rangle_{n=0}^{\infty}$, such an oracle
returns the finite set of indices of zeros of $\boldsymbol{u}$ that do not
already belong to some infinite arithmetic progression of zeros. Likewise, a
_Simple-Skolem oracle_ is a Skolem oracle restricted to simple LRS.

As mentioned earlier, the decidability of the Skolem Problem is a longstanding
open question [31, 49], with a positive answer for LRS of order at most $4$
known since the mid-1980s [53, 55]. Very recently, two major conditional
advances on the Skolem Problem have been made, achieving decidability subject
to certain classical number-theoretic conjectures: in [40], Lipton _et al._
established decidability for LRS of order $5$ assuming the _Skolem Conjecture_
(also known as the _Exponential Local-Global Principle_); and in [15], Bilu
_et al._ showed decidability for simple LRS of arbitrary order, subject to
both the Skolem Conjecture and the _$p$ -adic Schanuel Conjecture_ (we refer
the reader to [15] for the precise definitions and details). It is interesting
to note that in both cases, the procedures in question rely on the conjectures
_only_ for termination; correctness is unconditional. In fact, these
procedures are _certifying algorithms_ (in the sense of [45]) in that, upon
termination, they produce an independent certificate (or witness) that their
output is correct. Such a certificate can be checked algorithmically by a
third party with no reliance on any unproven conjectures. The authors of [15]
have implemented their algorithm within the skolem tool, available
online.777https://skolem.mpi-sws.org/ .

In view of the above, Simple-Skolem oracles _can_ be implemented with
unconditional correctness, and guaranteed termination subject to the Skolem
and $p$-adic Schanuel conjectures. Whether full Skolem oracles can be devised
is the subject of active research (see, e.g., [41, 43]); at the time of
writing, to the best of our knowledge, no putative procedure is even
conjectured in the general (non-simple) case.

###  1.2 Paper Outline

Questions of reachability and model checking for linear dynamical systems
constitute one of the central foci of this paper. In Section 2, we cover the
state of the art and beyond, both unconditionally and relative to Skolem
oracles. We paint what is essentially a complete picture of the landscape, in
each situation establishing either decidability (possibly conditional on
Skolem oracles), or hardness with respect to longstanding open problems. An
important theme in the classical theory of dynamical systems concerns the
study of _asymptotic_ properties (e.g., stability, convergence, or divergence
of orbits), and we therefore consider both MSO along with its _prefix-
independent_ fragment piMSO. Section 3 then focusses on questions of
robustness through the notion of pseudo-orbit. In Section 4, we discuss the
algorithmic synthesis of inductive invariants for linear dynamical systems,
and Section 5 examines the situation in which orbits originate from an initial
set rather than a single point. Finally, Section 6 concludes with a brief
summary and a glimpse of several research directions.

##  2 Model Checking

Throughout this section, we assume familiarity with the rudiments of Monadic
Second-Order Logic (MSO); an excellent reference is the text [16].

Let us work in fixed ambient space $\mathbb{R}^{d}$, and consider a
$d$-dimensional LDS $(M,x)$ (i.e., $M\in\mathbb{Q}^{d\times d}$ and
$x\in\mathbb{Q}^{d}$). Recall that the orbit $\mathcal{O}=\mathcal{O}(M,x)$ of
our LDS is the infinite sequence $\langle x,Mx,M^{2}x,\ldots\rangle$ in
$\mathbb{Q}^{d}$. Let us write $\mathcal{O}[n]$ for the $n$th term of the
orbit.

Given an MSO formula $\varphi$ over the collection of semialgebraic predicates
$\mathcal{P}=\\{P_{1},\ldots,P_{m}\\}$, where each
$P_{i}\subseteq\mathbb{R}^{d}$, the model-checking problem consists in
determining whether the orbit (more precisely, the characteristic word
$\alpha\in\left(2^{\mathcal{P}}\right)^{\omega}$ of the orbit
$\mathcal{O}(M,x)$ with respect to $\mathcal{P}$, where $P_{i}\in\alpha[n]$
iff $\mathcal{O}[n]\in P_{i}$) satisfies $\varphi$. Reachability problems for
LDS constitute special cases of the model-checking problem, and already the
questions of determining whether a given orbit reaches a hyperplane (Skolem
Problem) or a halfspace (the _Positivity Problem_ [46]) are longstanding open
problems in number theory, couched in the language of linear dynamical
systems. Recent research has, however, succeeded in uncovering several
important decidable subclasses of the model-checking problem and in
demarcating the boundary between what is decidable and what is hard with
respect to longstanding open mathematical problems.

In order to present the main results, we require some further definitions to
specify the classes of predicates that are allowed within MSO formulas. Let us
write $\mathcal{S}\subseteq 2^{\mathbb{R}^{d}}$ and $\mathcal{C}\subseteq
2^{\mathbb{R}^{d}}$ to denote respectively the collections of all
semialgebraic subsets of $\mathbb{R}^{d}$ and of all constructible subsets of
$\mathbb{R}^{d}$.888Recall that $\mathcal{C}$ is the smallest set containing
all algebraic subsets of $\mathbb{R}^{d}$, and which is closed under finite
union, finite intersection, and complement. (The terminology of
“constructible” originates from algebraic geometry.) We also define the
collection $\mathcal{T}\subseteq 2^{\mathbb{R}^{d}}$ of _tame_ sets as
follows: $\mathcal{T}$ comprises all semialgebraic subsets of $\mathbb{R}^{d}$
that are either contained in a three-dimensional subspace of $\mathbb{R}^{d}$,
or that have intrinsic dimension at most one.999The intrinsic dimension of a
semialgebraic set is formally defined via cell decomposition; intuitively,
one-dimensional semialgebraic sets can be viewed as ‘strings’ or ‘curves’,
whereas zero-dimensional semialgebraic sets are finite collections of
singleton points. Moreover, $\mathcal{T}$ is defined to be the smallest such
set which is in addition closed under finite union, finite intersection, and
complement. Finally, we define the set $\mathcal{T}\oplus\mathcal{C}$ to be
the smallest superset of $\mathcal{T}\cup\mathcal{C}$ that is closed under
finite union, finite intersection, and complement.

Note that all of $\mathcal{S}$, $\mathcal{C}$, $\mathcal{T}$, and
$\mathcal{T}\oplus\mathcal{C}$ are closed under all Boolean operations; this
is in keeping with their intended use as collections of predicates for MSO
formulas, bearing in mind that MSO itself possesses all Boolean operators.

The motivation for considering the collection $\mathcal{T}$ of tame predicates
has origins in the results of [21, 38, 6, 9]. A common theme is that for tame
predicates, the proofs that establish how to decide reachability also provide
one with a means of representing, in a finitary manner, all the time steps at
which the orbit of a given LDS is in a particular predicate set $T$. The
authors of [37] show how to combine these representations (one for each
predicate) to obtain structural information about the characteristic word
$\alpha$ that is sufficient for determining whether a deterministic automaton
$\mathcal{A}$ accepts $\alpha$, leading to the following.

###### Theorem 2.1

Let $(M,x)$ be an LDS,
$\mathcal{P}=\\{T_{1},\ldots,T_{m}\\}\subseteq\mathcal{T}$ be a collection of
tame predicates and $\varphi$ be an MSO formula over $\mathcal{P}$. It is
decidable whether $(M,x)\vDash\varphi$ (i.e., whether the characteristic word
$\alpha$ of the orbit $\mathcal{O}(M,x)$ with respect to $\mathcal{P}$
satisfies $\varphi$).

Let us note in passing that Theorem 2.1 subsumes the decidability of the
Kannan-Lipton Point-to-Point Reachability Problem, since points are singleton
sets and the latter are evidently tame.

It is also worth pointing out, absent other restrictions, that this
delineation of the decidable fragment of the model-checking problem is tight
as trying to expand the definition of tame predicates runs into open problems
already for formulas that describe mere reachability properties. In
particular, the Skolem Problem in dimension 5 is open and can be encoded (i)
as a reachability problem with a four-dimensional LDS and a three-dimensional
affine subspace [21] (that is, in general, not contained in a three-
dimensional linear subspace) and (ii) as a reachability problem with a target
of intrinsic dimension two [9].

To sidestep these obstacles, in [4] the authors restrict $\varphi$ to formulas
that define _prefix-independent_ properties. A property is prefix-independent
if the infinite words that satisfy it are closed under the operations of
insertion and deletion of finitely many letters.101010It is interesting to
note that whether an MSO formula $\varphi$ is prefix-independent or not is
decidable. To see this, for $A=(Q,q_{0},\Sigma,\Delta,F)$ a deterministic
Müller automaton, define $A(q)$, for $q\in Q$, to be the same as $A$, except
that the initial state of $A(q)$ is $q$ (rather than $q_{0}$). We say that a
deterministic Müller automaton $A$ (as above) is _prefix-independent_ if, for
all $q\in Q$ that are reachable from $q_{0}$, $A(q)$ recognises the same
language as $A$. Write $L(A)$ to denote the language recognised by $A$. It is
now straightforward to show that $A$ is prefix-independent iff $L(A)$ is
prefix-independent. Since any MSO formula is encodable as a deterministic
Müller automaton, and equality of $\omega$-regular languages is decidable, the
desired decidability result follows. Such properties capture behaviours that
are intrinsically asymptotic in nature (for example: “does the orbit enter $P$
infinitely often?”); note that the property of reachability is _not_ prefix-
independent. The main theorem of [4] in this direction concerns
_diagonalisable_ linear dynamical systems:111111An LDS $(M,x)$ is
_diagonalisable_ if the matrix $M$ is diagonalisable (over $\mathbb{C}$). In a
measure-theoretic sense, most LDS are diagonalisable.

###### Theorem 2.2

Let $(M,x)$ be a diagonalisable LDS and $\varphi$ be a prefix-independent MSO
formula over a collection of semialgebraic predicates
$S_{1},\ldots,S_{m}\in\mathcal{S}$. It is decidable whether
$(M,x)\vDash\varphi$.

Note in the above that the semialgebraic predicates are entirely unrestricted
(in particular, not required to be tame). However, the restrictions to prefix-
independent formulas and to diagonalisable systems both again turn out to be
essential. Since the Skolem Problem is open for diagonalisable systems (in
dimensions $d\geq 5$), the (non-prefix-independent) model-checking problem for
diagonalisable LDS is Skolem-hard already for four-dimensional systems and
affine subspace targets, as discussed earlier. On the other hand, if we allow
non-diagonalisable systems, then the problem of determining whether the orbit
of an LDS is eventually trapped in a given half-space $H$ (known as the
_Ultimate Positivity Problem_ , corresponding to the prefix-independent
formula $\varphi=\mathbf{F}\,\mathbf{G}\,H$) is hard with respect to certain
longstanding open problems in Diophantine approximation [46].

This last observation however suggests that it might be possible to
orchestrate a trade-off between the type of LDS under consideration and the
class of allowable specification predicates. Indeed, it turns out that one can
lift the restriction to diagonalisable LDS if one agrees to restrict the class
of predicates:

###### Theorem 2.3

Let $(M,x)$ be an LDS and $\varphi$ be a prefix-independent MSO formula over a
collection of predicates $P_{1},\ldots,P_{m}\in\mathcal{T}\oplus\mathcal{C}$.
It is decidable whether $(M,x)\vDash\varphi$.

Theorem 2.3 goes beyond both Theorem 2.1 (in that constructible predicates are
allowed into the mix) as well as [42, Thm. 7.3] (in that tame predicates are
allowed).

Let us provide a brief proof sketch of Theorem 2.3. Let $(M,x)$ and $\varphi$
be as above. Observe first (as a straightforward exercise) that any
$P\in\mathcal{T}\oplus\mathcal{C}$ can be written in conjunctive normal form,
i.e., as an expression of the form
$P=\bigcap_{i=1}^{a}\bigcup_{j=1}^{b}B_{i,j}$, where each $B_{i,j}$ is either
a tame predicate or a constructible predicate. Without loss of generality, one
may therefore assume that each predicate appearing in $\varphi$ is either tame
or constructible.

We now invoke [42, Prop. 5] to conclude that, for each constructible predicate
$B_{\ell}$ appearing in $\varphi$, the Boolean-valued word $\alpha_{\ell}$
tracking the passage of the orbit of $(M,x)$ through $B_{\ell}$ is ultimately
periodic. Moreover, thanks to the Berstel-Mignotte algorithm, the attendant
arithmetic progressions can all be effectively elicited. For each such
$\alpha_{\ell}$, one can therefore construct a (fully) periodic word
$\alpha^{\prime}_{\ell}$ which differs from $\alpha_{\ell}$ in at most
finitely many places. In other words, for all sufficiently large $n$,
$M^{n}x\in B_{\ell}$ iff $\alpha^{\prime}[n]=\mathit{true}$. Being periodic,
$\alpha^{\prime}_{\ell}$ can in turn be described by an MSO subformula
$\psi_{\ell}$. Let us therefore replace within $\varphi$ every occurrence of a
constructible predicate $B_{\ell}$ by the subformula $\psi_{\ell}$, obtaining
in this process a new MSO formula $\varphi^{\prime}$ that comprises
exclusively tame predicates. As $\varphi$ is prefix-independent, it is
immediate that $(M,x)\vDash\varphi$ iff $(M,x)\vDash\varphi^{\prime}$. But the
latter is of course decidable thanks to Theorem 2.1, concluding the proof
sketch of Theorem 2.3.

Once again, Theorem 2.3 is tight: in Appendix 0.A, we show that the ability to
solve the model-checking problem for prefix-independent MSO specifications
making use of semialgebraic predicates in ambient space $\mathbb{R}^{4}$ would
necessarily entail major breakthroughs in Diophantine approximation.

Let us now turn to the question of the extent to which the above results can
be enhanced through the use of Skolem oracles. The key result is as follows,
in effect enabling us to drop the restriction of prefix-independence from
Theorem 2.3:

###### Theorem 2.4

Let $(M,x)$ be an LDS and $\varphi$ be an MSO formula over a collection of
predicates $P_{1},\ldots,P_{m}\in\mathcal{T}\oplus\mathcal{C}$. It is
decidable whether $(M,x)\vDash\varphi$, subject to the existence of a Skolem
oracle.

The same result also holds for diagonalisable LDS, assuming the existence of a
Simple-Skolem oracle.

The proof of Theorem 2.4 is similar to that of Theorem 2.3; we provide a brief
sketch below.

Let $(M,x)$ and $\varphi$ be as above, and assume, thanks to the
representation of ($\mathcal{T}\oplus\mathcal{C}$)-predicates in conjunctive
normal form, that every predicate occurring in $\varphi$ is either tame of
constructible. Thanks to [42, Cor. 6], for each constructible predicate
$B_{\ell}$ appearing in $\varphi$, the Boolean-valued word $\alpha_{\ell}$
tracking the passage of the orbit of $(M,x)$ through $B_{\ell}$ is effectively
ultimately periodic (this requires the use of a Skolem oracle, or a Simple-
Skolem oracle if $M$ is diagonalisable). In other words, we have a finitary
exact representation of $\alpha_{\ell}$, and can therefore describe it via an
MSO subformula $\psi_{\ell}$.

We can now replace within $\varphi$ every occurrence of a constructible
predicate $B_{\ell}$ by its corresponding subformula $\psi_{\ell}$, obtaining
in this process an equivalent MSO formula $\varphi^{\prime}$ that comprises
exclusively tame predicates. The desired result then immediately follows from
Theorem 2.1, concluding the proof sketch of Theorem 2.4.

As noted earlier, Simple-Skolem oracles can be implemented into provably
correct certifying procedures which terminate subject to classical number-
theoretic conjectures [15]. Let us therefore separately record an important
corollary:

###### Corollary 1

Let $(M,x)$ be a diagonalisable LDS and $\varphi$ be an MSO formula over a
collection of predicates $P_{1},\ldots,P_{m}\in\mathcal{T}\oplus\mathcal{C}$.
It is decidable whether $(M,x)\vDash\varphi$, assuming the Skolem Conjecture
and the p-adic Schanuel Conjecture. Moreover, correctness of the attendant
procedure is unconditional, and independent correctness certificates can be
produced upon termination.

Let us point out that Theorem 2.4 is, once again, tight. For arbitrary LDS, a
similar argument as that put forth in Appendix 0.A applies, since it is not
known (or even believed) that Skolem oracles are of any use in tackling
Ultimate Positivity problems. For diagonalisable LDS, we can invoke the
order-10 Simple Positivity Problem, which remains open to this day (see [46]);
it can be modelled straightforwardly as a half-space reachability problem in
ambient space $\mathbb{R}^{10}$ (or even $\mathbb{R}^{9}$, by considering an
affine half-space). In fact, critical unsolved cases of order-10 Positivity
can even be formulated as semialgebraic reachability problems in ambient space
$\mathbb{R}^{4}$; we omit the details in the interests of space and simplicity
of exposition.

We summarise the main results of this section in Figure 2 below.

Diagonalisable LDS:
---
|  unconditional |  Simple-Skolem oracle
piMSO |  $\mathcal{S}$ (Thm. 2.2) |  $\mathcal{S}$ (Thm. 2.2)
MSO |  $\mathcal{T}$ (Thm. 2.1) |  $\mathcal{T}\oplus\mathcal{C}$ (Thm. 2.4)

Arbitrary LDS:
---
|  unconditional |  Skolem oracle
piMSO |  $\mathcal{T}\oplus\mathcal{C}$ (Thm. 2.3) |  $\mathcal{T}\oplus\mathcal{C}$ (Thm. 2.3 or Thm. 2.4)
MSO |  $\mathcal{T}$ (Thm. 2.1) |  $\mathcal{T}\oplus\mathcal{C}$ (Thm. 2.4)

Figure 2: A summary of the decidable model-checking fragments for both
diagonalisable and arbitrary linear dynamical systems. The prefix-independent
fragment of MSO is denoted piMSO. $\mathcal{S}$ is the collection of
semialgebraic predicates, $\mathcal{T}$ is the collection of tame predicates
(Boolean closure of semialgebraic sets that either are contained in a three-
dimensional subspace, or have intrinsic dimension at most one), $\mathcal{C}$
is the collection of constructible predicates (Boolean closure of algebraic
sets), and $\mathcal{T}\oplus\mathcal{C}$ is the Boolean closure of
$\mathcal{T}\cup\mathcal{C}$. The right-hand columns in both tables assume
access to Skolem or Simple-Skolem oracles.

Taken together, Theorems 2.1–2.4, along with Corollary 1, not only subsume—to
the best of our knowledge—all existing results regarding model-checking and
reachability problems for discrete linear dynamical systems, but moreover
paint an essentially complete picture of what is (even in principle) feasible,
barring major breakthroughs in longstanding open problems. It is noteworthy
that, in this characterisation, there appears to be very little difference
between being able to decide mere reachability for a given class of
predicates, and being able to decide the whole of MSO over the same class of
predicates.

##  3 Pseudo-Reachability and Robustness

In this section we discuss decision problems about pseudo-orbits that are
related to robustness of computation. Given an LDS $(M,x)$, recall that the
orbit of $x$ under $M$ is the sequence $\langle x,Mx,M^{2}x,\dots\rangle$. We
say that the sequence $\langle x_{n}:n\in\mathbb{N}\rangle$ is an
_$\varepsilon$ -pseudo-orbit_ of $x$ under $M$ if $x_{0}=x$ and
$x_{n+1}=Mx_{n}+d_{n}$ for some perturbation $d_{n}$ with
$||d_{n}||<\epsilon$. The _pseudo-orbit_ of $x$ under $M$ is then defined as
the set of points that are reachable from $x$ via an $\varepsilon$-pseudo-
orbit for every $\epsilon>0$. This notion of an ($\varepsilon$-)pseudo-orbit,
introduced and studied by Anosov [8], Bowen [17] and Conley [25], is an
important conceptual tool in dynamical systems. From the computational
perspective, an $\varepsilon$-pseudo-orbit can be viewed as a trajectory after
a rounding error of magnitude at most $\epsilon$ is applied at each step.

Given these definitions, we can consider the reachability and model-checking
problems for pseudo-orbits. A natural analogy to the Kannan-Lipton Orbit
Problem is the _Pseudo-Orbit Problem_ , which is to determine whether a target
point $y$ belongs to the pseudo-orbit of $x$ under $M$. In [28] the authors
show that, just like the Orbit Problem, the Pseudo-Orbit Problem is decidable
in polynomial time. Generalising from points to sets, let us say that a target
set $T$ is pseudo-reachable if for every $\epsilon>0$ there exists an
$\varepsilon$-pseudo-orbit of $x$ under $M$ that reaches $T$. We can then
define the _Pseudo-Skolem Problem_ and the _Pseudo-Positivity Problem_ to be
the pseudo-reachability problems with a hyperplane and a halfspace as target
sets, respectively. Surprisingly, [28] shows that both of these problems are
in fact decidable! Moreover, [29] establishes decidability of pseudo-
reachability with arbitrary semialgebraic targets for diagonalisable linear
dynamical systems.

Inspired by the above results, one might consider the model-checking problem
for pseudo-orbits, namely the problem of determining, given $(M,x)$ and a
formula $\varphi$, whether for every $\varepsilon>0$, there exists an
$\varepsilon$-pseudo-orbit that satisfies $\varphi$. After all, as discussed
in the preceding section, for genuine orbits the fragments of the reachability
problem and the full MSO model-checking problem that are known to be decidable
(i.e., the restrictions on the class of predicates and the property $\varphi$
that make the problems decidable) are essentially the same. This optimism is,
however, quickly shattered by the following observation. Let $H$ be a closed
halfspace and $\varphi$ be the property $\mathbf{G}\,H$ (“the trajectory
always remains inside $H$”). Then the pseudo-orbits satisfy $\varphi$ (in the
sense defined above) if and only the (genuine) orbit satisfies $\varphi$. The
problem of determining whether the orbit $\mathcal{O}(M,x)$ always remains in
$H$, is however, equivalent to the problem of determining whether the orbit
ever hits an open halfspace, which itself is the Positivity Problem (a
longstanding open question).

##  4 Invariant Generation

In the absence of fully general algorithms to decide whether the orbit of a
given LDS reaches targets of arbitrary forms, much effort has been expended on
sound—but possibly incomplete—techniques, and particularly on constructing
certificates of (non-)reachability. This splits into two broad lines of
attack: ranking functions and invariants. The former are certificates of
reachability, demonstrating that progress is being made towards the target.
Inductive invariants are, on the other hand, certificates of non-reachability,
establishing that the orbit will not reach the target by enclosing the former
within a set that is itself disjoint from the latter. We focus in this section
on the algorithmic generation of invariants.

More precisely, a set $\mathcal{I}\subseteq\mathbb{R}^{d}$ is said to be an
_inductive invariant_ of $(M,x)$ if it contains $x$ ($x\in\mathcal{I}$), and
is stable under $M$, that is:

$\displaystyle M\mathcal{I}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{My:y\in\mathcal{I}\\}\subseteq\mathcal{I}\,.$

Clearly there are some trivial invariants, such as $\mathbb{R}^{d}$ and the
orbit $\mathcal{O}(M,x)$ itself. They are not particularly useful in the sense
that the ambient space $\mathbb{R}^{d}$ is never disjoint from whatever target
might be under consideration, whereas for various classes of targets (such as
hyperplanes or half-spaces; or more generally arbitrary semialgebraic sets) we
do not in general know how to decide whether $\mathcal{O}(M,x)$ is disjoint
from the target. Hence one does not seek _any_ invariant, but rather an
invariant that can be algorithmically established to be disjoint from the
target.

We therefore seek a sufficiently large, or expressive, class of invariants
$\mathcal{F}$ which moreover exhibits favourable algorithmic properties. A
natural family to consider is the collection of all semialgebraic sets. We now
have:

######  Theorem 4.1 ([3])

Given an LDS $(M,x)$ in ambient space $\mathbb{R}^{d}$, together with a
semialgebraic target $T\subseteq\mathbb{R}^{d}$, it is decidable whether there
exists a semialgebraic invariant of $(M,x)$ that is disjoint from $T$.

Furthermore, the algorithm explicitly constructs the invariant when it exists,
in the form of a Boolean combination of polynomial inequalities.

Theorem 4.1 holds for an even larger class $\mathcal{F}$, namely that of
o-minimal sets. We give an informal definition. Recall the contents of
Tarski’s quantifier-elimination theorem, to the effect that semialgebraic
subsets of $\mathbb{R}^{d}$ are closed under projections. Moreover,
semialgebraic subsets of $\mathbb{R}$ are quite simple: they are finite unions
of intervals. Other families of sets that enjoy these two properties exist,
notably those definable in the first-order theory of the real numbers
augmented with a symbol for the exponential function, an important result due
to Wilkie [56]. Structures of $\mathbb{R}^{d}$ that are induced by such
logical theories are called _o-minimal_ , and an _o-minimal set_ is a set that
belongs to such a structure [30]. These include semialgebraic sets, as well as
sets definable in the first-order theory of the reals with restricted analytic
functions.

In [2], it is shown that it is decidable whether there exists an o-minimal
invariant (for a given LDS $(M,x)$) that is disjoint from a semialgebraic
target $T$; and moreover, when such an invariant exists, it is always possible
to exhibit one that is in fact semialgebraic [3]. Once again, these results
are effective, and the invariants can always be explicitly produced.

Varying the class of invariants and the class of targets gives rise to a
number of natural questions that—for the most part—remain unexplored. Let us
however mention a further desirable property enjoyed both by the class of
o-minimal sets and that of semialgebraic sets: in either case, they admit
_minimal families_ of invariants, a notion which we now explain. Let
$\mathcal{F}$ be a class of sets—either the class of o-minimal sets or that of
semialgebraic sets. It is easy to verify that, in general, $\mathcal{F}$ does
not possess minimal invariants. Nevertheless, [2, 3] show how to produce a
sequence of $(M,x)$-invariants $\langle\mathcal{C}_{k}:k\in\mathbb{N}\rangle$,
all belonging to $\mathcal{F}$, and such that
$\mathcal{C}_{k+1}\subset\mathcal{C}_{k}$. It can moreover be shown that,
given any $(M,x)$-invariant $\mathcal{I}\in\mathcal{F}$, it is always the case
that $\mathcal{I}$ contains one of the $\mathcal{C}_{k}$, and _ipso facto_
also all $\mathcal{C}_{j}$ for $j\geq k$.

##  5 Semialgebraic Initial Sets

Up until now we have exclusively considered problems concerning the orbit
$\mathcal{O}(M,x)$ of a _single_ initial point $x$. It is natural to ask
whether the algorithmic problems which we have discussed remain solvable if
one instead considers an entire _set_ of initial points
$S\subseteq\mathbb{R}^{d}$. Unfortunately the answer is negative. We sketch
below the proof of the undecidability of a natural model-checking problem.

###### Theorem 5.1

The following problem is undecidable. Given a natural number $k\in\mathbb{N}$,
a semialgebraic set $S\subseteq\mathbb{R}^{d}$, a $d\times d$ rational matrix
$M$, and a hyperplane $H$ in $\mathbb{R}^{d}$ (having rational normal vector),
determine whether there exists $x\in S$ such that the orbit generated by
$(M,x)$ hits $H$ at least $k$ times.

In symbols, whether there is some $x\in S$ such that

$\displaystyle\lvert\mathcal{O}(M,x)\cap H\rvert\geq k$

is undecidable.

It is worth noting that all the problems that we have discussed so far
(including the Skolem and Positivity Problems) are not known to be
undecidable, and are in fact widely conjectured to be decidable. It is
therefore perhaps somewhat surprising that this natural generalisation of our
setting immediately leads to undecidability.

The proof of Theorem 5.1 proceeds by reduction from a variant of Hilbert’s
tenth problem. Recall that Hilbert’s tenth problem asks whether a given
polynomial $P\in\mathbb{Z}[Y_{1},Y_{2},\ldots,Y_{d-1}]$ with integer
coefficients and $d-1$ variables has a root with all unknowns taking integer
values. This problem is undecidable, as shown by Davis, Putnam, Robinson, and
Matiyasevich [44].

The variant that we will reduce from asks whether the polynomial has roots
with the unknowns being distinct natural numbers. It is straightforward to
show that this variant is also undecidable.

Let $d\in\mathbb{N}$, $d>1$, and $P\in\mathbb{Z}[Y_{1},Y_{2},\ldots,Y_{d-1}]$
be an arbitrary polynomial. We define the subset $S\subseteq\mathbb{R}^{d}$
via a formula of the first-order theory of the reals:

$\displaystyle
S(x_{1},x_{2},\ldots,x_{d})\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\exists y_{1},y_{2},\ldots
y_{d-1}\begin{cases}0&=P(y_{1},y_{2},\ldots,y_{d-1}),\\\
x_{1}&=(1-y_{1})(1-y_{2})\cdots(1-y_{d-1}),\\\
x_{2}&=(2-y_{1})(2-y_{2})\cdots(2-y_{d-1}),\\\ &\vdots\\\
x_{d}&=(d-y_{1})(d-y_{2})\cdots(d-y_{d-1}).\end{cases}$

A point $x:=(x_{1},\ldots,x_{d})\in\mathbb{R}^{d}$ is in the set $S$ if and
only if one can find real numbers $y_{1},\ldots,y_{d-1}$ for which the above
equations hold. The idea behind this definition comes from the fact that, for
$x,y_{1},\ldots,y_{d-1}$ as above, one can construct a $d\times d$ matrix $M$
with rational entries such that

$\displaystyle\left(M^{n}x\right)_{1}=(n-y_{1})(n-y_{2})\cdots(n-y_{d-1})\,,$

for all $n\in\mathbb{N}$, where $(\cdot)_{1}$ refers to the first entry of the
vector. Admitting the existence of such a matrix, let $H$ be the hyperplane
having normal vector $(1,0,\ldots,0)$ and going through the origin. Then
clearly $\mathcal{O}(M,x)$ enters $H$ at least $d-1$ times if and only if the
reals $y_{1},\ldots,y_{d-1}$ are distinct natural numbers, because only then
is the first entry of $M^{n}x$—the polynomial
$(n-y_{1})\cdots(n-y_{d-1})$—equal to zero.

The existence of the matrix $M$ rests on the fact that the expression
$u_{n}=(n-y_{1})\cdots(n-y_{d-1})$ (for fixed $y_{1},\ldots,y_{d-1}$) can be
obtained as a linear recurrence sequence of order $d$, and in turn such a
linear recurrence sequence can be represented as the sequence of fixed-
position entries of increasing powers of a fixed $d\times d$ matrix $M$. In
the standard construction of this matricial representation, one must in
addition set $x_{1}=u_{1}$, $x_{2}=u_{2}$, …, $x_{d}=u_{d}$, which is achieved
through the definition of our initial semialgebraic set $S$.

It is worth noting that Theorem 5.1 holds even if $k$ is fixed, due to the
fact that Hilbert’s tenth problem remains undecidable for a fixed number of
variables. Furthermore, if $k$ is fixed to be $1$, then the problem becomes
decidable in low dimensions, however even in the case where the ambient space
has dimension $2$ and $k=2$, the problem does not seem to be trivially
decidable.

##  6 Research Directions and Open Problems

We have presented an overview of the state of the art regarding decidability
and solvability of a range of algorithmic problems for discrete linear
dynamical systems, focussing on reachability, model-checking, and invariant-
generation questions. In the case of model checking in particular, we have
painted an essentially complete picture of what is achievable, both
unconditionally as well as relative to Skolem oracles. We pointed out that
extending the existing results further runs up against formidable mathematical
obstacles (longstanding open problems in number theory); the work presented
here therefore appears to lie at the very frontier of what is attainable,
barring major breakthroughs in mathematics.

A central open question is whether Skolem oracles can actually be devised and
implemented. As remarked earlier, a certifying algorithm for the Simple-Skolem
Problem has recently been proposed, with termination relying on classical (and
widely believed) number-theoretic conjectures. Whether similar algorithms can
be obtained for the general Skolem Problem is the subject of active research.

An even more difficult question is whether oracles for the Positivity Problem
(or Simple-Positivity Problem) can be devised. This would enable one to
circumvent the mathematical obstacles mentioned earlier, and allow one to
substantially extend the scope of semialgebraic model checking for linear
dynamical systems. For the time being, this goal appears to be well out of
reach.

In the present paper we have entirely confined ourselves to matters of
decidability, largely on account of space limitations, but also because the
complexity-theoretic picture is not nearly as clear-cut as its decidability
counterpart. Providing a comprehensive account of the complexity landscape for
linear dynamical systems would be an interesting and promising research
direction.

##  Appendix 0.A Prefix-Independent Model Checking for LDS

The goal of this appendix is to exhibit boundaries on the extent to which
Theorem 2.3 can be improved. More precisely, we show that the ability to solve
the model-checking problem for arbitrary LDS against prefix-independent MSO
specifications making use of semialgebraic predicates in ambient space
$\mathbb{R}^{4}$ would necessarily entail major breakthroughs in Diophantine
approximation.

We build upon the framework developed in [47, Sec. 5]. To this end, consider
the class of order-$6$ rational LRS of the form

$u_{n}=-n+\frac{1}{2}(n-ri)\lambda^{n}+\frac{1}{2}(n+ri)\overline{\lambda}^{n}=r\operatorname{Im}(\lambda^{n})-n(1-\operatorname{Re}(\lambda^{n}))\,,$

where $\lambda\in\mathbb{Q}(i)$ and $|\lambda|=1$, and $r\in\mathbb{Q}$. Let
us write $\mathcal{L}$ to denote this class of LRS.

It is shown in [47] that solving the _Ultimate Positivity Problem_ for LRS in
$\mathcal{L}$, i.e., providing an algorithm which, given an LRS $\langle
u_{n}\rangle_{n=0}^{\infty}\in\mathcal{L}$, determines whether there exists
some integer $N$ such that, for all $n\geq N$, $u_{n}\geq 0$, would
necessarily entail major breakthroughs in the field of Diophantine
approximation. The purpose of the present section is to reduce the Ultimate
Positivity Problem for LRS in $\mathcal{L}$ to the prefix-independent
semialgebraic MSO model-checking problem for $4$-dimensional LDS.

Given $\lambda$ and $r$ as above, let

$M=\begin{bmatrix}\operatorname{Re}(\lambda)&-\operatorname{Im}(\lambda)&1&0\\\
\operatorname{Im}(\lambda)&\operatorname{Re}(\lambda)&0&1\\\
0&0&\operatorname{Re}(\lambda)&-\operatorname{Im}(\lambda)\\\
0&0&\operatorname{Im}(\lambda)&\operatorname{Re}(\lambda)\\\
\end{bmatrix}\text{ and }x=\begin{bmatrix}1\\\ 1\\\ 1\\\ 1\end{bmatrix}.$

Observe that $M$ has rational entries. We have that

$M^{n}x=\begin{bmatrix}\operatorname{Re}(\lambda^{n})-\operatorname{Im}(\lambda^{n})+n\operatorname{Re}(\lambda^{n-1})-n\operatorname{Im}(\lambda^{n-1})\\\
\operatorname{Im}(\lambda^{n})+\operatorname{Re}(\lambda^{n})+n\operatorname{Im}(\lambda^{n-1})+n\operatorname{Re}(\lambda^{n-1})\\\
\operatorname{Re}(\lambda^{n})-\operatorname{Im}(\lambda^{n})\\\
\operatorname{Im}(\lambda^{n})+\operatorname{Re}(\lambda^{n})\end{bmatrix}.$

As a semialgebraic target consider the set $S=\\{x:p(x)>0\\}$, where

$p(x_{1},x_{2},x_{3},x_{4})=\frac{r}{2}(x_{4}-x_{3})-\frac{x_{1}-x_{3}}{\operatorname{Re}(\lambda^{-1})x_{3}-\operatorname{Im}(\lambda^{-1})x_{4}}\left(1-\frac{x_{3}+x_{4}}{2}\right).$

We now have that
$p(M^{n}x)=r\operatorname{Im}(\lambda^{n})-n(1-\operatorname{Re}(\lambda^{n}))$,
and that $\langle u_{n}\rangle_{n=0}^{\infty}$ is ultimately positive if and
only if the orbit of $x$ under $M$ eventually gets trapped in $S$. This can be
expressed by the prefix-independent LTL formula
$\varphi=\mathbf{F}\,\mathbf{G}\,S$.

## References

  * [1] Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S.: Approximate verification of the symbolic dynamics of Markov chains. J. ACM 62(1), 2:1–2:34 (2015)
  * [2] Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for linear loops. In: 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018. LIPIcs, vol. 107, pp. 114:1–114:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
  * [3] Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for discrete-time dynamical systems. ACM Trans. Comput. Log. 23(2), 9:1–9:20 (2022)
  * [4] Almagor, S., Karimov, T., Kelmendi, E., Ouaknine, J., Worrell, J.: Deciding $\omega$-regular properties on linear recurrence sequences. Proc. ACM Program. Lang. 5(POPL), 1–24 (2021)
  * [5] Almagor, S., Ouaknine, J., Worrell, J.: The Polytope-Collision Problem. In: 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017. LIPIcs, vol. 80, pp. 24:1–24:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
  * [6] Almagor, S., Ouaknine, J., Worrell, J.: The Semialgebraic Orbit Problem. In: 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019. LIPIcs, vol. 126, pp. 6:1–6:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
  * [7] Almagor, S., Ouaknine, J., Worrell, J.: First-order orbit queries. Theory Comput. Syst. 65(4), 638–661 (2021)
  * [8] Anosov, D.V.: Geodesic flows on closed Riemannian manifolds of negative curvature. Proc. Steklov Inst. Math. 90 (1967)
  * [9] Baier, C., Funke, F., Jantsch, S., Karimov, T., Lefaucheux, E., Luca, F., Ouaknine, J., Purser, D., Whiteland, M.A., Worrell, J.: The Orbit Problem for parametric linear dynamical systems (2021)
  * [10] Ben-Amram, A.M., Doménech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Static Analysis - 26th International Symposium, SAS 2019. Lecture Notes in Computer Science, vol. 11822, pp. 459–480. Springer (2019)
  * [11] Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13. pp. 51–62. ACM (2013)
  * [12] Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 26:1–26:55 (2014)
  * [13] Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Computer Aided Verification - 29th International Conference, CAV 2017. Lecture Notes in Computer Science, vol. 10427, pp. 601–620. Springer (2017)
  * [14] Berstel, J., Mignotte, M.: Deux propriétés décidables des suites récurrentes linéaires. Bull. Soc. math. France 104, 175–184 (1976)
  * [15] Bilu, Y., Luca, F., Nieuwveld, J., Ouaknine, J., Purser, D., Worrell, J.: Skolem meets Schanuel. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria. LIPIcs, vol. 241, pp. 62:1–62:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  * [16] Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic, Springer (1997)
  * [17] Bowen, R.: Equilibrium States and the Ergodic Theory of Anosov Diffeomorphisms, Lecture Notes in Mathematics, vol. 470. Springer-Verlag (1975)
  * [18] Bradley, A.R., Manna, Z., Sipma, H.B.: Termination analysis of integer linear loops. In: CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005. Lecture Notes in Computer Science, vol. 3653, pp. 488–502. Springer (2005)
  * [19] Braverman, M.: Termination of integer linear programs. In: Computer Aided Verification, 18th International Conference, CAV 2006. Lecture Notes in Computer Science, vol. 4144, pp. 372–385. Springer (2006)
  * [20] Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. Int. J. Softw. Tools Technol. Transf. 17(1), 47–57 (2015)
  * [21] Chonev, V., Ouaknine, J., Worrell, J.: The Orbit Problem in higher dimensions. In: Symposium on Theory of Computing Conference, STOC’13. pp. 941–950. ACM (2013)
  * [22] Chonev, V., Ouaknine, J., Worrell, J.: The Polyhedron-Hitting Problem. In: Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015. pp. 940–956. SIAM (2015)
  * [23] Chonev, V., Ouaknine, J., Worrell, J.: On the complexity of the Orbit Problem. J. ACM 63(3), 23:1–23:18 (2016)
  * [24] Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001. Lecture Notes in Computer Science, vol. 2031, pp. 67–81. Springer (2001)
  * [25] Conley, C.C.: Isolated invariant sets and the Morse index, CBMS Regional Conference Series in Mathematics, vol. 25. American Mathematical Society (1978)
  * [26] Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation. pp. 415–426. ACM (2006)
  * [27] Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Computer Aided Verification, 18th International Conference, CAV 2006. Lecture Notes in Computer Science, vol. 4144, pp. 415–418. Springer (2006)
  * [28] D’Costa, J., Karimov, T., Majumdar, R., Ouaknine, J., Salamati, M., Soudjani, S., Worrell, J.: The Pseudo-Skolem Problem is decidable. In: Bonchi, F., Puglisi, S.J. (eds.) 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 202, pp. 34:1–34:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021)
  * [29] D’Costa, J., Karimov, T., Majumdar, R., Ouaknine, J., Salamati, M., Worrell, J.: The pseudo-reachability problem for diagonalisable linear dynamical systems. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria. LIPIcs, vol. 241, pp. 40:1–40:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  * [30] Van den Dries, L.: Tame topology and o-minimal structures, vol. 248. Cambridge university press (1998)
  * [31] Everest, G., van der Poorten, A.J., Shparlinski, I.E., Ward, T.: Recurrence Sequences, Mathematical surveys and monographs, vol. 104. American Mathematical Society (2003)
  * [32] Halava, V., Harju, T., Hirvensalo, M.: Positivity of second order linear recurrent sequences. Discret. Appl. Math. 154(3), 447–451 (2006)
  * [33] Harrison, M.A.: Lectures on Linear Sequential Machines. Academic Press, New York (1969)
  * [34] Hosseini, M., Ouaknine, J., Worrell, J.: Termination of linear loops over the integers. In: 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019. LIPIcs, vol. 132, pp. 118:1–118:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
  * [35] Kannan, R., Lipton, R.J.: The Orbit Problem is decidable. In: Proceedings of the 12th Annual ACM Symposium on Theory of Computing 1980. pp. 252–261. ACM (1980)
  * [36] Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the Orbit Problem. J. ACM 33(4), 808–821 (1986)
  * [37] Karimov, T., Lefaucheux, E., Ouaknine, J., Purser, D., Varonka, A., Whiteland, M.A., Worrell, J.: What’s decidable about linear loops? Proc. ACM Program. Lang. 6(POPL), 1–25 (2022)
  * [38] Karimov, T., Ouaknine, J., Worrell, J.: On LTL model checking for low-dimensional discrete linear dynamical systems. In: 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020. LIPIcs, vol. 170, pp. 54:1–54:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  * [39] Laohakosol, V., Tangsupphathawat, P.: Positivity of third order linear recurrence sequences. Discret. Appl. Math. 157(15), 3239–3248 (2009)
  * [40] Lipton, R.J., Luca, F., Nieuwveld, J., Ouaknine, J., Worrell, D.P.J.: On the Skolem Problem and the Skolem Conjecture. In: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022, Haifa, Israel, August 2 \- August 5, 2022. ACM (2022)
  * [41] Luca, F., Ouaknine, J., Worrell, J.: Universal Skolem sets. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1–6. IEEE (2021)
  * [42] Luca, F., Ouaknine, J., Worrell, J.: Algebraic model checking for discrete linear dynamical systems. In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13465, pp. 3–15. Springer (2022)
  * [43] Luca, F., Ouaknine, J., Worrell, J.: A universal Skolem set of positive lower density. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria. LIPIcs, vol. 241, pp. 73:1–73:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  * [44] Matiyasevich, Y.V.: Hilbert’s tenth problem. MIT press (1993)
  * [45] McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119–161 (2011)
  * [46] Ouaknine, J., Worrell, J.: On the positivity problem for simple linear recurrence sequences. In: Automata, Languages, and Programming. pp. 318–329. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
  * [47] Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014. pp. 366–379. SIAM (2014)
  * [48] Ouaknine, J., Worrell, J.: Ultimate Positivity is decidable for simple linear recurrence sequences. In: Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014. Lecture Notes in Computer Science, vol. 8573, pp. 330–341. Springer (2014)
  * [49] Ouaknine, J., Worrell, J.: On linear recurrence sequences and loop termination. ACM SIGLOG News 2(2), 4–13 (2015)
  * [50] Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI. Lecture Notes in Computer Science, vol. 2937, pp. 239–251. Springer (2004)
  * [51] Podelski, A., Rybalchenko, A.: Transition invariants. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004). pp. 32–41. IEEE Computer Society (2004)
  * [52] Tarasov, S.P., Vyalyi, M.N.: Orbits of linear maps and regular languages. In: Computer Science - Theory and Applications - 6th International Computer Science Symposium in Russia, CSR 2011. Lecture Notes in Computer Science, vol. 6651, pp. 305–316. Springer (2011)
  * [53] Tijdeman, R., Mignotte, M., Shorey, T.N.: The distance between terms of an algebraic recurrence sequence. Journal für die reine und angewandte Mathematik 349, 63–76 (1984)
  * [54] Tiwari, A.: Termination of linear programs. In: Computer Aided Verification, 16th International Conference, CAV 2004. Lecture Notes in Computer Science, vol. 3114, pp. 70–82. Springer (2004)
  * [55] Vereshchagin, N.: The problem of appearance of a zero in a linear recurrence sequence. Mat. Zametki 38(2), 609–615 (1985)
  * [56] Wilkie, A.J.: Model completeness results for expansions of the ordered field of real numbers by restricted pfaffian functions and the exponential function. Journal of the American Mathematical Society 9(4), 1051–1094 (1996)