A fundamental question in logic and verification is the following: for which unary predicates P_1, …, P_k is the monadic second-order theory of ⟨ℕ;<,P_1,…,P_k⟩ decidable? Equivalently, for which infinite words α can we decide whether a given Büchi automaton 𝒜 accepts α? Carton and Thomas showed decidability in the case that α is a fixed point of a letter-to-word substitution σ, i.e., σ(α) = α. However, abundantly more words, e.g., Sturmian words, are characterised by a broader notion of self-similarity that involves a set S of substitutions. A word α is said to be directed by a sequence s = (σ_n)_{n ∈ ℕ} over S if there is a sequence of words (α_n)_{n ∈ ℕ} such that α₀ = α and α_n = σ_n(α_{n+1}) for all n; such α are called S-adic. We study the automaton acceptance problem for such words and prove, among others, the following: given finite S and an automaton 𝒜, we can compute an automaton ℬ that accepts s ∈ S^ω if and only if s directs a word α accepted by 𝒜. Thus we can algorithmically answer questions of the form "Which S-adic words are accepted by a given automaton 𝒜?"

A discrete-time linear dynamical system (LDS) is given by an update matrix M ∈ ℝ^{d× d}, and has the trajectories ⟨s, Ms, M²s, …⟩ for s ∈ ℝ^d. Reachability-type decision problems of linear dynamical systems, most notably the Skolem Problem, lie at the forefront of decidability: typically, sound and complete algorithms are known only in low dimensions, and these rely on sophisticated tools from number theory and Diophantine approximation. Recently, however, o-minimality has emerged as a counterpoint to these number-theoretic tools that allows us to decide certain modifications of the classical problems of LDS without any dimension restrictions. In this paper, we first introduce the Decomposition Method, a framework that captures all applications of o-minimality to decision problems of LDS that are currently known to us. We then use the Decomposition Method to show decidability of the Robust Safety Problem (restricted to bounded initial sets) in arbitrary dimension: given a matrix M, a bounded semialgebraic set S of initial points, and a semialgebraic set T of unsafe points, it is decidable whether there exists ε > 0 such that all orbits that begin in the ε-ball around S avoid T.

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

We consider reachability problems for linear dynamical systems. In dimension d these problems are specified by respective semialgebraic sets S, T ⊆ ℝdof source and target states and a matrix $M \in {\mathbb{Q}^{d \times d}}$. The task is to determine whether there is a point in S whose orbit under M intersects the target T in at least m distinct points. The case m = 1 (mere reachability) can be reduced to mild generalisations of the Skolem and Positivity Problems for linear recurrence sequences, whose decidability has been open for many decades. The situation is markedly different for multiple reachability, where m can be greater than one. In this paper, we prove that multiple reachability is undecidable already in dimension d = 10 with fixed multiplicity m = 9. Since our undecidability construction also shows that decision procedures for dimension d ∈ {3, … , 9} would entail significant new results on effective solutions of Diophantine equations, we subsequently focus on the case d = 2, that is, multiple reachability in the plane. Here we obtain two positive results. We show that multiple reachability is decidable if the matrix M is a rotation and it is also decidable without restriction on M for halfplane targets. The former result relies on a theorem in arithmetic geometry, due to Bombieri and Zannier, concerning intersections of algebraic subgroups with subvarieties.

We prove that for any integers α, β > 1, the existential fragment of the first-order theory of the structure ⟨ℤ; 0,1,<, +,αℕ,ßℕ⟩ is decidable (where αℕ is the set of positive integer powers of α, and likewise for βℕ). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of ⟨ℕ; 0,1,<, +,x ↦ αx,x ↦ βχ⟩ for any multiplicatively independent α, β > 1 would lead to mathematical breakthroughs regarding base-α and base-β expansions of certain transcendental numbers. Finally, modifying the original proof of Hieronymi and Schulz we show that for any multiplicatively independent α, β > 1, it is undecidable whether a given formula with at most 3 alternating blocks of quantifiers holds in ⟨ℕ;0,1,<, +,αℕ,ßℕ⟩.

For which unary predicates P 1 , … , P m is the MSO theory of the structure 〈 N ; < , P 1 , … , P m 〉 decidable? We survey the state of the art, leading us to investigate combinatorial properties of almost-periodic, morphic, and toric words. In doing so, we show that if each P i can be generated by a toric dynamical system of a certain kind, then the attendant MSO theory is decidable. We give various applications of toric words, including the recent result of [1] that the MSO theory of 〈 N ; < , { 2 n : n ∈ N } , { 3 n : n ∈ N } 〉 is decidable.

In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.

We investigate the decidability of the monadic second-order (MSO) theory of the structure (N; <, P1,…,Pk), for various unary predicates P1,…,Pk ⊆ N. We focus in particular on 'arithmetic' predicates arising in the study of linear recurrence sequences, such as fixed-base powers Powk = {kn : n ∈ N}, k-th powers Nk = {nk : n ∈ N}, and the set of terms of the Fibonacci sequence Fib = {0, 1, 2, 3, 5, 8, 13,…} (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:

The Positivity Problem for linear recurrence sequences over a ring R of real algebraic numbers is to determine, given an LRS ${\left( {{u_n}} \right)_{n \in \mathbb{N}}}$ over R, whether un≥ 0 for all n. It is known to be Turing-equivalent to the following reachability problem: given a linear dynamical system (M, s) Rd×d×Rdand a halfspace H ⊆ ℝd, determine whether the orbit ${\left( {{M^n}s} \right)_{n \in \mathbb{N}}}$ ever enters H. The more general model-checking problem for LDS is to determine, given (M, s) and an ω-regular property φ over semialgebraic predicates T1,…, Tℓ⊆ ℝd, whether the orbit of (M, s) satisfies φ.In this paper, we establish the following1)The Positivity Problem for LRS over real algebraic numbers reduces to the Positivity Problem for LRS over the integers; and2)The model-checking problem for LDS with diagonalisable M is decidable subject to a Positivity oracle for simple LRS over the integers.In other words, the full semialgebraic model-checking problem for diagonalisable linear dynamical systems is no harder than the Positivity Problem for simple integer linear recurrence sequences. This is in sharp contrast with the situation for arbitrary (not necessarily diagonalisable) LDS and arbitrary (not necessarily simple) integer LRS, for which no such correspondence is expected to hold.

We consider the model-checking problem for parametric probabilistic dynamical systems, formalised as Markov chains with parametric transition functions, analysed under the distribution-transformer semantics (in which a Markov chain induces a sequence of distributions over states). We examine the problem of synthesising the set of parameter valuations of a parametric Markov chain such that the orbits of induced state distributions satisfy a prefix-independent ω-regular property. Our main result establishes that in all non-degenerate instances, the feasible set of parameters is (up to a null set) semialgebraic, and can moreover be computed (in polynomial time assuming that the ambient dimension, corresponding to the number of states of the Markov chain, is fixed).

We study fundamental reachability problems on pseudo-orbits of linear dynamical systems. Pseudo-orbits can be viewed as a model of computation with limited precision and pseudo-reachability can be thought of as a robust version of classical reachability. Using an approach based on $o$-minimality of $\reals_{\exp}$ we prove decidability of the discrete-time pseudo-reachability problem with arbitrary semialgebraic targets for diagonalisable linear dynamical systems. We also show that our method can be used to reduce the continuous-time pseudo-reachability problem to the (classical) time-bounded reachability problem, which is known to be conditionally decidable.

We consider the MSO model-checking problem for simple linear loops, or equivalently discrete-time linear dynamical systems, with semialgebraic predicates (i.e., Boolean combinations of polynomial inequalities on the variables). We place no restrictions on the number of program variables, or equivalently the ambient dimension. We establish decidability of the model-checking problem provided that each semialgebraic predicate either has intrinsic dimension at most 1, or is contained within some three-dimensional subspace. We also note that lifting either of these restrictions and retaining decidability would necessarily require major breakthroughs in number theory.

We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters. More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix $N \in \mathbb{R}^{d\times d}$, and a positive integer $n\in \mathbb{N}$, such that $N^nu = v$. We show decidability for the case in which $M$ depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.

We study fundamental decision problems on linear dynamical systems in discrete time. We focus on pseudo-orbits, the collection of trajectories of the dynamical system for which there is an arbitrarily small perturbation at each step. Pseudo-orbits are generalizations of orbits in the topological theory of dynamical systems. We study the pseudo-orbit problem, whether a state belongs to the pseudo-orbit of another state, and the pseudo-Skolem problem, whether a hyperplane is reachable by an ε-pseudo-orbit for every ε. These problems are analogous to the well-studied orbit problem and Skolem problem on unperturbed dynamical systems. Our main results show that the pseudo-orbit problem is decidable in polynomial time and the Skolem problem on pseudo-orbits is decidable. The former extends the seminal result of Kannan and Lipton from orbits to pseudo-orbits. The latter is in contrast to the Skolem problem for linear dynamical systems, which remains open for proper orbits.

We consider the problem of deciding ω-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent ω-regular property and a sequence of numbers satisfying a linear recurrence, and determines whether the sign description of the sequence (obtained by replacing each positive entry with “+”, each negative entry with “−”, and each zero entry with “0”) satisfies the given property. Our procedure requires that the recurrence be simple, i.e., that the update matrix of the underlying loop be diagonalisable. This assumption is instrumental in proving our key technical lemma: namely that the sign description of a simple linear recurrence sequence is almost periodic in the sense of Muchnik, Sem'enov, and Ushakov. To complement this lemma, we give an example of a linear recurrence sequence whose sign description fails to be almost periodic. Generalising from sign descriptions, we also consider the verification of properties involving semi-algebraic predicates on program variables.

We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix M ∈ ℚ^{d × d}, an initial vector x ∈ ℚ^{d}, a granularity g ∈ ℚ_+ and a rounding operation [⋅] projecting a vector of ℚ^{d} onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit 𝒪 = ⟨[x], [M[x]],[M[M[x]]],… ⟩, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability - whether a given target y ∈ ℚ^{d} belongs to 𝒪 - is PSPACE-complete for hyperbolic systems (when no eigenvalue of M has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.

Consider a discrete dynamical system given by a square matrix $M \in \mathbb{Q}^{d \times d}$ and a starting point $s \in \mathbb{Q}^d$. The orbit of such a system is the infinite trajectory $\langle s, Ms, M^2s, \ldots\rangle$. Given a collection $T_1, T_2, \ldots, T_m \subseteq \mathbb{R}^d$ of semialgebraic sets, we can associate with each $T_i$ an atomic proposition $P_i$ which evaluates to true at time $n$ if, and only if, $M^ns \in T_i$. This gives rise to the LTL Model-Checking Problem for discrete linear dynamical systems: given such a system $(M,s)$ and an LTL formula over such atomic propositions, determine whether the orbit satisfies the formula. The main contribution of the present paper is to show that the LTL Model-Checking Problem for discrete linear dynamical systems is decidable in dimension 3 or less.