Affine Subspace Reachability Problem

Speaker: 

Time: 

Thursday, 5 December 2019, 15:30 to 16:30

Venue: 

  • A-201 (STCS Seminar Room)

Abstract:  Discrete-time linear systems are a ubiquitous modeling tool across the sciences. We study a reachability problem related to discrete-time linear systems which we call ``Affine Subspace Reachability Problem''. Given a linear operator $M$, a vector $v$ and an affine subspace $W$, this problem asks whether there is a time $t$ such that $M^tv$ is in  $W$. A rich body of research has developed around several special cases of this problem, such as the Orbit Problem, the Skolem Problem and the Extended Orbit Problem.
\par In this report, we survey some of the results known about the various special cases of the Affine Subspace Reachability Problem. We begin by observing the equivalence of the ``Affine Subspace Reachability Problem'' with some special cases as an immediate consequence of famous Skolem-Mahler-Lech theorem. We then provide a constructive proof of Skolem-Mahler-Lech theorem for the case when the eigenvalues of $M$ are roots of real numbers. We use this proof to construct an algorithm for the Skolem Problem for the same case.
\par We then investigate the limitation of our proof technique by exhibiting a decidable problem for which the eigenvalues of the corresponding $M$ are not roots of real numbers. More specifically, we consider the sequence $a_t = \cos t \theta$ (where $\theta$ is not a rational multiple of $\pi$ and $\cos \theta$ is algebraic), and show that the problem of whether there exists a $t$ such that $a_t = c$ is a decidable special case of the general affine subspace reachability problem. We also exhibit that the eigenvalues of the corresponding matrix are not roots of reals.
\par  We also show efficient decidability of the problem of deciding if a state of an ergodic Markov chain can approximately achieve a given probability starting from the distribution in which the system is in a given state with probability 1.
\par This work is done to prepare a ground for future works in the direction of verification of succinctly represented probabilistic models such as the Ising model.

(This is done under the supervision of S Akshay (IIT B) and Piyush Srivastava)