Joel Ouaknine

Ventsislav Chonev, Joel Ouaknine, James Worrell

The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differential equation has a zero in a given interval of real numbers. This is a fundamental reachability problem for continuous linear dynamical systems, such as linear hybrid automata and continuous-time Markov chains. Decidability of the problem is currently open---indeed decidability is open even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show decidability of the bounded problem subject to Schanuel's Conjecture, a unifying conjecture in transcendental number theory. We furthermore analyse the unbounded problem in terms of the frequencies of the differential equation, that is, the imaginary parts of the characteristic roots. We show that the unbounded problem can be reduced to the bounded problem if there is at most one rationally linearly independent frequency, or if there are two rationally linearly independent frequencies and all characteristic roots are simple. We complete the picture by showing that decidability of the unbounded problem in the case of two (or more) rationally linearly independent frequencies would entail a major new effectiveness result in Diophantine approximation, namely computability of the Diophantine-approximation types of all real algebraic numbers.

Ventsislav Chonev, Joel Ouaknine, James Worrell

The continuous evolution of a wide variety of systems, including continuous-time Markov chains and linear hybrid automata, can be described in terms of linear differential equations. In this paper we study the decision problem of whether the solution $\boldsymbol{x}(t)$ of a system of linear differential equations $d\boldsymbol{x}/dt=A\boldsymbol{x}$ reaches a target halfspace infinitely often. This recurrent reachability problem can equivalently be formulated as the following Infinite Zeros Problem: does a real-valued function $f:\mathbb{R}_{\geq 0}\rightarrow\mathbb{R}$ satisfying a given linear differential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most $7$, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order $9$ (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.

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.