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...
| Príomhchruthaitheoirí: | , , |
|---|---|
| Formáid: | Conference item |
| Teanga: | English |
| Foilsithe / Cruthaithe: |
Leibniz International Proceedings in Informatics
2020
|