# Model Checking Linear Dynamical Systems under Floating-point Rounding

Engel Lefaucheux, Joël Ouaknine, David Purser, Mohammadamin Sharifi

► To cite this version:

Engel Lefaucheux, Joël Ouaknine, David Purser, Mohammadamin Sharifi. Model Checking Linear Dynamical Systems under Floating-point Rounding. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Apr 2023, Paris, France. pp.47-65, 10.1007/978-3-031-30823-9_3. hal-03843471

HAL Id: hal-03843471

https://inria.hal.science/hal-03843471

Submitted on 8 Nov 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Model Checking Linear Dynamical Systems
under Floating-point Rounding

Engel Lefaucheux¹[0000-0003-0875-300X], Joël Ouaknine²[0000-0003-0031-9356],
David Purser³[0000-0003-0394-1634], and Mohammadamin Sharifi⁴

¹ University of Lorraine, CNRS, Inria, LORIA, Nancy, France

² Max Planck Institute for Software Systems, Saarland Informatics Campus,
Germany

³ University of Warsaw, Poland

⁴ Sharif University of Technology

**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 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 $\omega$-regular temporal model checking against semi-algebraic 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 to the unrounded setting where point-to-point reachability is known to be decidable in polynomial time.

# 1 Introduction

Loops are a fundamental staple of any programming language, and the study of loops plays a pivotal role in many subfields of computer science, including automated verification, abstract interpretation, program analysis, semantics, etc. The focus of the present paper is on the algorithmic analysis of simple (i.e., non-nested) linear (or affine) while loops, such as the following:

$x = 3, y = 4, z = 2$

while $x+3y+z > 4$:

$x = 3x + 2z$

$y = 3x + y$

$z = y + z$
We are interested in analysing how the loop evolves. A simple reachability query is to decide whether the loop variables ever satisfy a (Boolean combination of) polynomial inequalities, for example modelling a loop guard. More generally, model checking can express significantly more complex temporal properties, such as those expressible in linear temporal logic or monadic second order logic.

Modelling the evolution of such a loop may require unbounded memory. That is, the number of bits required to represent the numbers $x$, $y$, and $z$ may grow larger and larger. However, most computer systems do not represent rational numbers to arbitrary precision, but rather use *floating-point rounding*, in which a number $y$ is stored using two components: the mantissa $m \in \mathbb{Q}$ and the exponent $\alpha \in \mathbb{Z}$, such that $y = m \cdot 10^{\alpha}$.<fnref n="5" />

Typically floating-point numbers are specified using either 32 or 64 bits, with some of these reserved for the mantissa and some for the exponent, thus bounding both the mantissa and the exponent. **We do not do this**, and only place a bound on the number of bits representing the mantissa, allowing the exponent to grow unboundedly (in either direction). From a theoretical standpoint, bounding the number of bits of both the mantissa and the exponent would necessarily give rise to a finite-state system, for which essentially any decision problem would become decidable (at least in theory, if not necessarily in practice). Due to the unboundedness of exponents in our setting, we do not have to consider overflows ('NaN', 'infinity' or '-infinity' which are part of most floating-point specifications).

Formally, we model our programs using linear dynamical systems (LDS), which are composed of a starting vector representing the initial state of each variable of the system and of a matrix describing the evolution of the program. An LDS generates an infinite sequence of vectors (the *orbit* of the system) by multiplying the matrix with the current vector and then applying floating-point rounding to the result.

## Our results

We consider the *model-checking* problem for linear dynamical systems evolving under floating-point rounding. More formally, let $Y_1, \dots, Y_k \subseteq \mathbb{R}^d$ be semi-algebraic targets. Given an orbit $(x^{(t)})_{t \in \mathbb{N}}$, we define the characteristic word $w = w_1, w_2, w_3, \dots$ with respect to $Y_1, \dots, Y_k$ over alphabet $2^{\{1, \dots, k\}}$ such that $i \in w_t$ if and only if $x^{(t)} \in Y_i$. The model-checking problem asks whether $w$ is in an $\omega$-regular language, or equivalently satisfies a temporal specification given in monadic second-order logic (MSO).

Our results show that analysing LDS under floating-point rounding is neither clearly easier or harder than in the standard setting (without rounding). Our first result establishes *undecidability* of point-to-point reachability (and a fortiori model checking) under floating-point rounding, a surprising outcome given that reachability is solvable in polynomial time without rounding [15]. On the other

<footnote n="5">⁵ We work in base 10 throughout for simplicity of exposition. All our results carry *mutatis mutandis* in any integer base, including base 2 as typically used in practice.</footnote>
hand, in the standard setting neither decidability nor undecidability are known
for full model checking (although mathematical hardness results exist [21]).

**Theorem 1.** The floating-point point-to-point reachability problem is undecid-
able.

However, for non-negative matrices, we show that the model-checking prob-
lem is decidable in our setting, without restrictions on the dimensions of the
predicates or the ambient space. This is in stark contrast to the standard setting,
where assuming non-negativity does not simplify the problem. Model checking
non-negative LDS without rounding would require (at a minimum) solving the
longstanding open Skolem and Positivity problems [2].

**Theorem 2.** Let $(M, x)$ be a non-negative linear dynamical system, let $Y_1, \dots, Y_k$ be semialgebraic targets and let $\phi$ be an MSO formula using predicates over $Y_1, \dots, Y_k$. It is decidable whether the characteristic word under floating-point rounding satisfies $\phi$.

We place no dimension restriction on the predicates; in particular, showing
that the Skolem and Positivity problems are *decidable* on non-negative systems
under floating-point rounding. At this time we do not however have complexity
upper bounds on our model-checking algorithm, or lower bounds on the model-
checking problem.

Related work

There is a line of practical tools for the analysis, verification and invariant synthesis for floating-point loops [7,17,1,19]. These tools typically work well in practice, but do not necessarily work in all cases. The analysis of concrete implementations of floating-point specifications requires careful analysis of edge cases around $\pm\infty$ and ‘NaN’. In contrast to these tools which focus primarily on practical analysis, our work seeks to understand the theoretical possibilities and limitations of the exact analysis of (possibly long running) floating-point loops in a generalised setting.

The study of linear dynamical systems explores the sequence of vectors in-
duced by a matrix. Model checking is only known to be decidable for certain
classes of semialgebraic predicates—in particular those with low dimension [16]
or for prefix-independent properties [4]. The well-known Skolem and Positivity
problems being special cases of model checking, they place technical limits on
the dimension that can be addressed without first resolving long-standing open
cases of these problems. Recent progress suggests that the Skolem problem may
be feasible, at least for diagonalisable matrices [8,18], but Positivity requires
solving particularly difficult problems in analytic number theory [21,11]. The
non-negative case can be used to model sequences of probabilities induced by
Markov chains [6], although all hardness limitations apply already in the prob-
abilistic setting [2].
Baier et al. [5] consider LDS under rounding to fixed-decimal precision, show-
ing reachability is PSPACE-complete for hyperbolic systems (when no eigenvalue
has modulus one) and decidable for certain other constrained classes of rounding.
A notable difference of fixed-decimal precision is that it cannot allow arbitrarily
small numbers, unlike the floating-point numbers we consider.

A recent line of work considers linear dynamical systems with perturbations
at every step, with a view to understanding the robustness of reachability prob-
lems [12,13,3]. However, unlike rounding, the perturbation is chosen in order to
assist hitting the target and the perturbation is arbitrarily small.

*Organisation*
This paper is organised as follows. In Section 2, we formalise the
model and problems and discuss some of the properties of floating-point round-
ing. In Section 3, we present our undecidability result for the general case. Fi-
nally, in Section 4 we establish some special periodic structure associated with
the orbit and use this structure in Section 5 to show that model checking is
decidable for non-negative LDS.

2 Preliminaries

**2.1 Linear dynamical systems and rounding functions**

**Definition 1.** A $d$-dimensional linear dynamical system (LDS) $(M, x)$ comprises a matrix $M \in \mathbb{Q}^{d \times d}$ and an initial vector $x \in \mathbb{Q}^d$.

Given a rounding function $[\cdot] : \mathbb{Q}^d \to \mathbb{Q}^d$, and an LDS $(M, x)$ the rounded orbit $\mathcal{O}$ is the sequence $(x^{(t)})_{t \in \mathbb{N}}$ such that $x^{(0)} = [x]$ and $x^{(t)} = [Mx^{(t-1)}]$ for all $t \ge 1$.

Given $p \in \mathbb{N}$, we say that a number $x$ is a floating-point number with precision $p$ if $x = m \cdot 10^{\alpha}$ such that $m \in \mathbb{Q}$ is a decimal number in $\{0\} \cup [0.1, 1)$ with $p$ digits in the fractional part (after the decimal point) and $\alpha \in \mathbb{Z}$. In particular, we associate by convention the number with mantissa $m = 0$ to the exponent $-\infty$. Given a number $x = m \cdot 10^{\alpha}$ we define **mantissa**($x$) = $m$ and **exponent**($x$) = $\alpha$.

We are interested in the floating-point rounding function $[\cdot]$ with precision $p \in \mathbb{N}$. Given a real number $x \in \mathbb{R}$, we define $[x]$, the floating-point rounding of $x$, as the closest floating-point number with precision $p$ based on the first $p+1$ digits of $x$.

Where there are two possible choices, any deterministic choice that is con-
sistent with the properties listed below is acceptable<fnref n="6" />. We denote by $\mathbb{FP}_{10}[p]$ the
subset of $\mathbb{Q}$ representable in base 10 as a floating-point numbers with $p$ digits.
We use the following useful properties of the rounding function:

- it is log-bounded, i.e. there exists a constant $c \in \mathbb{R}_+$ such that $\forall x \in \mathbb{R}, \frac{|x|}{c} \le |[x]| \le c|x|$.

<footnote n="6">⁶ For example, always rounding up, always rounding down, round to even, rounding towards zero, rounding away from zero are acceptable providing it is fixed.</footnote>
- it is *mantissa-based*, i.e. if $x = 10^{\alpha}x'$, then $[x] = 10^{\alpha}[x']$.

- it is *p+1-finite*, i.e. the output of the rounding is not dependent on the $i$'th digit of the mantissa, for each integer $i > p+1$. In other words, if $x$ and $x'$ agree on the first $p+1$ digits then $[x] = [x']$.

- it is *sign preserving*, i.e. $\operatorname{sign}(x) = \operatorname{sign}([x])$. The fact that $[x] = 0$ if and only if $x = 0$ also follows from the log-bounded property.

The floating-point rounding is defined above on a single real. It is extended straightforwardly to a vector $x$ by applying it to each of its component $(x)_i$ where $i$ ranges from 1 to the dimension of the vector. As such, the term $[Mx]$ is obtained by first computing exactly the the vector $Mx$ and then by rounding each component $(Mx)_i$. An alternative approach could be to maintain each sub-computation in $p$-bits of precision, *but this is not the approach we take*. Such an orbit can be simulated in our setting by increasing the dimension so that operations can be staggered in a way that at most one operation (scalar product or variable addition) is used in each assignment.

## 2.2 Model checking

We consider the model-checking problem of an LDS over semialgebraic sets.

**Definition 2.** A semialgebraic set $Y \subseteq \mathbb{R}^d$ is defined by a finite Boolean combination of polynomial inequalities.

Let $(M, x)$ be an LDS with rounded orbit $O$ and $\mathcal{Y} = \{Y_1, \dots, Y_k\}$ be a collection of semialgebraic sets. The characteristic word of $O$ is $w = w_1w_2w_3\dots \in (2^{\{1,\dots,k\}})^\omega$, such that $j \in w_t$ if and only if $x^{(j)} \in Y_j$.

The model-checking problem asks whether the characteristic word is contained within a given $\omega$-regular language, usually specified in a temporal logic such as monadic second order logic (MSO), and often the LTL fragment. Without loss of generality we assume that the property is given as Büchi automaton [10].

**Problem 1 (Floating-point Model-checking Problem).** Given an LDS $(M, x)$ with rounded orbit $O$, a collection of semialgebraic sets $\mathcal{Y} = \{Y_1, \dots, Y_k\}$ and an $\omega$-regular specification $\phi$, the model-checking problem consists in deciding whether the characteristic word $w$ of $O$ satisfies the specification $\phi$.

We will also consider the point-to-point reachability problem, which is a subcase of the model-checking problem (Problem 1):

**Problem 2 (Floating-point Point-to-point Reachability Problem).** Given a $d$-dimensional LDS $(M, x)$, and a target vector $y \in \mathbb{Q}^d$, the point-to-point reachability problem consists in deciding whether $y$ belongs to the rounded orbit $O$.

Given a target $Y \subseteq \mathbb{R}^d$, we associate the set of hitting times $\mathcal{Z}(Y) = \{t \mid x^{(t)} \in Y\}$. Under this formulation, the reachability problem is reformulated as whether $\mathcal{Z}(Y)$ is empty. However, for model checking we will develop a more comprehensive understanding of the hitting times of each target $Y_1, \dots, Y_k$.
## 2.3 Structure of M

Formally, as a $d$-dimensional matrix $M$ is indexed by the elements $\{1, \dots, d\}$. However, we interpret $M$ as an automaton over states $Q = \{q_1, \dots, q_d\}$ and reference the matrix in the natural way by pairs of elements of $Q$. We can represent the automaton as a directed graph $G_M$, with vertices $Q$ and an edge from $q_j$ to $q_i$ weighted by $M_{i,j}$ (which we will denote $M_{q_i,q_j}$) if $M_{q_i,q_j} \neq 0$. We draw the readers attention to the orientation of the edge may appear switched, which stems from our consideration of the matrix being pre-multiplied at every step as is standard in the study of linear dynamical systems.

This motivates a closer attention to the structure of the graph. Denote every strongly connected component (SCC) of $G_M$ as $S_1, \dots, S_s$. We can split a vector $x$ into $s$ smaller vectors such that variables in a same vector are in the same SCC. Without loss of generality, by reordering where necessary, we assume the entries appear in order consistent with their topological sort i.e. there is no edge from $S_i$ to $S_j$ where $i > j$, we have the following partition

$$x = (z_{1,1} \cdots z_{d_1,1}, \cdots, z_{1,s} \cdots z_{d_s,s})^T$$

where $z_{1,j}, \dots, z_{d_j,j}$ are the variables related to $S_j$, for each integer $1 \le j \le s$. For the sake simplicity, denote $(z_{1,j}, \dots, z_{d_j,j})^T$ as $x_{S_j}$, for each integer $1 \le j \le s$.

Moreover, for each positive integers $1 \le i, j \le d$, we denote the intersection of rows related to the $i$'th SCC and columns related to the $j$'th SCC, which is a matrix with $d_i$ rows and $d_j$ columns, as $M_{S_i,S_j}$. If $S_i = S_j$, we simply write $M_{S_i}$. In another word, $M_{S_i,S_j}$ is the matrix that shows the dependency between $S_i$ and $S_j$, and we have

$$M = \begin{pmatrix} M_{S_1} & M_{S_1,S_2} & \cdots & M_{S_1,S_s} \\ M_{S_2,S_1} & M_{S_2} & \cdots & M_{S_2,S_s} \\ \vdots & \vdots & \ddots & \vdots \\ M_{S_s,S_1} & M_{S_s,S_2} & \cdots & M_{S_s} \end{pmatrix}$$

We say $S_i$ feeds $S_j$, and $S_j$ is fed by $S_i$ if there is some edge from $S_i$ to $S_j$.

## 3 Undecidability of point-to-point reachability

In this section, we give a sketch of the proof of the undecidability of Problem 2 (and thus of Problem 1) in the general case. The full proof is postponed to Appendix A.

**Theorem 1.** *The floating-point point-to-point reachability problem is undecid-able.*

This result is obtained by reduction of a two-counter Minsky machine. We recall here the definition of this model:
**Definition 3.** A two-counter Minsky machine is defined by a finite set of states $\ell_1, \dots, \ell_m$, a distinguished starting state (w.l.o.g. $\ell_1$), a distinguished halting state (w.l.o.g. $\ell_m$), two natural integer counters, here denoted as $x$ and $y$, and a mapping deterministically associating to each state transition.

Each transition takes one of the following forms: for $z \in \{x, y\}$,

**increment** $\text{inc}_z(\ell_j)$: add 1 to counter $z$, move to state $\ell_j$.

**decrement** $\text{dec}_z(\ell_j)$: remove 1 from counter $z$ if $z > 0$, move to state $\ell_j$.

**zero test** $\text{zero}_z(\ell_j, \ell_k)$: if $z = 0$ move to state $\ell_j$ else move to state $\ell_k$.

The configuration of a two-counter Minsky machine consists of the current state and the values of $x$ and $y$.

Without loss of generality (by first using a zero test), one can assume a decrementation operation is never used in a configuration where the would-be decreased counter has value 0, hence removing the need to check whether $z > 0$.

The halting problem asks whether, starting in configuration $(\ell_1, 0, 0)$, that is, in the distinguished starting state with both counters set to 0, whether the state $\ell_m$ is reached. The problem is undecidable [20].

We build an LDS with mantissa length $p = 1$ and base 10 that emulates a run of a given Minsky machine. In particular, our reduction maintains that the mantissa always has the value 0 or 1 after rounding (although, as we operate in base 10, there are 10 possible values the mantissa could have taken). For ease of readability, we describe this LDS using variables to represent the dimensions and linear functions to represent the transition matrix. For each state of the Minsky machine, we use two variables corresponding to the two counters. At any point in the run of the LDS, the variables associated to state $j$ are not equal to 0 if the corresponding run of the emulated machine is in state $j$.

The crux of our reduction lies in the handling of the zero test. More precisely, assume that we wish to test whether $x$ is equal to 0, then we need to define linear transitions that transfer the values of the two counters from one pair of variables to the right new pair of variables. This is done using filter functions: the function $\text{filter}_+(u, v)$ (resp. $\text{filter}_-(u, v)$) is equal to $v$ if $v \ge u$ (resp. $v < u$) and to 0 otherwise. We end this sketch with the construction and proof of those functions.

**Lemma 1.** Given $u, v$ of the form $10^c$ with $c \in \mathbb{N}$, one can compute the value $w = \text{filter}_+(u, v)$ in three linear operations with floating-point rounding.

*Proof.* We compute $w = \text{filter}_+(u, v)$ in three successive operations using two temporary variables, $\text{temp}$ and $\text{temp2}$, initially set at 0 (recall, rounding is applied after each step):

$$ \text{temp} \leftarrow u + v $$

$$ \text{temp2} \leftarrow \text{temp} - u $$

$$ w \leftarrow 1.1 * \text{temp2} $$

Let $c_1, c_2 \in \mathbb{N}$ such that $u = 10^{c_1}$ and $v = 10^{c_2}$. Recall that the notation $[\cdot]$ is the floating-point rounding function.
First observe that if $c_1 = c_2$:

$$ \mathit{temp} \leftarrow [10^{c_1} + 10^{c_2}] = 2 \cdot 10^{c_1} $$

$$ \mathit{temp2} \leftarrow [2 \cdot 10^{c_1} - 10^{c_1}] = 10^{c_1} (= v) $$

$$ w \leftarrow [1.1 \cdot 10^{c_1}] = 10^{c_1} = v \quad \text{as required.} $$

Secondly, assume that $u > v$, and thus $c_1 > c_2$:

$$ \mathit{temp} \leftarrow [10^{c_1} + 10^{c_2}] = 10^{c_1} = u $$

$$ \mathit{temp2} \leftarrow [10^{c_1} - 10^{c_1}] = 0 $$

$$ w \leftarrow [1.1 \cdot 0] = 0 \quad \text{as required.} $$

We split the case that $v > u$, thus $c_2 > c_1$, into two cases. Suppose $c_2 > c_1 + 1$:

$$ \mathit{temp} \leftarrow [10^{c_1} + 10^{c_2}] = 10^{c_2} = v $$

$$ \mathit{temp2} \leftarrow [10^{c_2} - 10^{c_1}] = [0.\underline{99} \dots \underline{99} \cdot 10^{c_2}] = 1 \cdot 10^{c_2} = v $$

$$ w \leftarrow [1.1 \cdot 10^{c_2}] = 10^{c_2} = v \quad \text{as required.} $$

Finally, $c_2 = c_1 + 1$:

$$ \mathit{temp} \leftarrow [10^{c_1} + 10^{c_2}] = 10^{c_2} = v $$

$$ \mathit{temp2} \leftarrow [10^{c_2} - 10^{c_1}] = [0.9 \cdot 10^{c_2}] = 9 \cdot 10^{c_2-1} $$

$$ w \leftarrow [1.1 \cdot 9 \cdot 10^{c_2-1}] = [9.9 \cdot 10^{c_2-1}] = 10 \cdot 10^{c_2-1} = 10^{c_2} = v $$

as required.

Observe that 1.1 cannot be encoded with a mantissa of length 1, but can be encoded as $\mathit{temp2} + 10^{-1} \cdot \mathit{temp2}'$ where $\mathit{temp2}'$ is a second copy of $\mathit{temp2}$. $\square$

**Corollary 1.** Given $u, v$ of the form $10^c$ with $c \in \mathbb{N}$, one can compute the value $w = \mathit{filter}_-(u, v)$ in four linear operations with floating-point rounding.

*Proof.* Observe that $\mathit{filter}_-(u, v) = v - \mathit{filter}_+(u, v)$, which can be encoded in four steps by first computing $\mathit{filter}_+(u, v)$ in three steps. $\square$

# 4 Pseudo-periodic orbits of non-negative LDS

We shift our focus to proving that model checking is decidable for systems with non-negative matrices. We first establish the behaviour of the system in this section and then complete the proof of Theorem 2 in Section 5. Our main result is that the rounded orbit of an LDS is periodic in the following sense, which we call pseudo-periodic.

**Definition 4.** A sequence $(x^{(t)})_{i \in \mathbb{N}}$ of $d$-dimensional vectors of floating-point numbers is called pseudo-periodic if and only if there exists a starting point $N \in \mathbb{N}$, period $T \in \mathbb{N}$ and growth-rates $\alpha_1, \dots, \alpha_d \in \mathbb{Z}$ such that

$$ \forall t \ge N, \forall j \in \{1, \dots, d\}, (x^{(t+T)})_j = 10^{\alpha_j} (x^{(t)})_j. $$

We say the sequence is effectively pseudo-periodic if the defining constants $N, T, \alpha_1, \dots, \alpha_d$ can be computed.

**Theorem 3.** Let $(M, x)$ be a $d$-dimensional LDS where each entry is non-negative and let $(x^{(t)})_{t \in \mathbb{N}}$ be its rounded orbit.

The rounded orbit $(x^{(t)})_{t \in \mathbb{N}}$ is effectively pseudo-periodic.
In order to establish this theorem, we will find some partitions of the graph
associated to $M$ such that each part is effectively pseudo-periodic with the same
$\alpha$ in the increase-rate for each state within the partition.

## 4.1 Preprocessing periodicity

The core of our approach is to show that, within each SCC of the graph associated
to $M$, the values associated with states are of similar magnitude. This is only
true however if the SCC is aperiodic. When a state is in a periodic SCC its
value could change drastically depending on which phase the system is in. For
example, consider a simple alternation between two states, in which the value
is very large in one state and very small in the other; the states will alternate
between big and small values.

We “hide” these periodic behaviours by blowing up the system so that each
SCC of the new system describes only one of the periodic subsequence and we
will subsequently show that the value of each state in an SCC is either zero or
of a similar magnitude.

We apply the following construction to our system. Let $P$ be the least com-
mon multiple of the length of every simple cycle in the graph. Let $Q$ be the
indexes of $M$ (aka the states of the automaton it generates). We define new
states $Q' = Q \times \{0, \dots, P-1\}$ by annotating each state in $Q$ with the phase. To
avoid cluttering notation we will regularly refer to states in $Q'$ in the form $(q, i+\ell)$
for $\ell \in \mathbb{Z}$, this is done on the understanding that the phase, $i+\ell$, is normalised
into $\{0, \dots, P-1\}$ by taking the residue modulo $P$. We define a new matrix $M'$
over the states $Q'$ such that $M'_{(q,i+1),(q',i)} = M_{q,q'}$ for $i \in \{0, \dots, P-1\}$. We
initialise a new starting vector $x_{(q,0)}^{(0)} = x_q^{(0)}$ and $x_{(q,i)}^{(0)} = 0$ for $i \in \{1, \dots, P-1\}$.
Intuitively, at each time step $t$ the vector generated by the initial system is equal
to the vector of the new system restricted to the states indexed by $i \equiv t \mod P$
and every state with another index is equal to 0.

Let $S \subseteq Q$ be a strongly connected component. In $Q'$ there exists strongly
connected components $S'_1, \dots, S'_k \subseteq Q'$ with $k \le |S|$ such that $\bigcup_{i=1}^k S'_i =$
$\{(q, i) \in Q' \mid q \in S \wedge i \in \{0, \dots, P-1\}\}$. Each set $S'_j$ is periodic, with pe-
riod $P$.

Henceforth in the rest of this section we work on the system $(M', x')$ implicitly
over states $Q'$ which, by overloading of notation, we rename $(M, x)$ over $Q$ to
avoid cluttering notation.

Note that this transformation also requires to marginally complicate the
reachability sets that one may target. Indeed, consider a set $Y \subseteq \mathbb{R}^Q$. We define
the sets $Y/i$ for $i < P$ such that $Y/i = \{y \in \mathbb{R}^{Q'} \mid \exists y' \in Y : y_{(q,i)} = y'_q$ for $q \in$
$Q$ and $y'_{(q,j)} = 0$ for $j \ne i\}$}. The hitting times of $Y$, $\mathcal{Z}(Y)$, in the original LDS
can then be obtained in the new LDS as $\bigcup_{i \in \{0, \dots, P-1\}} \mathcal{Z}(Y/i)$, where the union
is disjoint. Hence, it suffices to characterise the reachability sets for each $Y/i$.
## 4.2 Pseudo-periodicity within top SCCs

Let us first consider top SCCs, these are SCCs with no incoming edges from states of other SCC, and therefore the value of each variable at each step depends only on the value of states in the same SCC.

**Lemma 2.** Let $S_j$ be a strongly connected component of $(M, x)$. Let $S_{j,i} = \{(q, i) \in S_j\}$ be the states associated with $S_j$ from the ith phase.

There exists $C \le Pd^2$, such that for every $i, j$ $(M^C)_{S_{j,i}}$ is positive.

*Proof.* The matrix $(M^P)_{S_{j,i}}$ is non-negative, irreducible (aka its graph is strongly connected) and of period 1. As such, $(M^P)_{S_{j,i}}$ is primitive [9] which means that a power $C'$ of this matrix is positive. The theorem follows with $C = PC'$. Moreover, $C'$ is at most $d^2 - 2d + 2|22|$. □

Our goal is to show that within an SCC, each of the non-zero entries are of a similar magnitude due to the presence of a relatively short path ($C$) between any two states in the SCC. To do this we introduce the notion of closeness and observe some useful properties.

**Definition 5.** We say two numbers $x, x' \in \mathbb{FP}_{10}[p]$ are $\delta$-close, denoted by $x \approx_{\delta} x'$ if $|\text{exponent}(x) - \text{exponent}(x')| < \delta$. In particular, 0 is assumed to be $\delta$-close to itself only for every $\delta$.

We extend the notion to vectors $y, y \in \mathbb{FP}_{10}[p]^S$, indexed by $S \subseteq Q$, such that $y \approx_{\delta} y'$ if for each phase $i \in \{0, \dots, P-1\}$ and all $(q, i), (q', i) \in S$: $y_{(q,i)} \approx_{\delta} y'_{(q',i)}$, $y_{(q,i)} \approx_{\delta} y_{(q',i)}$ and $y'_{(q,i)} \approx_{\delta} y'_{(q',i)}$.

**Proposition 1.** Let $x, x' \in \mathbb{FP}_{10}[p]$ be non-zero floating-point numbers.

(1) If $x \approx_{\delta} x'$ then $10^{-\delta-1} \le x/x' \le 10^{\delta+1}$.

(2) If $10^{-\delta} \le x/x' \le 10^{\delta}$ then $x \approx_{\delta+2} x'$.

(3) If $x \approx_{\delta} x'$ and $x' \approx_{\eta} x''$ then $x \approx_{\delta+\eta+4} x''$.

**Lemma 3.** Let $S_j$ be a top strongly connected component of $(M, x)$, and let $C$ be as given by Lemma 2.

There exists $\beta, \in \mathbb{N}$ such that for all $(q, i), (q', i) \in S_j$ and every $t \ge C$ then

- if $t \not\equiv i \pmod{P}$, then $x_{(q,i)}^{(t)} = 0$,

- otherwise, $x_{(q,i)}^{(t)} \approx_{\beta} x_{(q',i)}^{(t)}$.

*Proof.* Let $t \in \mathbb{N}$. If $t \not\equiv i \pmod{P}$ then $x_{(q,i)}^{(t)} = 0$ for all $(q, i) \in S_{j,i}$ by construction.

Otherwise, let $m \ge \max_{q,q' \in Q: M_{q,q'} \ne 0} \max(M_{q,q'}, (M_{q,q'})^{-1})$ be a constant larger than all values occurring in $M$ and so that $1/m$ is smaller than all non-zero values appearing in $M$. Let $c$ be the constant from the log bounded property of the rounding function $[\cdot]$ and $d$ be the dimension of $M$.
Observe that for all $t \in \mathbb{N}$ with $t = i \bmod P$ we have

$$ 
\begin{aligned}
x_{(q,i)}^{(t)} &= \left[ \sum_{(q',i-1)} M_{(q,i),(q',i-1)} x_{(q',i-1)}^{(t-1)} \right] \\
&\geq \frac{1}{c} \sum_{(q',i-1)} M_{(q,i),(q',i-1)} x_{(q',i-1)}^{(t-1)} \quad \text{(by log bounded)} \\
&\geq \frac{1}{cm} \max_{(q',i-1)|M_{(q,i),(q',i-1)}>0} x_{(q',i-1)}^{(t-1)} \quad \text{(by defn of $m$)}
\end{aligned}
$$

In particular

$$ x_{(q,i)}^{(t)} \geq \frac{1}{cm} x_{(q',i-1)}^{(t-1)} \quad \text{for all } (q', i-1) \text{ s.t. } M_{(q,i),(q',i-1)} > 0 $$

Using induction we obtain:

$$ x_{(q,i+k)}^{(t+k)} \geq \frac{1}{(cm)^{k-1}} x_{(q',i+1)}^{(t+1)} \geq \frac{1}{(cm)^k} x_{(q'',i)}^{(t)} $$

for all $(q', i+1), (q'', i)$ such that $M_{(q,i+k),(q',i+1)}^{k-1} > 0$ and $M_{(q',i+1),(q'',i)} > 0$.

In particular, we have $x_{(q,i)}^{(t+C)} \geq \frac{1}{(cm)^C} x_{(q',i)}^{(t)}$ for all $q'$ (since $M_{(q,i),(q',i)}^{C} > 0$ for all $q'$ by the previous lemma).

On the other hand we have

$$ x_{(q,i+1)}^{(t+1)} = \left[ \sum_{q':M_{(q,i+1),(q',i)}>0} M_{(q,i+1),(q',i)} x_{(q',i)}^{(t)} \right] \leq mcd \max_{(q',i) \in S_j} x_{(q',i)}^{(t)}. $$

By induction we get that $x_{(q,i)}^{(t+C)} \leq (mcd)^C \max_{(q',i) \in S_j} x_{(q',i)}^{(t)}$. Hence, for all $q, q' \in S_j$ we have

$$ \frac{1}{(mc)^C} \max_{(q'',i) \in S_j} x_{(q'',i)}^{(t)} \leq x_{(q',i)}^{(t+C)} \quad \text{and} \quad x_{(q,i)}^{(t+C)} \leq (mcd)^C \max_{(q'',i) \in S_j} x_{(q'',i)}^{(t)}. $$

$$ \text{Hence } \frac{x_{(q,i)}^{(t+C)}}{x_{(q',i)}^{(t+C)}} \leq d^C(mc)^{2C}. $$

Setting $\gamma = [\log_{10} d^C(mc)^{2C}]$, we thus have that $10^{-\gamma} x_{(q',i)}^{(t+C)} \leq x_{(q,i)}^{(t+C)} \leq 10^{\gamma} x_{(q',i)}^{(t+C)}$ for all $(q, i), (q', i) \in S_{j,i}$ and $t \in \mathbb{N}$. Then $x_{(q',i)}^{(t)}$ and $x_{(q,i)}^{(t)}$ are $\beta = \gamma+2$ close by Proposition 1. $\square$

**Lemma 4.** Let $S_j$ be a top strongly connected component of $(M, x)$. Then the sequence $(x_{S_j}^{(t)})_{t \in \mathbb{N}}$ is effectively pseudo-periodic.

*Proof.* Let $\beta$ and $C$ be as in Lemma 3. Denote $q_1, \dots, q_m$ the states of $S_j$. We define the sequence $(y^{(t)})_{t \geq C}$ such that for all $t \geq C$ and $q \in S_j$ denoting $(p^{(t)})_q = \text{mantissa}([x_q^{(t)}])$ and $(\alpha^{(t)})_q = \text{exponent}([x_q^{(t)}])$ we have that $y^{(t)} =$
$(p_{q_1}, 0, p_{q_2}, \alpha_{q_2} - \alpha_{q_1}, \dots, p_{q_m}, \alpha_{q_m} - \alpha_{q_1})$. Note that this sequence can only take finitely many values as the mantissas have a precision of $p$ decimals and by Lemma 3, for all $k \le m$, $\alpha_{q_k} - \alpha_{q_1} \in \{-\beta, \dots, \beta\}$. As a consequence, the sequence $(y^{(t)})_{t \ge C}$ takes the same value multiple times. Let $k_1$ and $k_2$ be the two minimal integers such that $y^{(k_1)} = y^{(k_2)}$. Setting $\alpha = \alpha_{q_1}^{(k_2)} - \alpha_{q_1}^{(k_1)}$ We have that $x^{(k_1)} = x^{(k_2)} \cdot 10^{\alpha}$. Since $[$ is mantissa-based, one can show by induction that for all $t \ge 0$, $x^{(k_1+t)} = x^{(k_2+t)} \cdot 10^{\alpha}$. Therefore the sequence $(x_{S_j}^{(t)})_{t \in \mathbb{N}}$ is effectively pseudo-periodic with period $T = k_2 - k_1$ and starting point $N = C + k_1$.

Moreover, as the maximum number of different values taken by $(y^{(t)})_{t \ge C}$ is known, we can deduce that both $k_1$ and $k_2 - k_1$ are smaller than $10^{pm}(2\beta+1)^m+1$.

□

Note that the increase rate is the same for every state of the strongly connected component.

## 4.3 Pseudo-periodicity within lower SCCs

We consider a strongly connected component $S_{me}$, which is fed by at least one strongly connected components $F_1, \dots, F_\ell, \ell \ge 1$. We let $S_F = F_1 \cup \dots \cup F_\ell$ and assume every $F_i$ is pseudo-periodic.

In this section we show

**Theorem 4.** $S_{me}$ is effectively pseudo-periodic and the growth-rate of $S_{me}$ is the same for all $q \in S_{me}$.

We first observe that the difference between values in $S_{me}$ is bounded. This is achieved with a proof similar to the one of Lemma 2 and Lemma 3 (though having to combine considerations of $S_{me}$ and $S_F$).

**Lemma 5.** There exists $\eta, N' \in \mathbb{N}$, such that for all $(q, i), (q', i) \in S_{me}$, all $t \ge N'$ and all $i \in \{0, \dots, P-1\}$ then

- if $t \ne i \bmod P$, then $x_{(q,i)}^{(t)} = 0$,

- otherwise, $x_{(q,i)}^{(t)} \approx_{\eta} x_{(q',i)}^{(t)}$.

**Definition 6.** We say that $x_q^{(t)}$ is influenced by $S_F$ if

$$x_q^{(t)} = \left[ \sum_{q' \in S_F} M_{q,q'} x_{q'}^{(t-1)} + \sum_{q' \in S_{me}} M_{q,q'} x_{q'}^{(t-1)} \right] \ne \left[ \sum_{q' \in S_{me}} M_{q,q'} x_{q'}^{(t-1)} \right]$$

and in particular $x_q^{(t)}$ is influenced by $u \in S_F$ if:

$$\left[ \sum_{q' \in S_F \cup S_{me}} M_{q,q'} x_{q'}^{(t-1)} \right] \ne \left[ \sum_{q' \in S_F \cup S_{me} \setminus \{u\}} M_{q,q'} x_{q'}^{(t-1)} \right].$$
We can restrict $S_F$ to the $F_i$ in $S_F$ with the maximum growth rate. Indeed, from some point on, any $F_i$ with non-maximal growth rate is much smaller than the maximal ones, and as by the proof of Lemma 5 the values within $S_{me}$ are close (or greater) to the maximum value within $S_F$, this $F_i$ would not interfere with any $x_q^{(t)}$ with $q \in S_{me}$. Let $N_1$ be the point from which we can assume, that the elements of $S_F$ are much larger than any other feeding SCCs and are thus the only ones potentially influencing of $S_{me}$.

Since each $F_i$ is pseudo-periodic, we have that $S_F$ pseudo-periodic. Let $T$ be the period of $S_F$, $N_2$ be the starting point and $\alpha$ be the growth rate of every state dimension of $S_F$ (meaning the exponent of every state changes by $\alpha$ every $T$ starting from the $N$th step.) Let $N = \max_{N_2,N_1}$, that is, the point from which we can assume $S_F$ is both pseudo-periodic and dominating non-maximal SCCs feeding $S_{me}$.

As a direct consequence of having the same growth rate, the non-zero terms within $S_F$ are close.

**Proposition 2.** If a sequence of non-zero floating-point vectors $(v^{(t)})_{t \in \mathbb{N}}$ is pseudo-periodic with the same growth rate within a set $Q$, then there exists $\delta$ such that for all $q, q' \in Q$ and all $t \ge N$, $v_q^{(t)} \approx \delta v_{q'}^{(t)}$.

Moreover, either $S_F$ does not influence $S_{me}$, or they are close.

**Lemma 6.** There exists $\beta, N \in \mathbb{N}$ such that:

For $t \ge N$ and $(q, i) \in S_{me}$, if $x_{(q,i)}^{(t)}$ is influenced by $(q', i - 1) \in S_F$, then $x_{(r,i)}^{(t)} \approx \beta x_{(r',i)}^{(t)}$ for all $(r, i)$, $(r', i) \in S_{me} \cup S_F$.

We will show Theorem 4 through the following observation:

**Observation 1.** Observe that $S_F$ either influences $S_{me}$ infinitely many times or finitely many times. We have two cases:

- If $S_F$ influences $S_{me}$ infinitely often, then they are infinitely often $\beta$-close by Lemma 6. Then we will observe through a simultaneous version of Lemma 4 that $S_{me}$ is pseudo-periodic.

- If $S_F$ influences $S_{me}$ only finitely often, then it is clear that from some point on $S_{me}$ behaves like a top SCC, and thus is pseudo-periodic directly by Lemma 4.

It will then remain to show that we can detect which of the two cases applies, and place a bound on the time to detect this, which will effectively reveal the constants of the pseudo-periodic behaviour.

Let us now consider a version of Lemma 4 that simultaneously considers $S_F$ and $S_{me}$ to observe that if $S_F$ and $S_{me}$ are infinitely often $\beta$-close then $S_{me}$ is pseudo-periodic:

**Lemma 7.** Suppose $x_{S_F}^{(t)} \approx \beta x_{S_{me}}^{(t)}$ for infinitely many $t$. Then there exists $t_1 < t_2$, such that $x_{S_F}^{(t_1)} \approx \beta x_{S_{me}}^{(t_1)}$ and $x_{S_F}^{(t_2)} \approx \beta x_{S_{me}}^{(t_2)}$, $x_{S_F}^{(t_2)} = 10^\gamma x_{S_F}^{(t_1)}$ and $x_{S_{me}}^{(t_2)} = 10^\gamma x_{S_{me}}^{(t_1)}$. In particular, the sequence $(x_{S_{me}}^{(t)})_{t \in \mathbb{N}}$ is pseudo-periodic with period $(t_2 - t_1)$, starting from $t_1$ with growth-rate of $\gamma$ in every state.
*Proof.* At a time $t$ such that $x_{S_F}^{(t)} \approx_{\beta} x_{S_{me}}^{(t)}$, we denote the vectors $x_{S_F} \in \mathbb{F}_{10}[p]^{|S_F|}$ and $x_{S_{me}}^{(t)} \in \mathbb{F}_{10}[p]^{|S_{me}|}$ respectively

$$(m_1^{(t)} 10^{\gamma_1^{(t)}}, m_2^{(t)} 10^{\gamma_2^{(t)} + \alpha_2^{(t)}}, \dots, m_{|S_F|}^{(t)} 10^{\gamma^{(t)} + \alpha_{|S_F|}^{(t)}}) \text{ and}$$

$$(n_1^{(t)} 10^{\gamma^{(t)} + \zeta_1^{(t)}}, \dots, n_{|S_{me}|}^{(t)} 10^{\gamma^{(t)} + \zeta_{|S_{me}|}^{(t)}}),$$

where $m_i, n_i$ are taken from the finite set of mantissa values expressible in $p$ bits, $\gamma^{(t)} \in \mathbb{Z}$ and $\alpha_i, \zeta_i \in \mathbb{Z} \cap [-\beta, \beta]$ denote the offset from $\gamma^{(t)}$.

Let $F$ bound the number of possible values $m_i, n_i, \alpha_i, \zeta_i$ can take on, where $F \le 10^{p(|S_F|+|S_{me}|)} \cdot (2\beta + 1)^{|S_F|+|S_{me}|-1}$. By the pigeon hole principle, after at most $F + 1$ times in which $x_{S_F}^{(t)} \approx_{\beta} x_{S_{me}}^{(t)}$ there must exist two times $t_1 < t_2$ where the values of $m_i, n_i, \alpha_i, \beta_i$'s are equal (although the value of $\gamma$ could be different), thus $x_{S_F \cup S_{me}}^{(t_2)} = \frac{10^{\gamma^{(t_2)}}}{10^{\gamma^{(t_1)}}} x_{S_F \cup S_{me}}^{(t_1)}$.

Since the rounding function is mantissa-based, the system evolution from $x^{(t_1)}$ is equivalent to the systems evolution from $x^{(t_2)} = 10^{\gamma} x^{(t_1)}$, where $\gamma$ is the growth rate, $\gamma^{(t_2)} - \gamma^{(t_1)}$. $\square$

The following lemma says that we can decide whether $x_{S_F}^{(t)} \approx_{\beta} x_{S_{me}}^{(t)}$ for the last time.

**Lemma 8.** Let $\beta, N$ be defined as in Lemma 6. If $t \ge N$ then it is decidable whether there exists $t' > t$ such that $x_{S_F}^{(t')} \approx_{\beta} x_{S_{me}}^{(t')}.$

*Proof Sketch (Full proof in Appendix F).* If we considered $S_{me}$ in isolation, without the effect of $S_F$, we know it would be pseudo-periodic. We can simulate one period of $S_{me}$ with and without the effect of $S_F$ and determine if $S_F$ influences $S_{me}$ within one period. If it does then they must be close at this point. If $S_F$ does not influence $S_{me}$ we know that $S_{me}$ will behave pseudo-periodically at least until $S_F$ is close to $S_{me}$ again; having established a growth rate for $S_{me}$, we can compare the growth rates of $S_F$ and $S_{me}$ to see if $S_{me}$ will ever be close to $S_F$ again in the future. $\square$

Finally to conclude the proof of Theorem 4, we refine Observation 1 to show that the period is bounded and thus the growth rates are computable:

- either $S_F$ is $\beta$-close to $S_{me}$ infinitely often, in particular if they become close $F + 1$ times then by Lemma 7 it is pseudo-periodic.

- or the system is pseudo-periodic because it behaves like a top-SCC, in which Lemma 4 gives effective computation of the constants.

Which of the two cases occurs can be determined by at most $F + 1$ applications of Lemma 8.
# 5 Decidability of model checking

In this section we use the results obtained in the previous section to show that model checking is decidable. We use pseudo-periodicity to show that the characteristic work is eventually periodic, a case for which model checking is decidable.

**Theorem 2.** Let $(M, x)$ be a non-negative linear dynamical system, let $Y_1, \dots, Y_k$ be semialgebraic targets and let $\phi$ be an MSO formula using predicates over $Y_1, \dots, Y_k$. It is decidable whether the characteristic word under floating-point rounding satisfies $\phi$.

Consider a semialgebraic target $Y$, which can be expressed as a boolean combination of polynomial inequalities over variables representing the dimensions. That is $Y = \{(x_1, \dots, x_d) \mid \bigwedge_i \bigvee_j P_{ij}(x_1, \dots, x_n) \triangleright_{ij} 0\}$, where $\triangleright_{ij} \in \{\ge, >, =\}$.

Given a linear dynamical system $(M, x)$ defining the rounded orbit $(x^{(n)})_{n=1}^{\infty}$, recall the set $\mathcal{Z}(Y) = \{n \mid x^{(n)} \in Y\}$ is the hitting set of $Y$. We claim that this set has is semi-linear (equivalently eventually periodic) for semialgebraic $Y$.

**Definition 7.** A 1-dimensional linear-set, defined by a base $b \in \mathbb{N}$ and period $p \in \mathbb{N}$, is the set $\{x \mid \exists k \in \mathbb{N} : x = b + k \cdot p\}$.

A semi-linear set is the finite union of a finite set $F \subseteq \mathbb{N}$ and linear sets. It can be assumed that each linear-set has the same period. Hence a 1-dimensional semi-linear set $X$ is defined by a finite set $F \subseteq \mathbb{N}$ and integers $m, p, b_1, \dots, b_m \in \mathbb{N}$ such that $x \in X$ if and only if $x \in F$ or $x = b_i + k \cdot p$ for some $k \in \mathbb{N}$ and $i \in \{1, \dots, m\}$.

**Theorem 5.** Let $Y$ be a semialgebraic target, $\mathcal{Z}(Y)$ is a semi-linear set.

Theorem 5 essentially completes the proof of Theorem 2. It is almost immediate that the characteristic word is eventually periodic (see Lemma 10 in the appendix for a formal proof) and thus the model-checking problem can be decided by checking $A \cap \bar{B} = \emptyset$, where $A$ is an automaton representing the characteristic word and $B$ encodes the language of $\phi$.

It is standard that semi-linear sets are closed under intersection, union, and complementation (see [14] for a nice introduction to semi-linear sets). Thus in order to express the hitting set of $\mathcal{Z}(Y)$ it is sufficient to express the hitting set of $\{(x_1, \dots, x_d) \mid P_{ij}(x_1, \dots, x_n) \ge 0\}$. Conjunction is found by taking the intersection of the hitting sets, and disjunction by taking union. The hitting set of $P(x_1, \dots, x_n) > 0$ can be rewritten as the complement of the hitting set of $-P(x_1, \dots, x_n) \ge 0$. The hitting set of $P(x_1, \dots, x_n) = 0$ is the conjunction (intersection) of $P(x_1, \dots, x_n) \ge 0$ and $-P(x_1, \dots, x_n) \ge 0$. Therefore Theorem 5 is a consequence of the following lemma.

**Lemma 9.** Assume $x^{(t)} = (z_1^{(t)}, \dots, z_d^{(t)})_{i=1}^{\infty}$, is a pseudo-periodic sequence with start point $N$, period $T$ and growth rates $\alpha_1, \dots, \alpha_n$ and $P \in \mathbb{Q}[x_1, \dots, x_d]$ a rational polynomial in $d$ variables$^7$. Then, $\{i \in \mathbb{N} \mid P(z_1^{(t)}, \dots, z_d^{(t)}) \ge 0\}$ is a semi-linear set.

<footnote n="7">⁷ Some variables may be redundant; if the polynomial does not depend on all dimensions of $x^{(t)}$ then some of the variables may not appear in $P$.</footnote>
*Proof.* First, we show that pseudo-periodicity is closed under product. Suppose $x_i^{(N+Tn)} = m_i 10^{\beta_i + \alpha_i \cdot n}$ and $x_j^{(N+Tn)} = m_j 10^{\beta_j + \alpha_j \cdot n}$. Observe that $x_i^{(N+Tn)} \cdot x_j^{(N+Tn)} = m_i \cdot m_j \cdot 10^{\beta_i + \alpha_i \cdot n} \cdot 10^{\beta_j + \alpha_j \cdot n} = m_i m_j \cdot 10^{\beta_i + \beta_j + n(\alpha_i + \alpha_j)}$. We conclude that the vector $(x_i \cdot x_j)^{(t)}$ is pseudo-periodic with growth rate $\alpha_i + \alpha_j$. Observe that the mantissa precision increase by at most 2.

Secondly, we show that if two pseudo-periodic sequences have the same growth rate, then their sum is also pseudo-periodic with the same growth rate. Suppose $x_i^{(N+Tn)} = m_i 10^{\beta_i + \alpha_i \cdot n}$, and $x_j^{(N+Tn)} = m_j 10^{\beta_j + \alpha_j \cdot n}$. Observe that $(x_i + x_j)^{(N+Tn)} = m_i 10^{\beta_i + \alpha_i \cdot n} + m_j 10^{\beta_j + \alpha_j \cdot n} = (m_i + m_j \cdot 10^{\beta_j - \beta_i}) 10^{\beta_i + \alpha_i \cdot n}$. Observe that the mantissa precision increased by at most $10^{|\beta_j - \beta_i|}$.

Let $P(x_1, \dots, x_n) = \sum_{i=1}^N c_i Z_i$, where $Z_i$ is a product of $x_1, \dots, x_n$. Consider each monomial $Z_i$ occurring in $P$, since produce preserves pseudo-periodicity, we conclude that $Z_i$ is pseudo-periodic. $P^{(t)}$ is thus a linear combination of these pseudo-periodic vectors. Note our prior observation does not immediately imply that $P^{(t)}$ is pseudo-periodic as we required that we took the sum of elements with the same growth rate. However, from some point on, we are only interested in those with the maximal growth rate.

Without loss of generality, let $Z_1, \dots, Z_r$ have the maximum-growth rate, and $Z_{r+1}, \dots, Z_N$ have strictly smaller growth rate. For every $L \in \mathbb{N}$ there exists $N \in \mathbb{N}$ such that for all $t > N$, $\text{exponent}(Z_1^{(t)}) - \text{exponent}(Z_{r+1}^{(t)}) > L$.

Hence there exists $N \in \mathbb{N}$ such that for all $t > N$ if $\sum_{i=1}^r c_i Z_i > 0$ if and only if $\sum_{i=1}^N c_i Z_i = \sum_{i=1}^r c_i Z_i + \sum_{i=r+1}^N c_i Z_i > 0$ because $|\sum_{i=r+1}^N c_i Z_i| < |\sum_{i=1}^r c_i Z_i|$ from some point on. Hence $\text{sign}(\sum_{i=1}^N c_i Z_i^{(t)}) = \text{sign}(\sum_{i=1}^r c_i Z_i^{(t)})$.

Thus we restrict our attention to $\sum_{i=1}^r c_i Z_i^{(t)}$. Since each of the $Z_i$ for $i \in \{1, \dots, r\}$ have the same growth rate, we know that $\sum_{i=1}^r c_i Z_i^{(t)}$ is pseudo-periodic. Since $\text{sign}(\sum_{i=1}^r c_i Z_i^{(t)})$ does not depend on the exponent, only the periodic mantissa, we have that the sign is periodic. The hitting times for $t \le N$ can be determined exhaustively and included in the finite set of the semi-linear set. $\square$

## References

1. Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive verification of floating-point java programs in key. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Part of ETAPS 2021. Part II. Lecture Notes in Computer Science, vol. 12652, pp. 242–261. Springer (2021). https://doi.org/10.1007/978-3-030-72013-1_13

2. Akshay, S., Antonopoulos, T., Ouaknine, J., Worrell, J.: Reachability problems for Markov chains. Inf. Process. Lett. 115(2), 155–158 (2015). https://doi.org/10.1016/j.ipl.2014.08.013

3. Akshay, S., Bazille, H., Genest, B., Vahanwala, M.: On robustness for the Skolem and Positivity problems. In: Berenbrink, P., Monmege, B. (eds.) 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022. LIPIcs,
vol. 219, pp. 5:1–5:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022).
https://doi.org/10.4230/LIPIcs.STACS.2022.5

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). https://doi.org/10.1145/3434329

5. Baier, C., Funke, F., Jantsch, S., Karimov, T., Lefaucheux, E., Ouaknine, J., Pouly, A., Purser, D., Whiteland, M.A.: Reachability in dynamical systems with rounding. In: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020. LIPIcs, vol. 182, pp. 36:1–36:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.FSTTCS.2020.36

6. Baier, C., Funke, F., Jantsch, S., Karimov, T., Lefaucheux, E., Ouaknine, J., Purser, D., Whiteland, M.A., Worrell, J.: Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 243, pp. 10:1–10:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022). https://doi.org/10.4230/LIPIcs.CONCUR.2022.10

7. Becker, H., Panchekha, P., Darulova, E., Tatlock, Z.: Combining tools for optimization and analysis of floating-point computations. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E.P. (eds.) Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018. Lecture Notes in Computer Science, vol. 10951, pp. 355–363. Springer (2018). https://doi.org/10.1007/978-3-319-95582-7_21

8. 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. LIPIcs, vol. 241, pp. 20:1–20:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.MFCS.2022.20

9. Boyle, M.: Notes on the perron-frobenius theory of nonnegative matrices (2005)

10. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: The collected works of J. Richard Büchi, pp. 425–435. Springer (1990)

11. Chonev, V., Ouaknine, J., Worrell, J.: On the complexity of the orbit problem. J. ACM 63(3), 23:1–23:18 (2016). https://doi.org/10.1145/2857050

12. 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. LIPIcs, vol. 202, pp. 34:1–34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.MFCS.2021.34

13. 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. LIPIcs, vol. 241, pp. 40:1–40:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.MFCS.2022.40

14. Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News 5(3), 67–82 (2018). https://doi.org/10.1145/3242953.3242964

15. Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808–821 (1986). https://doi.org/10.1145/6490.6496
16. Karimov, T., Lefauchez, 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). https://doi.org/10.1145/3498727

17. Lohar, D., Jeangoudoux, C., Sobel, J., Darulova, E., Christakis, M.: A two-phase approach for conditional floating-point verification. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Part of ETAPS 2021. Part II. Lecture Notes in Computer Science, vol. 12652, pp. 43–63. Springer (2021). https://doi.org/10.1007/978-3-030-72013-1_3

18. 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. Lecture Notes in Computer Science, vol. 13465, pp. 3–15. Springer (2022). https://doi.org/10.1007/978-3-031-15839-1_1

19. Maurica, F., Mesnard, F., Payet, E.: Optimal approximation for efficient termination analysis of floating-point loops. In: 2017 1st International Conference on Next Generation Computing Applications (NextComp). pp. 17–22. IEEE (2017)

20. Minsky, M.L.: Computation. Prentice-Hall Englewood Cliffs (1967)

21. Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Chekuri, C. (ed.) Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014. pp. 366–379. SIAM (2014). https://doi.org/10.1137/1.9781611973402.27

22. Schneider, H.: Wielandt’s proof of the exponent inequality for primitive nonnegative matrices. Linear Algebra and its Applications 353(1), 5–10 (2002)

## A Undecidability of point-to-point reachability

In this section we show that, in general, Problem 2 (and thus Problem 1) is undecidable.

**Theorem 1.** *The floating-point point-to-point reachability problem is undecidable.*

We reduce the halting of a two-counter Minsky machine to the point-to-point reachability problem. We recall here the definition of this model:

**Definition 3.** *A two-counter Minsky machine is defined by a finite set of states $\ell_1, \dots, \ell_m$, a distinguished starting state (w.l.o.g. $\ell_1$), a distinguished halting state (w.l.o.g. $\ell_m$), two natural integer counters, here denoted as $x$ and $y$, and a mapping deterministically associating to each state transition.*

*Each transition takes one of the following forms: for $z \in \{x, y\}$,*

*increment* $\text{inc}_z(\ell_j)$: add 1 to counter $z$, move to state $\ell_j$.

*decrement* $\text{dec}_z(\ell_j)$: remove 1 from counter $z$ if $z > 0$, move to state $\ell_j$.

*zero test* $\text{zero}_z(\ell_j, \ell_k)$: if $z = 0$ move to state $\ell_j$ else move to state $\ell_k$.

*The configuration of a two-counter Minsky machine consists of the current state and the values of $x$ and $y$.*
Without loss of generality (by first using a zero test), one can assume a decre-
ment operation is never used in a configuration where the would-be decreased
counter has value 0, hence removing the need to check whether $z > 0$.

The halting problem asks whether, starting in configuration $(\ell_1, 0, 0)$, that is, in the distinguished starting state with both counters set to 0, whether the state $\ell_m$ is reached. The problem is undecidable [20].

We describe below the construction of an LDS with mantissa length $p = 1$ and base 10 that will emulate a run of this machine. In particular, our reduction will maintain that the mantissa always has the value 0 or 1 after rounding (although, as we operate in base 10, there are 10 possible values the mantissa could have taken)$^8$. For ease of readability, we describe the LDS using variables to represent the dimensions and linear functions to represent the transition matrix.

In order to describe our proof we introduce two filter functions which will
help us encode control flow. The function filter_+(u, v) (resp. filter_-(u, v)) is equal
to v if v ≥ u (resp. v < u) and to 0 otherwise. The two following results are
shown in Section 3.

**Lemma 1.** *Given u, v of the form 10<sup>c</sup> with c ∈ N, one can compute the value w = filter<sub>+</sub>(u, v) in three linear operations with floating-point rounding.*

**Corollary 1.** *Given u, v of the form 10<sup>c</sup> with c ∈ N, one can compute the value w = filter<sub>-</sub>(u, v) in four linear operations with floating-point rounding.*

We now show the encoding of the two-counter machine into a linear dynami-
cal system with rounding using the defined filter functions, entailing Theorem 1.

*Proof (Proof of Theorem 1).*

First, for each state $\ell_j$ of the Minsky machine, we build variables $x_j, y_j$, and $a_j$, which will have the following invariant property: when the run of the Minsky machine reaches a configuration $(\ell_j, x, y)$, then in the corresponding run of the LDS we will have that $x_j = 10^x, y_j = 10^y$ and $a_j = 10^{x+y}$. Moreover, for all $k \neq j$, $x_k = y_k = a_k = 0$.

Assuming the variable $\alpha_k$ corresponds to dimension $k$ in the LDS, setting
$\alpha_i \leftarrow \sum_k a_k \cdot \alpha_k$ means that $M_{i,k} = a_k$. Any entries which are not specified are
assumed to be zero. When describing update transitions, we also want to use
the filter operations. Since these operations represent up to four linear steps,
we create four copies of each variable as well as temporary variables (*temp
and *temp2*) for each state of the Minsky machine. These copies and temporary
variables are used implicitly: we only describe here the updates of the primary
variable; the updates of the secondary variables can be deduced from Lemma 1
and Corollary 1. Moreover, if an update function takes fewer than four steps, we
complete it with updates that pass the value to the next secondary variable in
order for every update to take exactly four steps.

Let us now define the update functions of the primary variables of the system.

<footnote n="8">⁸ Technically we define floating-point numbers with mantissa in {0} ∪ [0.1, 1). For convenience, throughout this section we write 1 · 10ᶜ (or simply 10ᶜ) instead of 0.1 · 10ᶜ⁺¹.</footnote>
- if the transition in $\ell_i$ is an increment, $\text{inc}_z(\ell_j)$, then we multiply by 10 the variables to keep the invariant on the variables and move the values to the next instruction. For instance, if $x$ is increased, we set $x_j \leftarrow 10 \cdot x_i$, $y_j \leftarrow y_i$, and $a_j \leftarrow 10 \cdot a_i$.

- if the transition in $\ell_i$ is a decrement, $\text{dec}_z(\ell_j)$ then conversely to incrementation, we divide the variables by 10 to keep the invariant on the variables and move the values to the next instruction, we set $x_j \leftarrow 10^{-1} \cdot x_i$, $y_j \leftarrow y_i$, and $a_j \leftarrow 10^{-1} \cdot a_i$.

- if the transition in $\ell_i$ is a zero test of $z$, zero?$_z(\ell_j, \ell_k)$, we need to copy the values of our variables only to the correct coordinate. For that, we need a way to filter their values, depending on the zeroness of $z$. Assume the test is on $x$ without loss of generality. We define the following operations:

• $x_j \leftarrow \text{filter}_-(10, x_i)$,

• $x_k \leftarrow \text{filter}_+(10, x_i)$,

• $y_j \leftarrow \text{filter}_+(a_i, y_i)$,

• $y_k \leftarrow \text{filter}_-(a_i, y_i)$,

• $a_j \leftarrow \text{filter}_-(10 \cdot y_i, a_i)$

• $a_k \leftarrow \text{filter}_+(10 \cdot y_i, a_i)$.

One can check that the $j$ variables are assigned the values from the $i$ variables if and only if $x = 0$ (and thus $x_i = 10^0$ and $a_j = y_j$), and the $k$ variables are assigned the values in the opposite case.

- if the state is $\ell_m$ we zero the system: the values of the counters received in $x_m, y_m$ and the test value $a_m$ are discarded on the next step, thus making every value of the system equal to 0.

We have that the Minsky machine terminates if and only if the LDS described by the above behaviour, starting with $x_1 = y_1 = a_1 = 1$ (and everything else at 0) eventually hits the zero vector.

This equivalence is a direct result of the invariant kept within the construction on the variables $x_j$ and $y_j$. Indeed, if the Minsky machine terminates, then following the same path the LDS we constructed puts all the stored values in $a_m, x_m, y_m$ associated to the terminating state $\ell_m$, thus discarding them and reaching the zero vector in the next step. And reciprocally, the zero vector can only be reached by discarding the stored variables thanks to a halting instruction, proving halting of the Minsky machine.

Hence, point-to-point reachability is undecidable for LDS under floating-point rounding. □

This proof, and in particular the construction of the filter functions rely on the use of base 10. It works as well for most other bases. A notable exception is base 2 as the gap between $2^c$ and $2^{c+1}$ is not large enough for the rounding functions to operate correctly. It's possible however to artificially widen this gap by storing the value of the counter $x$ for instance as $2^{2x}$ instead of $2^x$ in the variables of the LDS. With the guarantee that the exponent is even, the filter functions, and the rest of the proof, work in base 2 as well.
## B Proof of Proposition 1

**Proposition 1.** Let $x, x' \in \mathbb{F}_{10}[p]$ be non-zero floating-point numbers.

(1) If $x \approx_{\delta} x'$ then $10^{-\delta-1} \le x/x' \le 10^{\delta+1}$.

(2) If $10^{-\delta} \le x/x' \le 10^{\delta}$ then $x \approx_{\delta+2} x'$.

(3) If $x \approx_{\delta} x'$ and $x' \approx_{\eta} x''$ then $x \approx_{\delta+\eta+4} x''$.

*Proof.*

(1) Let $x = q_1 10^{\alpha}, x' = q_2 10^{\beta}$, with $|\alpha - \beta| \le \delta$ and $q_1$ and $q_2$ are non-zero mantissa with $p$ decimals. Then, $10^{-p} \le \frac{q_1}{q_2} \le 10^p$.

Hence $\frac{x}{x'} = \frac{q_1 10^{\alpha}}{q_2 10^{\beta}} \le \frac{q_1 10^{\beta+\delta}}{q_2 10^{\beta}} \le \frac{10^{\delta}}{0.1^p} \le 10^{\delta+1}$.

And $\frac{x}{x'} = \frac{q_1 10^{\alpha}}{q_2 10^{\beta}} \ge \frac{q_1 10^{\alpha}}{q_2 10^{\alpha-\delta}} \ge \frac{0.1^p}{0.1 \cdot 10^{\delta}} \ge 10^{-\delta-1}$.

(2) Let $x = q_1 10^{\alpha}, x' = q_2 10^{\beta}$, with $10^{-\delta} \le x/x' \le 10^{\delta}$.

Then $\frac{0.1 \cdot 10^{\alpha}}{10^{\beta}} \le \frac{q_1 10^{\alpha}}{q_2 10^{\beta}} = \frac{x}{x'} \le 10^{\delta}$, so $10^{\alpha-\beta} \le 10^{\delta+1} < 10^{\delta+2}$

and $\frac{10^{\alpha}}{0.1 \cdot 10^{\beta}} \ge \frac{q_1 10^{\alpha}}{q_2 10^{\beta}} = \frac{x}{x'} \ge 10^{-\delta}$, so $10^{\alpha-\beta} \ge 10^{-\delta-1} > 10^{-\delta-2}$.

(3) If $x \approx_{\delta} x'$ and $x' \approx_{\eta} x''$ then $\frac{x}{x'} \le 10^{\delta+1}$ and $\frac{x'}{x''} \le 10^{\eta+1}$ by (1). Hence $\frac{x}{x''} \le 10^{\delta+\eta+2}$ and similarly $\frac{x'}{x} \le 10^{\delta+\eta+2}$. Hence by (2) we have $x \approx_{\delta+\eta+2+\delta} x''$. $\square$

## C Proof of Lemma 5

**Lemma 5.** There exists $\eta, N' \in \mathbb{N}$, such that for all $(q, i), (q', i) \in S_{me}$, all $t \ge N'$ and all $i \in \{0, \dots, P-1\}$ then

- if $t \not\equiv i \pmod{P}$, then $x_{(q,i)}^{(t)} = 0$,

- otherwise, $x_{(q,i)}^{(t)} \approx_{\eta} x_{(q',i)}^{(t)}$.

*Proof.* Let $C$ be such that $(M^C)_{S_{me}, S_F}$ and $(M^C)_{S_{me}}$ is positive (i.e. there is a path in the graph associated to $M$ from each element of $S_{me} \cup S_F$ to each element of $S_{me}$). This integer exists as, from Lemma 2, there exists $C_i$ and $C_0$ such that $M_{F_i}^{C_i}$ and $M_{S_{me}}^{C_0}$ are positive. As the SCC $F_i$ feeds $S_{me}$, the $M_{S_{me}, F_i}$ are non-zero non-negative matrices, and in particular, there is a path of length $C_i + C_0 + 1$ (corresponding to the an element of $M_{S_{me}}^{C_0} M_{S_{me}, F_i} M_{F_i}^{C_i}$) between any state of $F_i \cup S_{me}$ to any state of $S_{me}$. Setting $C$ as the product of $C_0$ and of the $C_0 + C_i + 1$, we have that there is a path of length $C$ between any state of $S_F \cup S_{me}$ to any state of $S_{me}$.

Recall that $m$ is a constant larger than all entries of $M$ and $\frac{1}{m}$ is smaller than all non-zero entries of $M$. Recall $c$ is the constant such that $[\cdot]$ is log-bounded. Let $d$ be $|S_F \cup S_{me}|$.
Let us bound the effect of C steps, first from above, for all $u \in S_{me}$, we have:

$$
\begin{align*}
x_{(q,i)}^{(t+C)} &= \left[ \sum_{r \in S_F \cup S_{me}} M_{(q,i),(r,i-1)} x_{(r,i-1)}^{(t+C-1)} \right] \\
&\leq mcd \max_{(r,i-1):M_{(q,i),(r,i-1)}>0} x_{(r,i-1)}^{(t+C-1)} \\
&\leq (mcd)^2 \max_{(q,i-2):M_{(q,i),(r,i-2)}^2}>0} x_{(r,i-2)}^{(t+C-2)} \\
&\leq \dots \leq (mcd)^C \max_{(r,i):M_{(q,i),(r,i)}^C}>0} x_{(r,i)}^{(t)} \quad (i \equiv i + C \mod P) \\
&= (mcd)^C \max_{(r,i) \in S_F \cup S_{me}} x_{(r,i)}^{(t)}
\end{align*}
$$

Similarly, bounding from below, for all $u \in S_{me}$, we have:

$$
\begin{align*}
x_{(q,i)}^{(t+C)} &\ge \frac{1}{mc} \max_{(r,i-1):M_{(q,i),(r,i-1)}>0} x_{(r,i-1)}^{(t+C-1)} \\
&\ge \frac{1}{(mc)^2} \max_{(r,i-2):M_{(q,i),(r,i-1)}^2}>0} x_{(r,i-2)}^{(t+C-2)} \\
&\ge \dots \ge \frac{1}{(mc)^C} \max_{(r,i):M_{(q,i),(r,i)}^C}>0} x_{(r,i)}^{(t)} \quad (i \equiv i + C \mod P) \\
&= \frac{1}{(mc)^C} \max_{(r,i) \in S_F \cup S_{me}} x_{(r,i)}^{(t)}
\end{align*}
$$

Finally we observe that for all $(q, i)$, $(q', i) \in S_{me}$ and $t \ge N + C$ we have

$$
\frac{x_{(q,i)}^{(t+C)}}{x_{(q',i)}^{(t+C)}} \le \frac{(mcd)^C \max_{(r,i) \in S_F \cup S_{me}} x_{(r,i)}^{(t)}}{\frac{1}{(mc)^C} \max_{(r,i) \in S_F \cup S_{me}} x_{(r,i)}^{(t)}} = (mc)^{2C} d^C.
$$

Hence, by Proposition 1, we can select $\eta = [\log (mc)^{2C} d^C] + 2$ and $N = C$. $\square$

D Proof of Proposition 2

**Proposition 2.** If a sequence of non-zero floating-point vectors $(v^{(t)})_{t \in \mathbb{N}}$ is pseudo-periodic with the same growth rate within a set $Q$, then there exists $\delta$ such that for all $q, q' \in Q$ and all $t \ge N$, $v_q^{(t)} \approx_{\delta} v_{q'}^{(t)}$.

*Proof.* For $t \ge N$ a pseudo-periodic vector can be expressed as $v_q^{(t)} = m_q^{(t)} 10^{\alpha_q^{(t)} + \gamma^{(t)}}$, where $m_q^{(t)}$ is periodic and comes from the finite set of mantissas expressible with $p$ digits, $\alpha_q^{(t)}$ is periodic and $\gamma^{(t)}$ comes from the growth rate and thus does not depend on $q$.
Thus at any given time step we have $\frac{v_q^{(t)}}{v_{q'}^{(t)}} = \frac{m_q^{(t)} 10^{\alpha_q^{(t)} + \gamma^{(t)}}}{m_{q'}^{(t)} 10^{\alpha_{q'}^{(t)} + \gamma^{(t)}}} = \frac{m_q^{(t)} 10^{\alpha_q^{(t)}}}{m_{q'}^{(t)} 10^{\alpha_{q'}^{(t)}}}$. Since each of $m_q, m_{q'}, \alpha_q, \alpha_{q'}$ comes from a finite set of attainable values, the ratio has a maximum $D$ as both $v_q^{(t)}, v_{q'}^{(t)}$ are non-zero. Hence $v_q^{(t)} \approx_{\delta} v_{q'}^{(t)}$ for $\delta = \lceil \log_{10}(D) \rceil + 2$. $\square$

## E Proof of Lemma 6

**Lemma 6.** There exists $\beta, N \in \mathbb{N}$ such that:

For $t \ge N$ and $(q, i) \in S_{me}$, if $x_{(q,i)}^{(t)}$ is influenced by $(q', i - 1) \in S_F$, then
$$x_{(r,i)}^{(t)} \approx_{\beta} x_{(r',i)}^{(t)} \text{ for all } (r,i), (r',i) \in S_{me} \cup S_F.$$

*Proof.* Note that if $(r, i), (r', i) \in S_{me}$ and $(r, i), (r', i) \in S_F$ then the claim follows from Lemma 5 and Proposition 2 (applied on the sequence of values in the non-zero phase) respectively.

Assume now that $(r, i) \in S_{me}$ and $(r', i) \in S_F$, we show that the claim follows by 'transitivity' of the closeness property (property (3) of Proposition 1), due to the closeness within $S_F$ and $S_{me}$, as well as the closeness implied by the interference.

More formally,

- By Proposition 2, as $S_F$ is pseudo-periodic there exists $\delta$ such that for all $t \in \mathbb{N}$, $(v, i), (v', i) \in S_F$, $x_{(v,i)}^{(t)} \approx_{\delta} x_{(v',i)}^{(t)}$.

In particular $x_{(r',i)}^{(t)} \approx_{\delta} x_{(v,i)}^{(t)}$ for all $(v, i) \in S_F$.

- By Lemma 5, there exists $\eta$ and $K$ such that for all $t \ge K$, $(s, i), (s', i) \in S_{me}$, $x_{(s,i)}^{(t)} \approx_{\eta} x_{(s',i)}^{(t)}$.

In particular $x_{(r,i)}^{(t)} \approx_{\eta} x_{(s,i)}^{(t)}$ for all $(s, i) \in S_{me}$.

- Let $t \ge 1$, if $x_{(q,i)}^{(t)}$ is influenced by $(q', i - 1)$, then $\frac{1}{m} \le \frac{x_{(q,i)}^{(t)}}{x_{(q',i-1)}^{(t)}} \le 2m10^p$.

Moreover, as seen in the proof of Lemma 3, $\frac{1}{mc10^{\delta+1}} \le \frac{x_{(v,i)}^{(t)}}{x_{(q',i-1)}^{(t)}} \le mcd10^{\delta+1}$ for some $(v, i) \in S_F$ such that $M_{(v,i),(u,i-q)} > 0$. Thus $\frac{1}{m^2c10^{\delta+1}} \le \frac{x_{(q,i)}^{(t)}}{x_{(v,i)}^{(t)}} \le 2m^2cd10^{p+\delta+1}$

Therefore, by setting $\zeta = \lceil \log_{10}(2m^2cd) \rceil + p + \delta + 3$, by property (2) of Proposition 1 we have $x_{(v,i)}^{(t)} \approx_{\zeta} x_{(q,i)}^{(t)}$ for $(q, i) \in S_{me}$ and $(v, i) \in S_F$.

Thus we have $x_{(r,i)}^{(t)} \approx_{\eta} x_{(q,i)}^{(t)} \approx_{\zeta} x_{(v,i)}^{(t)} \approx_{\delta} x_{(r',i)}^{(t)}$ and by property (3) of Proposition 1 we have $x_{(r,i)}^{(t)} \approx_{\delta+\eta+\zeta+8} x_{(r',i)}^{(t)}$. Thus, the claim holds for $\beta = \delta+\eta+\zeta+12$ and $N = K$. $\square$
## F Proof of Lemma 8

**Lemma 8.** Let $\beta, N$ be defined as in Lemma 6. If $t \ge N$ then it is decidable whether there exists $t' > t$ such that $x_{S_F}^{(t')} \approx \beta x_{S_{me}}^{(t')}.$

*Proof.* Define a new dynamical system $(M_{S_{me}}, y)$ such that $y = x_{S_{me}}^{(t)}$, with orbit $y^{(t)}$. The vector $y$ evolves without the influence of $S_F$. Since $y^{(t)}$ consists of a single strongly connected, then it is effectively pseudo-periodic, with starting point $N_y$, period $T_y$ and growth rate $\alpha_y$ for every $q \in S_{me}$.

We consider two cases:

First, suppose $y^{(t')} \neq x_{S_{me}}^{(t+t')}$ for $t' \le N_y + T \cdot T_y$. Then clearly a value of $x_{S_F}$ influenced the value of $x_{S_{me}}$, and so they must have been close for some $t'$ and we're done.

Secondly, suppose $y^{(t')} = x_{S_{me}}^{(t+t')}$ for $t' \le N_y + T \cdot T_y$ then both $S_F$ and $S_{me}$ completed a synchronised pseudo-period in which they did not interact. We now inspect the increase rate to see if they are converging, so that they will interact in the future, or diverging, so that they will not interact in the future. This implies that we can detect within $K = N_y + T \cdot T_y$ steps whether $x_{S_F}^{(t')}$ is close to $x_{S_{me}}^{(t')}$ again. Note that this does entail that $t' \le t + K$ steps as it will take time for the convergence entailed by the growth rates bring them together.

We now analyse the number of steps require until they are close. Consider two states $q \in S_F$ and $q' \in S_{me}$, we have observed that within the first $K$ steps used to determine they will be close again. The two systems can diverge by at most $10^\beta d(mc)^{2K_1}$ in this time (supposing one grows maximally and one reduces maximally at every step). Hence $(x_{S_F}^{(t+K_1)})_q \approx \tau (x_{S_{me}}^{(t+K)})_{q'}$, where $\tau \le \lceil \log 10^p 10^\beta d(mc)^{2K} \rceil$.

Observe we have exponent$((x_{S_{me}}^{(t+K)})_{q'}) > exponent((x_{S_F}^{(t+K)})_q)$, otherwise $S_F$ would influence $S_{me}$.

By the increase rate of $(x_{S_{me}}^{(t)})_{q'}$, every $T_y$ steps, the exponent changes by $\alpha_y$, that is, exponent$((x_{S_{me}}^{(t+T_y)})_{q'}) = exponent((x_{S_{me}}^{(t)})_{q'}) + \alpha_y$.

Similarly by the increase rate of $(x_{S_F}^{(t)})_q$, every $T$ steps, the exponent changes by $\alpha$, that is, exponent$((x_{S_F}^{(t+T)})_q) = exponent((x_{S_F}^{(t+T)})_q) + \alpha$.

We observe that exponents become closer at least every $T \cdot T_y$ steps:

$$ \begin{aligned} \operatorname{exponent}((x_{S_{me}}^{(t+T \cdot T_y)})_{q'}) - \operatorname{exponent}((x_{S_F}^{(t+T \cdot T_y)})_q) & \\ & = \operatorname{exponent}((x_{S_{me}}^{(t)})_{q'}) + \alpha_y T - \operatorname{exponent}((x_{S_F}^{(t)})_q) - \alpha T_y \\ & = \operatorname{exponent}((x_{S_{me}}^{(t)})_{q'}) - \operatorname{exponent}((x_{S_F}^{(t)})_q) + \alpha_y T - \alpha T_y \\ & < \operatorname{exponent}((x_{S_{me}}^{(t)})_{q'}) - \operatorname{exponent}((x_{S_F}^{(t)})_q). \end{aligned} $$

The final inequality is because $\frac{\alpha_y}{T_y} < \frac{\alpha}{T}$ by the assumption that the exponents are converging. Since the difference reduces by at least one every $T \cdot T_y$ steps, we have exponent$((x_{S_{me}}^{(t+K)})_{q'}) - exponent((x_{S_{me}}^{(t+K)})_{q'}) \le p$ within $\tau \cdot T \cdot T_y$ steps.
Hence if there exists $t'$ such that $x_{S_F}^{(t')} \approx_{\beta} x_{S_{me}}^{(t')}$, there exists $t' \le t+K+\tau \cdot T \cdot T_y$. $\square$

## G Proof of Lemma 10

**Lemma 10.** Let $Y_1, \dots, Y_k$ be sets such that $\mathcal{Z}(Y_i)$ is semi-linear for each $1 \le i \le k$. The characteristic word is eventually periodic.

*Proof.* We show that the characteristic word is eventually periodic. Recall that the alphabet of $w$ is $2^{\{1,\dots,k\}}$.

Let $S \subseteq \{1, \dots, k\}$. By Theorem 5, since each $\mathcal{Z}(Y_i)$ is semi-linear, observe that the set $C_S = \{i \mid w_i = S\} = \bigcap_{i \in S} \mathcal{Z}(Y_i) \setminus \bigcup_{i \notin S} \mathcal{Z}(Y_i)$ is semi-linear. Let $F_S$ be the finite set of $C_S$ and $p_S$ be the common period of its linear-sets. Let $F = \max \bigcup_{S \subseteq \{1, \dots, k\}} F_S$ and $p = \text{lcm}_{S \subseteq \{1, \dots, k\}} p_S$.

The word $w$ can thus be represented using an automaton with a finite initial segment of length $F$ and a cycle of length $p$. In the finite initial segment, the $i$th transition is uniquely labelled by the set $S$ such that $i \in C_S$. The $j$th character of the cycle is uniquely labelled by the unique $S$ such that $F + j \in C_S$. $\square$