Toghrul Karimov

Highlights Conference 2025 Conference Abstract

Ergodicity for linear dynamical systems via o-minimality

• Toghrul Karimov

KR Conference 2025 Conference Paper

Model Checking Linear Temporal Logic with Standpoint Modalities

• Rajab Aghamov
• Christel Baier
• Toghrul Karimov
• Rupak Majumdar
• Joël Ouaknine
• Jakob Piribauer
• Timm Spork

Standpoint linear temporal logic (SLTL) is a recently introduced extension of classical linear temporal logic (LTL) with standpoint modalities. Intuitively, these modalities allow to express that, from agent a's standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to SLTL under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the SLTL satisfiability problem.

SODA Conference 2025 Conference Paper

On the Decidability of Presburger Arithmetic Expanded with Powers

• Toghrul Karimov
• Florian Luca
• Joris Nieuwveld
• Joël Ouaknine
• James Worrell 0001

TCS Journal 2025 Journal Article

The monadic theory of toric words

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

For which unary predicates P 1, …, P m is the MSO theory of the structure 〈 N; <, P 1, …, P m 〉 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. We give various applications of toric words, including the recent result of [1] that the MSO theory of 〈 N; <, { 2 n: n ∈ N }, { 3 n: n ∈ N } 〉 is decidable.

MFCS Conference 2022 Conference Paper

The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems

• Julian D'Costa
• Toghrul Karimov
• Rupak Majumdar
• Joël Ouaknine
• Mahmoud Salamati
• James Worrell 0001

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 ℝ_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.

MFCS Conference 2021 Conference Paper

The Pseudo-Skolem Problem is Decidable

• Julian D'Costa
• Toghrul Karimov
• Rupak Majumdar
• Joël Ouaknine
• Mahmoud Salamati
• Sadegh Soudjani
• James Worrell 0001

We study fundamental decision problems on linear dynamical systems in discrete time. We focus on pseudo-orbits, the collection of trajectories of the dynamical system for which there is an arbitrarily small perturbation at each step. Pseudo-orbits are generalizations of orbits in the topological theory of dynamical systems. We study the pseudo-orbit problem, whether a state belongs to the pseudo-orbit of another state, and the pseudo-Skolem problem, whether a hyperplane is reachable by an ε-pseudo-orbit for every ε. These problems are analogous to the well-studied orbit problem and Skolem problem on unperturbed dynamical systems. Our main results show that the pseudo-orbit problem is decidable in polynomial time and the Skolem problem on pseudo-orbits is decidable. The former extends the seminal result of Kannan and Lipton from orbits to pseudo-orbits. The latter is in contrast to the Skolem problem for linear dynamical systems, which remains open for proper orbits.

MFCS Conference 2020 Conference Paper

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

• Toghrul Karimov
• Joël Ouaknine
• James Worrell 0001

Consider a discrete dynamical system given by a square matrix M ∈ ℚ^{d × d} and a starting point s ∈ ℚ^d. The orbit of such a system is the infinite trajectory ⟨ s, Ms, M²s, …⟩. Given a collection T₁, T₂, …, T_m ⊆ ℝ^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 ∈ 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.