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

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 wh...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí: Karimov, T, Ouaknine, J, Worrell, J
Formáid: Conference item
Teanga:English
Foilsithe / Cruthaithe: Leibniz International Proceedings in Informatics 2020