This series is devoted to the publication of research monographs, lecture notes, and other
material arising from programs of the Institut de Recherche Mathématique Avancée …

We survey the complexity class $\exists\mathbb {R} $, which captures the complexity of
deciding the existential theory of the reals. The class $\exists\mathbb {R} $ has roots in two …

Given a linear recurrence sequence (LRS) over the integers, the Positivity Problem asks
whether all terms of the sequence are positive. We show that, for simple LRS (those whose …

A sequence of real numbers is said to be positive if all terms are positive, and ultimately
positive if all but finitely many terms are positive. In this article we survey recent progress on …

We consider the MSO model-checking problem for simple linear loops, or equivalently
discrete-time linear dynamical systems, with semialgebraic predicates (ie, Boolean …

We show that completeness at higher levels of the theory of the reals is a robust notion
(under changing the signature and bounding the domain of the quantifiers). This mends …

We consider the following decision problem: given a finite Markov chain with distinguished
source and target states, and given a rational number r, does there exist an integer n such …

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 …

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∈N over R, whether un≥ 0 for all n …

A fundamental problem in program verification concerns the termination of simple linear
loops of the form: where x is a vector of variables, u, a, and c are integer vectors, and A and …