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...
| Asıl Yazarlar: | , , |
|---|---|
| Materyal Türü: | Conference item |
| Dil: | English |
| Baskı/Yayın Bilgisi: |
Leibniz International Proceedings in Informatics
2020
|