On LTL model-checking for low-dimensional discrete linear dynamical systems
| Autor: | Karimov, Toghrul, Ouaknine, Joël, Worrell, James |
|---|---|
| Přispěvatelé: | Javier Esparza, Daniel Kráľ |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
FOS: Computer and information sciences
060201 languages & linguistics Computer Science - Logic in Computer Science Orbit Problem LTL model checking Linear dynamical systems 0602 languages and literature 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 06 humanities and the arts 02 engineering and technology Theory of computation → Logic and verification Logic in Computer Science (cs.LO) |
| Zdroj: | 45th International Symposium on Mathematical Foundations of Computer Science Leibniz International Proceedings in Informatics 45th International Symposium on Mathematical Foundations of Computer Science (MFCS) |
| DOI: | 10.4230/lipics.mfcs.2020.54 |
| Popis: | Consider a discrete dynamical system given by a square matrix $M \in \mathbb{Q}^{d \times d}$ and a starting point $s \in \mathbb{Q}^d$. The orbit of such a system is the infinite trajectory $\langle s, Ms, M^2s, \ldots\rangle$. Given a collection $T_1, T_2, \ldots, T_m \subseteq \mathbb{R}^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 \in 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. Comment: Long version of MFCS 2020 paper (19 pages) |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|