arXiv subjects

Edon Kelmendi

Publications and source records attributed to Edon Kelmendi.

13 recordsLinked to original sources

arXiv2025

Multiple Reachability in Linear Dynamical Systems

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.

cs.LO↗

arXiv2023

Computing the Density of the Positivity Set for Linear Recurrence Sequences

The set of indices that correspond to the positive entries of a sequence of numbers is called its positivity set. In this paper, we study the density of the positivity set of a given linear recurrence sequence, that is the question of how much more frequent are the positive entries compared to the non-positive ones. We show that one can compute this density to arbitrary precision, as well as decide whether it is equal to zero (or one). If the sequence is diagonalisable, we prove that its positivity set is finite if and only if its density is zero. Further, arithmetic properties of densities are treated, in particular we prove that it is decidable whether the density is a rational number, given that the recurrence sequence has at most one pair of dominant complex roots. Finally, we generalise all these results to symbolic orbits of linear dynamical systems, thereby showing that one can decide various properties of such systems, up to a set of density zero.

math.NT↗

arXiv2023

Reachability in Injective Piecewise Affine Maps

One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is decidable. We also study various related problems, in each case either establishing decidability, or showing that they are closely connected to Diophantine properties of certain transcendental numbers, analogous to the positivity problem for linear recurrence sequences. Lastly, we consider topological properties of orbits of one-dimensional piecewise affine maps, not necessarily with two intervals, and negatively answer a question of Bournez, Kurganskyy, and Potapov, about the set of orbits in expanding maps.

math.DS↗

arXiv2022

What's Decidable about Discrete Linear Dynamical Systems?

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.

math.DS↗

arXiv2022

Submixing and Shift-invariant Stochastic Games

We consider zero-sum stochastic games with perfect information and finitely many states and actions. The payoff is computed by a function which associates to each infinite sequence of states and actions a real number. We prove that if the payoff function is both shift-invariant and submixing, then the game is half-positional, i.e. the first player has an optimal strategy which is both deterministic and stationary. This result relies on the existence of epsilon-subgame-perfect strategies in shift-invariant games, a second contribution of the paper. The techniques can be used to establish a third result: for shift-invariant and submixing payoff functions, the existence of finite-memory strategies for player 2 in one-player games implies the same property for two-player games as well.

cs.GT↗

arXiv2020

Deciding $ω$-Regular Properties on Linear Recurrence Sequences

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.

cs.LO↗

arXiv2020

Invariants for Continuous Linear Dynamical Systems

Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel's conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel's conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.

cs.LO↗

arXiv2020

Extensions of $ω$-Regular Languages

We consider extensions of monadic second order logic over $ω$-words, which are obtained by adding one language that is not $ω$-regular. We show that if the added language $L$ has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the $ω$-regular languages are the only decidable Boolean-closed full trio over $ω$-words.

cs.FL↗

arXiv2019

MSO+nabla is undecidable

This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying ``almost surely a branch π \in {0, 1}^w satisfies a formula ϕ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative probabilistic CTL, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+nabla is true in the full binary tree.

cs.LO↗

arXiv2018

Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm

Simple stochastic games can be solved by value iteration (VI), which yields a sequence of under-approximations of the value of the game. This sequence is guaranteed to converge to the value only in the limit. Since no stopping criterion is known, this technique does not provide any guarantees on its results. We provide the first stopping criterion for VI on simple stochastic games. It is achieved by additionally computing a convergent sequence of over-approximations of the value, relying on an analysis of the game graph. Consequently, VI becomes an anytime algorithm returning the approximation of the value and the current error bound. As another consequence, we can provide a simulation-based asynchronous VI algorithm, which yields the same guarantees, but without necessarily exploring the whole game graph.

cs.LO↗

arXiv2017

Emptiness of zero automata is decidable

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of mso, called tmso + zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size and the emptiness problem of nonzero automata is decidable and both in NP and in coNP. These results imply that tmso + zero has decidable satisfiability.

cs.FL↗

arXiv2016

Deciding Maxmin Reachability in Half-Blind Stochastic Games

Two-player, turn-based, stochastic games with reachability conditions are considered, where the maximizer has no information (he is blind) and is restricted to deterministic strategies whereas the minimizer is perfectly informed. We ask the question of whether the game has maxmin 1, in other words we ask whether for all $ε>0$ there exists a deterministic strategy for the (blind) maximizer such that against all the strategies of the minimizer, it is possible to reach the set of final states with probability larger than $1-ε$. This problem is undecidable in general, but we define a class of games, called leaktight half-blind games where the problem becomes decidable. We also show that mixed strategies in general are stronger for both players and that optimal strategies for the minimizer might require infinite-memory.

cs.GT↗

arXiv2015

Deciding the value 1 problem for probabilistic leaktight automata

The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1? This problem was proved undecidable recently; to overcome this, several classes of probabilistic automata of different nature were proposed, for which the value 1 problem has been shown decidable. In this paper, we introduce yet another class of probabilistic automata, called leaktight automata, which strictly subsumes all classes of probabilistic automata whose value 1 problem is known to be decidable. We prove that for leaktight automata, the value 1 problem is decidable (in fact, PSPACE-complete) by constructing a saturation algorithm based on the computation of a monoid abstracting the behaviours of the automaton. We rely on algebraic techniques developed by Simon to prove that this abstraction is complete. Furthermore, we adapt this saturation algorithm to decide whether an automaton is leaktight. Finally, we show a reduction allowing to extend our decidability results from finite words to infinite ones, implying that the value 1 problem for probabilistic leaktight parity automata is decidable.

cs.FL↗