Mihir Vahanwala

Valérie Berthé, Toghrul Karimov, Joris Nieuwveld et al.

We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_d \rangle$, for various unary predicates $P_1,\ldots,P_d \subseteq \mathbb{N}$. We focus in particular on 'arithmetic' predicates arising in the study of linear recurrence sequences, such as fixed-base powers $k^{\mathbf{N}} = \{k^n : n \in \mathbb{N}\}$, $k$-th powers $\mathbf{N}^k = \{n^k : n \in \mathbb{N}\}$, and the set of terms of the Fibonacci sequence $\mathsf{Fib} = \{0,1,2,3,5,8,13,\ldots\}$ (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: $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, \mathsf{Fib} \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, 3^{\mathbf{N}}, 6^{\mathbf{N}} \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, 3^{\mathbf{N}}, 5^{\mathbf{N}} \rangle$ is decidable assuming Schanuel's conjecture; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 4^{\mathbf{N}}, \mathbf{N}^2 \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, \mathbf{N}^2 \rangle$ is Turing-equivalent to the MSO theory of $\langle \mathbb{N};<,S \rangle$, where $S$ is the predicate corresponding to the binary expansion of $\sqrt{2}$. (As the binary expansion of $\sqrt{2}$ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.) These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.

Piotr Bacik, Joris Nieuwveld, Joël Ouaknine et al.

We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form $2n^3-5n+3$, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. In the case of single-variable theories, we obtain positive results for the following two families of predicates: (i) for perfect fixed powers, decidability ofthe corresponding theory follows from the solvability of hyperellipticDiophantine equations; and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves. Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.

Rajab Aghamov, Christel Baier, Joel Ouaknine et al.

Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding if a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is NP- and coNP-hard. We also identify natural restrictions on the graphical structure of DBNs that make the verification of structural CI properties tractable.