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...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Leibniz International Proceedings in Informatics
2020
|