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.

One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is decidable.We also study various related problems, in each case either establishing decidability, or showing that they are closely connected to Diophantine properties of certain transcendental numbers, analogous to the positivity problem for linear recurrence sequences. Lastly, we consider topological properties of orbits of one-dimensional piecewise affine maps, not necessarily with two intervals, and negatively answer a question of Bournez, Kurganskyy, and Potapov, about the set of orbits in expanding maps.

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.

The set of indices that correspond to the positive entries of a sequence of numbers is called its positivity set. In this paper, we study the density of the positivity set of a given linear recurrence sequence, that is the question of how much more frequent are the positive entries compared to the non-positive ones. We show that one can compute this density to arbitrary precision, as well as decide whether it is equal to zero (or one). If the sequence is diagonalisable, we prove that its positivity set is finite if and only if its density is zero. Lastly, arithmetic properties of densities are treated, in particular we prove that it is decidable whether the density is a rational number, given that the recurrence sequence has at most one pair of dominant complex roots.

The classical problem of reachability in simple stochastic games is typically solved by value iteration (VI), which produces a sequence of under-approximations of the value of the game, but is only guaranteed to converge in the limit. We provide an additional converging sequence of over-approximations, based on an analysis of the game graph. Together, these two sequences entail the first error bound and hence the first stopping criterion for VI on simple stochastic games, indicating when the algorithm can be stopped for a given precision. Consequently, VI becomes an anytime algorithm returning the approximation of the value and the current error bound. We further use this error bound to provide a learning-based asynchronous VI algorithm; it uses simulations and thus often avoids exploring the whole game graph, but still yields the same guarantees. Finally, we experimentally show that the overhead for computing the additional sequence of over-approximations often is negligible.

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.

Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel's conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel's conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.

We consider extensions of monadic second-order logic over ω-words, which are obtained by adding one language that is not ω-regular. We show that if the added language L has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the ω-regular languages are the only decidable Boolean-closed full trio over ω-words.

This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying “almost surely a branch π ∈ {0,1}ωsatisfies a formula φ(π)”, This logic was introduced by Michalewski and Mio; we call it MSO+∇ following notation of Shelah and Lehmann. The logic Mso+∇ subsumes many qualitative probabilistic formalisms, including qualitative probabilistic check, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+∇ is true in the full binary tree11Independently and in parallel another proof of this result was given employing different techniques in [3]..

Simple stochastic games can be solved by value iteration (VI), which yields a sequence of under-approximations of the value of the game. This sequence is guaranteed to converge to the value only in the limit. Since no stopping criterion is known, this technique does not provide any guarantees on its results. We provide the first stopping criterion for VI on simple stochastic games. It is achieved by additionally computing a convergent sequence of over-approximations of the value, relying on an analysis of the game graph. Consequently, VI becomes an anytime algorithm returning the approximation of the value and the current error bound. As another consequence, we can provide a simulation-based asynchronous VI algorithm, which yields the same guarantees, but without necessarily exploring the whole game graph.

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of MSO, called TMSO+zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size and the emptiness problem of nonzero automata is decidable, with complexity co-NP. These results imply that TMSO+zero has decidable satisfiability.