Conference item
On LTL model-checking for low-dimensional discrete linear dynamical systems
- Abstract:
- 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 which evaluates to true at time n if, and only if, M^ns ∈ 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.
- Publication status:
- Published
- Peer review status:
- Reviewed (other)
Actions
Access Document
- Files:
-
-
(Preview, Version of record, 518.3KB, Terms of use)
-
- Publisher copy:
- 10.4230/LIPIcs.MFCS.2020.54
Authors
- Publisher:
- Leibniz International Proceedings in Informatics
- Journal:
- 45th International Symposium on Mathematical Foundations of Computer Science More from this journal
- Volume:
- 170
- Pages:
- 54:1-54:14
- Publication date:
- 2020-08-18
- Acceptance date:
- 2020-06-29
- Event title:
- 45th International Symposium on Mathematical Foundations of Computer Science
- DOI:
- ISSN:
-
1868-8969
- Language:
-
English
- Keywords:
- Pubs id:
-
1115289
- Local pid:
-
pubs:1115289
- Deposit date:
-
2020-07-01
Terms of use
- Copyright holder:
- Karimov et al.
- Copyright date:
- 2020
- Rights statement:
- © Toghrul Karimov, Joël Ouaknine, and James Worrell; licensed under Creative Commons License CC-BY
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record