Showing 1–12 of 12 results for author: Karimov, T

On the Decidability of Presburger Arithmetic Expanded with Powers

Authors: Toghrul Karimov, Florian Luca, Joris Nieuwveld, Joël Ouaknine, James Worrell

Abstract: We prove that for any integers $α, β> 1$, the existential fragment of the first-order theory of the structure $\langle \mathbb{Z}; 0,1,<, +, α^{\mathbb{N}}, β^{\mathbb{N}}\rangle$ is decidable (where $α^{\mathbb{N}}$ is the set of positive integer powers of $α$, and likewise for $β^{\mathbb{N}}$). On the other hand, we show by way of hardness that decidability of the existential fragment of the th… ▽ More We prove that for any integers $α, β> 1$, the existential fragment of the first-order theory of the structure $\langle \mathbb{Z}; 0,1,<, +, α^{\mathbb{N}}, β^{\mathbb{N}}\rangle$ is decidable (where $α^{\mathbb{N}}$ is the set of positive integer powers of $α$, and likewise for $β^{\mathbb{N}}$). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of $\langle \mathbb{N}; 0,1, <, +, x\mapsto α^x, x \mapsto β^x\rangle$ for any multiplicatively independent $α,β> 1$ would lead to mathematical breakthroughs regarding base-$α$ and base-$β$ expansions of certain transcendental numbers. △ Less

Submitted 6 July, 2024; originally announced July 2024.

Model Checking Markov Chains as Distribution Transformers

Authors: Rajab Aghamov, Christel Baier, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Jakob Piribauer, Mihir Vahanwala

Abstract: The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50\% chance of rain? The conventional perspective is ill-equipped to decide s… ▽ More The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50\% chance of rain? The conventional perspective is ill-equipped to decide such problems regarding the evolution of the initial distribution. The alternate perspective we consider views Markov chains as distribution transformers: the focus is on the sequence of distributions on states at each step, where the evolution is driven by the underlying stochastic transition matrix. More precisely, given an initial distribution vector $μ$, a stochastic update transition matrix $M$, we ask whether the ensuing sequence of distributions $(μ, Mμ, M^2μ, \dots)$ satisfies a given temporal property. This is a special case of the model-checking problem for linear dynamical systems, which is not known to be decidable in full generality. The goal of this article is to delineate the classes of instances for which this problem can be solved, under the assumption that the dynamics is governed by stochastic matrices. △ Less

Submitted 21 June, 2024; originally announced June 2024.

On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates

Authors: Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, James Worrell

Abstract: We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_k \rangle$, for various unary predicates $P_1,\ldots,P_k \subseteq \mathbb{N}$. We focus in particular on "arithmetic" predicates arising in the study of linear recurrence sequences, such as fixed-base powers $\mathsf{Pow}_k = \{k^n : n \in \mathbb{N}\}$, $k$-th powers… ▽ More We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_k \rangle$, for various unary predicates $P_1,\ldots,P_k \subseteq \mathbb{N}$. We focus in particular on "arithmetic" predicates arising in the study of linear recurrence sequences, such as fixed-base powers $\mathsf{Pow}_k = \{k^n : n \in \mathbb{N}\}$, $k$-th powers $\mathsf{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};<,\mathsf{Pow}_2, \mathsf{Fib} \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_6 \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_5 \rangle$ is decidable assuming Schanuel's conjecture; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_4, \mathsf{N}_2 \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{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. △ Less

Submitted 20 May, 2024; v1 submitted 13 May, 2024; originally announced May 2024.

Comments: 17 pages

Multiple Reachability in Linear Dynamical Systems

Authors: Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell

Abstract: We consider reachability decision problems for linear dynamical systems: Given a linear map on $\mathbb{R}^d$ , together with source and target sets, determine whether there is a point in the source set whose orbit, obtained by repeatedly applying the linear map, enters the target set. When the source and target sets are semialgebraic, this problem can be reduced to a point-to-polytope reachabilit… ▽ More We consider reachability decision problems for linear dynamical systems: Given a linear map on $\mathbb{R}^d$ , together with source and target sets, determine whether there is a point in the source set whose orbit, obtained by repeatedly applying the linear map, enters the target set. When the source and target sets are semialgebraic, this problem can be reduced to a point-to-polytope reachability question. The latter is generally believed not to be substantially harder than the well-known Skolem and Positivity Problems. The situation is markedly different for multiple reachability, i.e. the question of whether the orbit visits the target set at least m times, for some given positive integer m. In this paper, we prove that when the source set is semialgebraic and the target set consists of a hyperplane, multiple reachability is undecidable; in fact we already obtain undecidability in ambient dimension d = 10 and with fixed m = 9. Moreover, as we observe that procedures for dimensions 3 up to 9 would imply strong results pertaining to effective solutions of Diophantine equations, we mainly focus on the affine plane ($\mathbb{R}^2$). We obtain two main positive results. We show that multiple reachability is decidable for halfplane targets, and that it is also decidable for general semialgebraic targets, provided the linear map is a rotation. The latter result involves a new method, based on intersections of algebraic subgroups with subvarieties, due to Bombieri and Zannier. △ Less

Submitted 11 March, 2024; originally announced March 2024.

The Monadic Theory of Toric Words

Authors: Valérie Berthé, Toghrul Karimov, Joël Ouaknine, Mihir Vahanwala, James Worrell

Abstract: For which unary predicates $P_1, \ldots, P_m$ is the MSO theory of the structure $\langle \mathbb{N}; <, P_1, \ldots, P_m \rangle$ 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 th… ▽ More For which unary predicates $P_1, \ldots, P_m$ is the MSO theory of the structure $\langle \mathbb{N}; <, P_1, \ldots, P_m \rangle$ 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. △ Less

Submitted 15 December, 2023; v1 submitted 8 November, 2023; originally announced November 2023.

Swarmodroid 1.0: A Modular Bristle-Bot Platform for Robotic Active Matter Studies

Authors: Alexey A. Dmitriev, Alina D. Rozenblit, Vadim A. Porvatov, Mikhail K. Buzakov, Anastasia A. Molodtsova, Daria V. Sennikova, Vyacheslav A. Smirnov, Oleg I. Burmistrov, Timur I. Karimov, Ekaterina M. Puhtina, Nikita A. Olekhno

Abstract: Large swarms of extremely simple robots (i.e., capable just of basic motion activities, like propelling forward or self-rotating) are widely applied to study collective task performance based on self-organization or local algorithms instead of sophisticated programming and global swarm coordination. Moreover, they represent a versatile yet affordable platform for experimental studies in physics, p… ▽ More Large swarms of extremely simple robots (i.e., capable just of basic motion activities, like propelling forward or self-rotating) are widely applied to study collective task performance based on self-organization or local algorithms instead of sophisticated programming and global swarm coordination. Moreover, they represent a versatile yet affordable platform for experimental studies in physics, particularly in active matter - non-equilibrium assemblies of particles converting their energy to a directed motion. However, a large set of robotics platforms is being used in different studies, while the universal design is still lacking. Despite such platforms possess advantages in certain application scenarios, their large number sufficiently limits further development of results in the field, as advancing some study requires to buy or manually produce the corresponding robots. To address this issue, we develop an open-source Swarmodroid 1.0 platform based on bristle-bots with reconfigurable 3D-printed bodies, external control of motion velocity, and basic capabilities of velocity profile programming. In addition, we introduce AMPy software package in Python featuring OpenCV-based extraction of robotic swarm kinematics accompanied by the evaluation of key physical quantities describing the collective dynamics. We perform a detailed analysis of individual Swarmodroids' motion characteristics and address their use cases with two examples: a cargo transport performed by self-rotating robots and a velocity-dependent jam formation in a bottleneck by self-propelling robots. Finally, we provide a comparison of existing centimeter-scale robotic platforms, a review of key quantities describing collective dynamics of many-particle systems, and a comprehensive outlook considering potential applications as well as further directions for fundamental studies and Swarmodroid 1.0 platform development. △ Less

Submitted 22 May, 2023; originally announced May 2023.

Comments: 18 pages, 7 figures, 1 table + Supplementary Information. Comments are welcome

What's Decidable about Discrete Linear Dynamical Systems?

Authors: Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell

Abstract: We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem. We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem. △ Less

Submitted 19 September, 2022; v1 submitted 22 June, 2022; originally announced June 2022.

ACM Class: F.4

The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems

Authors: Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, James Worrell

Abstract: 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 arbitrar… ▽ More 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. △ Less

Submitted 5 July, 2022; v1 submitted 26 April, 2022; originally announced April 2022.

The Orbit Problem for Parametric Linear Dynamical Systems

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, James Worrell

Abstract: 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 poi… ▽ More 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. △ Less

Submitted 13 August, 2021; v1 submitted 21 April, 2021; originally announced April 2021.

Comments: Full version of the paper appearing at CONCUR 2021

Deciding $ω$-Regular Properties on Linear Recurrence Sequences

Authors: Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Jöel Ouaknine, James Worrell

Abstract: 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 recurre… ▽ More 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, \ie, 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ënov, 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. △ Less

Submitted 27 October, 2020; originally announced October 2020.

ACM Class: F.3.1; F.4.1

Reachability in Dynamical Systems with Rounding

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, Markus A. Whiteland

Abstract: 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 \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose ever… ▽ More 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 \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose every entry is a multiple of $g$, we are interested in the behaviour of the orbit $\mathcal{O}={<}[x], [M[x]],[M[M[x]]],\dots{>}$, 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 \in\mathbb{Q}^{d}$ belongs to $\mathcal{O}$---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. △ Less

Submitted 28 September, 2020; originally announced September 2020.

Comments: To appear at FSTTCS'20

On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems

Authors: Toghrul Karimov, Joël Ouaknine, James Worrell

Abstract: 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 tr… ▽ More 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. △ Less

Submitted 9 July, 2020; v1 submitted 6 July, 2020; originally announced July 2020.

Comments: Long version of MFCS 2020 paper (19 pages)