## On LTL model-checking for low-dimensional discrete linear dynamical systems

*Toghrul Karimov*, *Joël
Ouaknine*, and *James Worrell*
Consider a discrete dynamical system given by a square matrix
*M* ∈ **Q**^{d×d}
and a starting point
*s* ∈ **Q**^{d}. The *orbit* of such a
system is the infinite trajectory <*s*, *Ms*, *M*^{2}*s*,...> . Given a collection
*T*_{1}, *T*_{2}, ... ,
*T*_{m} ⊆ **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*^{n}*s* ∈ *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.

*Proceedings of MFCS 20*, LIPIcs 170, 2020. 18 pages.

PDF
© 2020 Toghrul Karimov, Joël Ouaknine, and James Worrell.

Imprint / Data Protection